Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/lazy_tree_proof_generator.h	Lines:	13	14	92.9 %
Date:	2021-05-22	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__THEORY__LAZY_TREE_PROOF_GENERATOR_H
#define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H

#include <iostream>

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

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