Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Gereon Kremer
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 proof-producing equality engine.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
19 : : #define CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
20 : :
21 : : #include <vector>
22 : :
23 : : #include "context/cdhashmap.h"
24 : : #include "context/cdhashset.h"
25 : : #include "expr/node.h"
26 : : #include "proof/assumption_proof_generator.h"
27 : : #include "proof/buffered_proof_generator.h"
28 : : #include "proof/eager_proof_generator.h"
29 : : #include "proof/lazy_proof.h"
30 : : #include "smt/env_obj.h"
31 : :
32 : : namespace cvc5::internal {
33 : :
34 : : class Env;
35 : : class ProofNode;
36 : : class ProofNodeManager;
37 : :
38 : : namespace theory {
39 : : namespace eq {
40 : :
41 : : class EqualityEngine;
42 : :
43 : : /**
44 : : * A layer on top of an EqualityEngine. The goal of this class is manage the
45 : : * use of an EqualityEngine object in such a way that the proper proofs are
46 : : * internally constructed, and can be retrieved from this class when
47 : : * necessary.
48 : : *
49 : : * Notice that this class is intended to be a *partial layer* on top of
50 : : * equality engine. A user of this class should still issue low-level calls
51 : : * (getRepresentative, areEqual, areDisequal, etc.) on the underlying equality
52 : : * engine directly. The methods that should *not* be called directly on the
53 : : * underlying equality engine are:
54 : : * - assertEquality/assertPredicate [*]
55 : : * - explain
56 : : * Instead, the user should use variants of the above methods provided by
57 : : * the public interface of this class.
58 : : *
59 : : * [*] the exception is that assertions from the fact queue (who are their own
60 : : * explanation) should be sent directly to the underlying equality engine. This
61 : : * is for the sake of efficiency.
62 : : *
63 : : * This class tracks the reason for why all facts are added to an EqualityEngine
64 : : * in a SAT-context dependent manner in a context-dependent (CDProof) object.
65 : : * It furthermore maintains an internal FactProofGenerator class for managing
66 : : * proofs of facts whose steps are explicitly provided (those that are given
67 : : * concrete ProofRule, children, and args). Call these "simple facts".
68 : : *
69 : : * Overall, this class is an eager proof generator (theory/proof_generator.h),
70 : : * in that it stores (copies) of proofs for lemmas at the moment they are sent
71 : : * out.
72 : : *
73 : : * A theory that is proof producing and uses the equality engine may use this
74 : : * class to manage proofs that are justified by its underlying equality engine.
75 : : * In particular, the following interfaces are available for constructing
76 : : * a TrustNode:
77 : : * - assertConflict, when the user of the equality engine has discovered that
78 : : * false can be derived from the current state,
79 : : * - assertLemma, for lemmas/conflicts that can be (partially) explained in the
80 : : * current state,
81 : : * - explain, for explaining why a literal is true in the current state.
82 : : * Details on these methods can be found below.
83 : : */
84 : : class ProofEqEngine : public EagerProofGenerator
85 : : {
86 : : typedef context::CDHashSet<Node> NodeSet;
87 : : typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofMap;
88 : :
89 : : public:
90 : : /**
91 : : * @param env The environment
92 : : * @param ee The equality engine this is layered on
93 : : */
94 : : ProofEqEngine(Env& env, EqualityEngine& ee);
95 : 275328 : ~ProofEqEngine() {}
96 : : //-------------------------- assert fact
97 : : /**
98 : : * Assert the literal lit by proof step id, given explanation exp and
99 : : * arguments args. This fact is
100 : : *
101 : : * @param lit The literal to assert to the equality engine
102 : : * @param id The proof rule of the proof step concluding lit
103 : : * @param exp The premises of the proof step concluding lit. These are also
104 : : * the premises that are used when calling explain(lit).
105 : : * @param args The arguments to the proof step concluding lit.
106 : : * @return true if this fact was processed by this method. If lit already
107 : : * holds in the equality engine, this method returns false.
108 : : */
109 : : bool assertFact(Node lit,
110 : : ProofRule id,
111 : : const std::vector<Node>& exp,
112 : : const std::vector<Node>& args);
113 : : /** Same as above but where exp is (conjunctive) node */
114 : : bool assertFact(Node lit,
115 : : ProofRule id,
116 : : Node exp,
117 : : const std::vector<Node>& args);
118 : : /**
119 : : * Multi-step version of assert fact via a proof step buffer. This method
120 : : * is similar to above, but the justification for lit may have multiple steps.
121 : : * In particular, we assume that psb has a list of proof steps where the
122 : : * proof step concluding lit has free assumptions exp.
123 : : *
124 : : * For example, a legal call to this method is such that:
125 : : * lit: A
126 : : * exp: B
127 : : * psb.d_steps: { A by (step id1 {B,C} {}), C by (step id2 {} {}) )
128 : : * In other words, A holds by a proof step with rule id1 and premises
129 : : * B and C, and C holds by proof step with rule id2 and no premises.
130 : : *
131 : : * @param lit The literal to assert to the equality engine.
132 : : * @param exp The premises of the proof steps concluding lit. These are also
133 : : * the premises that are used when calling explain(lit).
134 : : * @param psb The proof step buffer containing the proof steps.
135 : : * @return true if this fact was processed by this method. If lit already
136 : : * holds in the equality engine, this method returns false.
137 : : */
138 : : bool assertFact(Node lit, Node exp, ProofStepBuffer& psb);
139 : : /**
140 : : * Assert fact via generator pg. This method asserts lit with explanation exp
141 : : * to the equality engine of this class. It must be the case that pg can
142 : : * provide a proof for lit in terms of exp. More precisely, pg should be
143 : : * prepared in the remainder of the SAT context to respond to a call to
144 : : * ProofGenerator::getProofFor(lit), and return a proof whose free
145 : : * assumptions are a subset of the conjuncts of exp.
146 : : *
147 : : * @param lit The literal to assert to the equality engine.
148 : : * @param exp The premises of the proof concluding lit. These are also
149 : : * the premises that are used when calling explain(lit).
150 : : * @param pg The proof generator that can provide a proof concluding lit
151 : : * from free asumptions in exp.
152 : : * @return true if this fact was processed by this method. If lit already
153 : : * holds in the equality engine, this method returns false.
154 : : */
155 : : bool assertFact(Node lit, Node exp, ProofGenerator* pg);
156 : : //-------------------------- assert conflicts
157 : : /**
158 : : * This method is called when the equality engine of this class is
159 : : * inconsistent (false has been proven) by a contradictory literal lit. This
160 : : * returns the trust node corresponding to the current conflict.
161 : : *
162 : : * @param lit The conflicting literal, which must rewrite to false.
163 : : * @return The trust node capturing the fact that this class can provide a
164 : : * proof for this conflict.
165 : : */
166 : : TrustNode assertConflict(Node lit);
167 : : /**
168 : : * Get proven conflict from contradictory facts. This method is called when
169 : : * the proof rule with premises exp and arguments args implies a contradiction
170 : : * by proof rule id.
171 : : *
172 : : * This method returns the TrustNode containing the corresponding conflict
173 : : * resulting from adding this step, and ensures that a proof has been stored
174 : : * internally so that this class may respond to a call to
175 : : * ProofGenerator::getProof(...).
176 : : */
177 : : TrustNode assertConflict(ProofRule id,
178 : : const std::vector<Node>& exp,
179 : : const std::vector<Node>& args);
180 : : /** Generator version, where pg has a proof of false from assumptions exp */
181 : : TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg);
182 : : //-------------------------- assert lemma
183 : : /**
184 : : * Called when we have concluded conc, typically via theory specific
185 : : * reasoning. The purpose of this method is to construct a TrustNode of
186 : : * kind TrustNodeKind::LEMMA or TrustNodeKind::CONFLICT corresponding to the
187 : : * lemma or conflict to be sent on the output channel of the Theory.
188 : : *
189 : : * The user provides the explanation of conc in two parts:
190 : : * (1) (exp \ noExplain), which are literals that hold in the equality engine
191 : : * of this class,
192 : : * (2) noExplain, which do not necessarily hold in the equality engine of this
193 : : * class.
194 : : * Notice that noExplain is a subset of exp.
195 : : *
196 : : * The proof for conc follows from exp by proof rule with the given
197 : : * id and arguments.
198 : : *
199 : : * This call corresponds to a conflict if conc is false and noExplain is
200 : : * empty.
201 : : *
202 : : * This returns the TrustNode corresponding to the formula corresonding to
203 : : * the call to this method [*], for which a proof can be provided by this
204 : : * generator in the remainder of the user context.
205 : : *
206 : : * [*]
207 : : * a. If this call does not correspond to a conflict, then this formula is:
208 : : * ( ^_{e in exp \ noExplain} <explain>(e) ^ noExplain ) => conc
209 : : * where <explain>(e) is a conjunction of literals L1 ^ ... ^ Ln such that
210 : : * L1 ^ ... ^ Ln entail e, and each Li was passed as an explanation to a
211 : : * call to assertFact in the current SAT context. This explanation method
212 : : * always succeeds, provided that e is a literal that currently holds in
213 : : * the equality engine of this class. Notice that if the antecedant is empty,
214 : : * the formula above is assumed to be conc itself. The above formula is
215 : : * intended to be valid in Theory that owns this class.
216 : : * b. If this call is a conflict, then this formula is:
217 : : * ^_{e in exp} <explain>(e)
218 : : * The formula can be queried via TrustNode::getProven in the standard way.
219 : : */
220 : : TrustNode assertLemma(Node conc,
221 : : ProofRule id,
222 : : const std::vector<Node>& exp,
223 : : const std::vector<Node>& noExplain,
224 : : const std::vector<Node>& args);
225 : : /** Generator version, where pg has a proof of conc */
226 : : TrustNode assertLemma(Node conc,
227 : : const std::vector<Node>& exp,
228 : : const std::vector<Node>& noExplain,
229 : : ProofGenerator* pg);
230 : : //-------------------------- explain
231 : : /**
232 : : * Explain literal conc. This calls the appropriate methods in the underlying
233 : : * equality engine of this class to construct the explanation of why conc
234 : : * currently holds.
235 : : *
236 : : * It returns a trust node of kind TrustNodeKind::PROP_EXP whose node
237 : : * is the explanation of conc (a conjunction of literals that implies it).
238 : : * The proof that can be proven by this generator is then (=> exp conc), see
239 : : * TrustNode::getPropExpProven(conc,exp);
240 : : *
241 : : * @param conc The conclusion to explain
242 : : * @return The trust node indicating the explanation of conc and the generator
243 : : * (this class) that can prove the implication.
244 : : */
245 : : TrustNode explain(Node conc);
246 : :
247 : : private:
248 : : /** Assert internal */
249 : : bool assertFactInternal(TNode pred, bool polarity, TNode reason);
250 : : /** holds */
251 : : bool holds(TNode pred, bool polarity);
252 : : /**
253 : : * Ensure proof for fact. This is called by the above method after we have
254 : : * determined the final set of assumptions used for showing conc. This
255 : : * method is used for lemmas, conflicts, and explanations for propagations.
256 : : * The argument tnk is the kind of trust node to return.
257 : : */
258 : : TrustNode ensureProofForFact(Node conc,
259 : : const std::vector<TNode>& assumps,
260 : : TrustNodeKind tnk,
261 : : ProofGenerator* curr);
262 : : /**
263 : : * This ensures the proof of the literals that are in exp but not in
264 : : * noExplain have been added to curr. This additionally adds the
265 : : * explanation of exp to assumps. It updates tnk to LEMMA if there
266 : : * are any literals in exp that are not in noExplain.
267 : : */
268 : : void explainVecWithProof(TrustNodeKind& tnk,
269 : : std::vector<TNode>& assumps,
270 : : const std::vector<Node>& exp,
271 : : const std::vector<Node>& noExplain,
272 : : LazyCDProof* curr);
273 : : /** Explain
274 : : *
275 : : * This adds to assumps the set of facts that were asserted to this
276 : : * class in the current SAT context that are required for showing lit.
277 : : *
278 : : * This additionally registers the equality proof steps required to
279 : : * regress the explanation of lit in curr.
280 : : */
281 : : void explainWithProof(Node lit,
282 : : std::vector<TNode>& assumps,
283 : : LazyCDProof* curr);
284 : : /** Reference to the equality engine */
285 : : eq::EqualityEngine& d_ee;
286 : : /** The default proof generator (for simple facts) */
287 : : BufferedProofGenerator d_factPg;
288 : : /** The no-explain proof generator */
289 : : AssumptionProofGenerator d_assumpPg;
290 : : /** common nodes */
291 : : Node d_true;
292 : : Node d_false;
293 : : /** The SAT-context-dependent proof object */
294 : : LazyCDProof d_proof;
295 : : /**
296 : : * The keep set of this class. This set is maintained to ensure that
297 : : * facts and their explanations are reference counted. Since facts and their
298 : : * explanations are SAT-context-dependent, this set is also
299 : : * SAT-context-dependent.
300 : : */
301 : : NodeSet d_keep;
302 : : };
303 : :
304 : : } // namespace eq
305 : : } // namespace theory
306 : : } // namespace cvc5::internal
307 : :
308 : : #endif /* CVC5__THEORY__STRINGS__PROOF_MANAGER_H */
|
