Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/lazy_tree_proof_generator.h	Lines:	11	14	78.6 %
Date:	2021-11-07	Branches:	7	14	50.0 %


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