Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/lazy_tree_proof_generator.h	Lines:	13	14	92.9 %
Date:	2021-08-03	Branches:	9	14	64.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The lazy tree proof generator class.
 */

#include "cvc5_private.h"

#ifndef CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H
#define CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H

#include <iostream>

#include "expr/node.h"
#include "proof/proof_generator.h"
#include "proof/proof_node_manager.h"

namespace cvc5 {
namespace detail {
/**
 * A single node in the proof tree created by the LazyTreeProofGenerator.
 * A node directly represents a ProofNode that is eventually constructed from
 * it. The Nodes of the additional field d_premise are added to d_children as
 * new assumptions via ASSUME.
 */
struct TreeProofNode
{
  /** The proof rule */
  PfRule d_rule = PfRule::UNKNOWN;
  /** Assumptions used as premise for this proof step */
  std::vector<Node> d_premise;
  /** Arguments for this proof step */
  std::vector<Node> d_args;
  /** Conclusion of this proof step */
  Node d_proven;
  /** Children of this proof step */
  std::vector<TreeProofNode> d_children;
};
}  // namespace detail

/**
 * This class supports the lazy creation of a tree-shaped proof.
 * The core idea is that the lazy creation is necessary because proof rules
 * depend on assumptions that are only known after the whole subtree has been
 * finished.
 *
 * We indend to argue about proofs that roughly go as follows:
 * - we assume a set of assumptions
 * - we do a case split
 * - for every case, we derive false, possibly by nested case splits
 *
 * Every case is represented by a SCOPE whose child derives false. When
 * composing the final proof, we explicitly extend the premise of every proof
 * step with the scope (the currently selected case) that this proof step lives
 * in. When doing this, we ignore the outermost scope (which assumes the
 * assertion set) to allow for having conflicts that are only a subset of the
 * assertion set.
 *
 * Consider the example  x*x<1 and x>2  and the intended proof
 *  (SCOPE
 *    (ARITH_NL_CAD_SPLIT
 *      (SCOPE
 *        (ARITH_NL_CAD_DIRECT  (x<=2  and  x>2) ==> false)
 *        :args [x<=2]
 *      )
 *      (SCOPE
 *        (ARITH_NL_CAD_DIRECT  (x>=1  and  x*x<1) ==> false)
 *        :args [x>=1]
 *      )
 *    )
 *    :args [ x*x<1, x>2 ]
 *  )
 * We obtain this proof in a way that (in general) gives us the assumptions
 * for the scopes (x<=2, x>=1) only when the scope children have been fully
 * computed. Thus, we store the proof in an intermediate form and add the scope
 * arguments when we learn them. Once we have completed the proof, we can easily
 * transform it into proper ProofNodes.
 *
 * This class is stateful in the sense that the interface (in particular
 * openChild() and closeChild()) navigates the proof tree (and creating it
 * on-the-fly). Initially, and after reset() has been called, the proof consists
 * of one empty proof node (with proof rule UNKNOWN). It stores the current
 * position in the proof tree internally to make the interface easier to use.
 *
 * THIS MAKES THIS CLASS INHERENTLY NOT THREAD-SAFE!
 *
 * To construct the above proof, use this class roughly as follows:
 *  setCurrent(SCOPE, {}, assertions, false);
 *  openChild();
 *  // First nested scope
 *  openChild();
 *  setCurrent(SCOPE, {}, {}, false);
 *  openChild();
 *  setCurrent(CAD_DIRECT, {x>2}, {}, false);
 *  closeChild();
 *  getCurrent().args = {x<=2};
 *  closeChild();
 *  // Second nested scope
 *  openChild();
 *  setCurrent(SCOPE, {}, {}, false);
 *  openChild();
 *  setCurrent(CAD_DIRECT, {x*x<1}, {}, false);
 *  closeChild();
 *  getCurrent().args = {x>=1};
 *  closeChild();
 *  // Finish split
 *  setCurrent(CAD_SPLIT, {}, {}, false);
 *  closeChild();
 *  closeChild();
 *
 * To explicitly finish proof construction, we need to call closeChild() one
 * additional time.
 */
class LazyTreeProofGenerator : public ProofGenerator
{
 public:
  friend std::ostream& operator<<(std::ostream& os,
                                  const LazyTreeProofGenerator& ltpg);

  LazyTreeProofGenerator(ProofNodeManager* pnm,
                         const std::string& name = "LazyTreeProofGenerator");

  std::string identify() const override { return d_name; }
  /** Create a new child and make it the current node */
  void openChild();
  /**
   * Finish the current node and return to its parent
   * Checks that the current node has a proof rule different from UNKNOWN.
   * When called on the root node, this finishes the proof construction: we can
   * no longer call getCurrent(), setCurrent() openChild() and closeChild(), but
   * instead can call getProof() now.
   */
  void closeChild();
  /**
   * Return a reference to the current node
   */
  detail::TreeProofNode& getCurrent();
  /** Set the current node / proof step */
  void setCurrent(PfRule rule,
                  const std::vector<Node>& premise,
                  std::vector<Node> args,
                  Node proven);
  /** Construct the proof as a ProofNode */
  std::shared_ptr<ProofNode> getProof() const;
  /** Return the constructed proof. Checks that we have proven f */
  std::shared_ptr<ProofNode> getProofFor(Node f) override;
  /** Checks whether we have proven f */
  bool hasProofFor(Node f) override;

