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