  /**
   * Removes children from the current node based on the given predicate.
   * It can be used for cases where facts (and their proofs) are eagerly
   * generated and then later pruned, for example to produce smaller conflicts.
   * The predicate is given as a Callable f that is called for every child with
   * the id of the child and the child itself.
   * f should return true if the child should be kept, fals if the child should
   * be removed.
   * @param f a Callable bool(std::size_t, const detail::TreeProofNode&)
   */
  template <typename F>
  void pruneChildren(F&& f)
  {
    auto& children = getCurrent().d_children;
    std::size_t cur = 0;
    std::size_t pos = 0;
    for (std::size_t size = children.size(); cur < size; ++cur)
    {
      if (f(cur, children[pos]))
      {
        if (cur != pos)
        {
          children[pos] = std::move(children[cur]);
        }
        ++pos;
      }
    }
    children.resize(pos);
  }

 private:
  /** recursive proof construction used by getProof() */
  std::shared_ptr<ProofNode> getProof(
      std::vector<std::shared_ptr<ProofNode>>& scope,
      const detail::TreeProofNode& pn) const;

  /** recursive debug printing used by operator<<() */
  void print(std::ostream& os,
             const std::string& prefix,
             const detail::TreeProofNode& pn) const;

  /** The ProofNodeManager used for constructing ProofNodes */
  ProofNodeManager* d_pnm;
  /** The trace to the current node */
  std::vector<detail::TreeProofNode*> d_stack;
  /** The root node of the proof tree */
  detail::TreeProofNode d_proof;
  /** Caches the result of getProof() */
  mutable std::shared_ptr<ProofNode> d_cached;
  /** Name of this proof generator */
  std::string d_name;
};

/**
 * Prints the current state of a LazyTreeProofGenerator. Can also be used on a
 * partially constructed proof. It is intended for debugging only and attempts
 * to pretty-print itself using indentation.
 */
std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);

}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* The lazy tree proof generator class.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H
19		#define CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H
20
21		#include <iostream>
22
23		#include "expr/node.h"
24		#include "proof/proof_generator.h"
25		#include "proof/proof_node_manager.h"
26
27		namespace cvc5 {
28		namespace detail {
29		/**
30		* A single node in the proof tree created by the LazyTreeProofGenerator.
31		* A node directly represents a ProofNode that is eventually constructed from
32		* it. The Nodes of the additional field d_premise are added to d_children as
33		* new assumptions via ASSUME.
34		*/
35	40	struct TreeProofNode
36		{
37		/** The proof rule */
38		PfRule d_rule = PfRule::UNKNOWN;
39		/** Assumptions used as premise for this proof step */
40		std::vector<Node> d_premise;
41		/** Arguments for this proof step */
42		std::vector<Node> d_args;
43		/** Conclusion of this proof step */
44		Node d_proven;
45		/** Children of this proof step */
46		std::vector<TreeProofNode> d_children;
47		};
48		} // namespace detail
49
50		/**
51		* This class supports the lazy creation of a tree-shaped proof.
52		* The core idea is that the lazy creation is necessary because proof rules
53		* depend on assumptions that are only known after the whole subtree has been
54		* finished.
55		*
56		* We indend to argue about proofs that roughly go as follows:
57		* - we assume a set of assumptions
58		* - we do a case split
59		* - for every case, we derive false, possibly by nested case splits
60		*
61		* Every case is represented by a SCOPE whose child derives false. When
62		* composing the final proof, we explicitly extend the premise of every proof
63		* step with the scope (the currently selected case) that this proof step lives
64		* in. When doing this, we ignore the outermost scope (which assumes the
65		* assertion set) to allow for having conflicts that are only a subset of the
66		* assertion set.
67		*
68		* Consider the example x*x<1 and x>2 and the intended proof
69		* (SCOPE
70		* (ARITH_NL_CAD_SPLIT
71		* (SCOPE
72		* (ARITH_NL_CAD_DIRECT (x<=2 and x>2) ==> false)
73		* :args [x<=2]
74		* )
75		* (SCOPE
76		* (ARITH_NL_CAD_DIRECT (x>=1 and x*x<1) ==> false)
77		* :args [x>=1]
78		* )
79		* )
80		* :args [ x*x<1, x>2 ]
81		* )
82		* We obtain this proof in a way that (in general) gives us the assumptions
83		* for the scopes (x<=2, x>=1) only when the scope children have been fully
84		* computed. Thus, we store the proof in an intermediate form and add the scope
85		* arguments when we learn them. Once we have completed the proof, we can easily
86		* transform it into proper ProofNodes.
87		*
88		* This class is stateful in the sense that the interface (in particular
89		* openChild() and closeChild()) navigates the proof tree (and creating it
90		* on-the-fly). Initially, and after reset() has been called, the proof consists
91		* of one empty proof node (with proof rule UNKNOWN). It stores the current
92		* position in the proof tree internally to make the interface easier to use.
93		*
94		* THIS MAKES THIS CLASS INHERENTLY NOT THREAD-SAFE!
95		*
96		* To construct the above proof, use this class roughly as follows:
97		* setCurrent(SCOPE, {}, assertions, false);
98		* openChild();
99		* // First nested scope
100		* openChild();
101		* setCurrent(SCOPE, {}, {}, false);
102		* openChild();
103		* setCurrent(CAD_DIRECT, {x>2}, {}, false);
104		* closeChild();
105		* getCurrent().args = {x<=2};
106		* closeChild();
107		* // Second nested scope
108		* openChild();
109		* setCurrent(SCOPE, {}, {}, false);
110		* openChild();
111		* setCurrent(CAD_DIRECT, {x*x<1}, {}, false);
112		* closeChild();
113		* getCurrent().args = {x>=1};
114		* closeChild();
115		* // Finish split
116		* setCurrent(CAD_SPLIT, {}, {}, false);
117		* closeChild();
118		* closeChild();
119		*
120		* To explicitly finish proof construction, we need to call closeChild() one
121		* additional time.
122		*/
123	1	class LazyTreeProofGenerator : public ProofGenerator
124		{
125		public:
126		friend std::ostream& operator<<(std::ostream& os,
127		const LazyTreeProofGenerator& ltpg);
128
129		LazyTreeProofGenerator(ProofNodeManager* pnm,
130		const std::string& name = "LazyTreeProofGenerator");
131
132	3	std::string identify() const override { return d_name; }
133		/** Create a new child and make it the current node */
134		void openChild();
135		/**
136		* Finish the current node and return to its parent
137		* Checks that the current node has a proof rule different from UNKNOWN.
138		* When called on the root node, this finishes the proof construction: we can
139		* no longer call getCurrent(), setCurrent() openChild() and closeChild(), but
140		* instead can call getProof() now.
141		*/
142		void closeChild();
143		/**
144		* Return a reference to the current node
145		*/
146		detail::TreeProofNode& getCurrent();
147		/** Set the current node / proof step */
148		void setCurrent(PfRule rule,
149		const std::vector<Node>& premise,
150		std::vector<Node> args,
151		Node proven);
152		/** Construct the proof as a ProofNode */
153		std::shared_ptr<ProofNode> getProof() const;
154		/** Return the constructed proof. Checks that we have proven f */
155		std::shared_ptr<ProofNode> getProofFor(Node f) override;
156		/** Checks whether we have proven f */
157		bool hasProofFor(Node f) override;
158
159		/**
160		* Removes children from the current node based on the given predicate.
161		* It can be used for cases where facts (and their proofs) are eagerly
162		* generated and then later pruned, for example to produce smaller conflicts.
163		* The predicate is given as a Callable f that is called for every child with
164		* the id of the child and the child itself.
165		* f should return true if the child should be kept, fals if the child should
166		* be removed.
167		* @param f a Callable bool(std::size_t, const detail::TreeProofNode&)
168		*/
169		template <typename F>
170	3	void pruneChildren(F&& f)
171		{
172	3	auto& children = getCurrent().d_children;
173	3	std::size_t cur = 0;
174	3	std::size_t pos = 0;
175	9	for (std::size_t size = children.size(); cur < size; ++cur)
176		{
177	6	if (f(cur, children[pos]))
178		{
179	5	if (cur != pos)
180		{
181		children[pos] = std::move(children[cur]);
182		}
183	5	++pos;
184		}
185		}
186	3	children.resize(pos);
187	3	}
188
189		private:
190		/** recursive proof construction used by getProof() */
191		std::shared_ptr<ProofNode> getProof(
192		std::vector<std::shared_ptr<ProofNode>>& scope,
193		const detail::TreeProofNode& pn) const;
194
195		/** recursive debug printing used by operator<<() */
196		void print(std::ostream& os,
197		const std::string& prefix,
198		const detail::TreeProofNode& pn) const;
199
200		/** The ProofNodeManager used for constructing ProofNodes */
201		ProofNodeManager* d_pnm;
202		/** The trace to the current node */
203		std::vector<detail::TreeProofNode*> d_stack;
204		/** The root node of the proof tree */
205		detail::TreeProofNode d_proof;
206		/** Caches the result of getProof() */
207		mutable std::shared_ptr<ProofNode> d_cached;
208		/** Name of this proof generator */
209		std::string d_name;
210		};
211
212		/**
213		* Prints the current state of a LazyTreeProofGenerator. Can also be used on a
214		* partially constructed proof. It is intended for debugging only and attempts
215		* to pretty-print itself using indentation.
216		*/
217		std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);
218
219		} // namespace cvc5
220
221		#endif