1 /********************* */
2 /*! \file proof_equality_engine.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief The proof-producing equality engine
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
18 #define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
23 #include "context/cdhashmap.h"
24 #include "context/cdhashset.h"
25 #include "expr/lazy_proof.h"
26 #include "expr/node.h"
27 #include "expr/proof_node.h"
28 #include "expr/proof_node_manager.h"
29 #include "expr/proof_step_buffer.h"
30 #include "theory/eager_proof_generator.h"
31 #include "theory/uf/equality_engine.h"
38 * A layer on top of an EqualityEngine. The goal of this class is manage the
39 * use of an EqualityEngine object in such a way that the proper proofs are
40 * internally constructed, and can be retrieved from this class when
43 * Notice that this class is intended to be a *partial layer* on top of
44 * equality engine. A user of this class should still issue low-level calls
45 * (getRepresentative, areEqual, areDisequal, etc.) on the underlying equality
46 * engine directly. The methods that should *not* be called directly on the
47 * underlying equality engine are:
48 * - assertEquality/assertPredicate [*]
50 * Instead, the user should use variants of the above methods provided by
51 * the public interface of this class.
53 * [*] the exception is that assertions from the fact queue (who are their own
54 * explanation) should be sent directly to the underlying equality engine. This
55 * is for the sake of efficiency.
57 * This class tracks the reason for why all facts are added to an EqualityEngine
58 * in a SAT-context dependent manner in a context-dependent (CDProof) object.
59 * It furthermore maintains an internal FactProofGenerator class for managing
60 * proofs of facts whose steps are explicitly provided (those that are given
61 * concrete PfRule, children, and args). Call these "simple facts".
63 * Overall, this class is an eager proof generator (theory/proof_generator.h),
64 * in that it stores (copies) of proofs for lemmas at the moment they are sent
67 * A theory that is proof producing and uses the equality engine may use this
68 * class to manage proofs that are justified by its underlying equality engine.
69 * In particular, the following interfaces are available for constructing
71 * - assertConflict, when the user of the equality engine has discovered that
72 * false can be derived from the current state,
73 * - assertLemma, for lemmas/conflicts that can be (partially) explained in the
75 * - explain, for explaining why a literal is true in the current state.
76 * Details on these methods can be found below.
78 class ProofEqEngine
: public EagerProofGenerator
80 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
81 typedef context::CDHashMap
<Node
, std::shared_ptr
<ProofNode
>, NodeHashFunction
>
85 ProofEqEngine(context::Context
* c
,
86 context::UserContext
* u
,
88 ProofNodeManager
* pnm
);
90 //-------------------------- assert assumption
92 * Assert literal lit by assumption to the underlying equality engine. It is
93 * its own explanation.
95 * @param lit The literal to assert to the equality engine
96 * @return true if this fact was processed by this method. If lit already
97 * holds in the equality engine, this method returns false.
99 bool assertAssume(TNode lit
);
100 //-------------------------- assert fact
102 * Assert the literal lit by proof step id, given explanation exp and
103 * arguments args. This fact is
105 * @param lit The literal to assert to the equality engine
106 * @param id The proof rule of the proof step concluding lit
107 * @param exp The premises of the proof step concluding lit. These are also
108 * the premises that are used when calling explain(lit).
109 * @param args The arguments to the proof step concluding lit.
110 * @return true if this fact was processed by this method. If lit already
111 * holds in the equality engine, this method returns false.
113 bool assertFact(Node lit
,
115 const std::vector
<Node
>& exp
,
116 const std::vector
<Node
>& args
);
117 /** Same as above but where exp is (conjunctive) node */
118 bool assertFact(Node lit
, PfRule id
, Node exp
, const std::vector
<Node
>& args
);
120 * Multi-step version of assert fact via a proof step buffer. This method
121 * is similar to above, but the justification for lit may have multiple steps.
122 * In particular, we assume that psb has a list of proof steps where the
123 * proof step concluding lit has free assumptions exp.
125 * For example, a legal call to this method is such that:
128 * psb.d_steps: { A by (step id1 {B,C} {}), C by (step id2 {} {}) )
129 * In other words, A holds by a proof step with rule id1 and premises
130 * B and C, and C holds by proof step with rule id2 and no premises.
132 * @param lit The literal to assert to the equality engine.
133 * @param exp The premises of the proof steps concluding lit. These are also
134 * the premises that are used when calling explain(lit).
135 * @param psb The proof step buffer containing the proof steps.
136 * @return true if this fact was processed by this method. If lit already
137 * holds in the equality engine, this method returns false.
139 bool assertFact(Node lit
, Node exp
, ProofStepBuffer
& psb
);
141 * Assert fact via generator pg. This method asserts lit with explanation exp
142 * to the equality engine of this class. It must be the case that pg can
143 * provide a proof for lit in terms of exp. More precisely, pg should be
144 * prepared in the remainder of the SAT context to respond to a call to
145 * ProofGenerator::getProofFor(lit), and return a proof whose free
146 * assumptions are a subset of the conjuncts of exp.
148 * @param lit The literal to assert to the equality engine.
149 * @param exp The premises of the proof concluding lit. These are also
150 * the premises that are used when calling explain(lit).
151 * @param pg The proof generator that can provide a proof concluding lit
152 * from free asumptions in exp.
153 * @return true if this fact was processed by this method. If lit already
154 * holds in the equality engine, this method returns false.
156 bool assertFact(Node lit
, Node exp
, ProofGenerator
* pg
);
157 //-------------------------- assert conflicts
159 * This method is called when the equality engine of this class is
160 * inconsistent (false has been proven) by a contradictory literal lit. This
161 * returns the trust node corresponding to the current conflict.
163 * @param lit The conflicting literal, which must rewrite to false.
164 * @return The trust node capturing the fact that this class can provide a
165 * proof for this conflict.
167 TrustNode
assertConflict(Node lit
);
169 * Get proven conflict from contradictory facts. This method is called when
170 * the proof rule with premises exp and arguments args implies a contradiction
173 * This method returns the TrustNode containing the corresponding conflict
174 * resulting from adding this step, and ensures that a proof has been stored
175 * internally so that this class may respond to a call to
176 * ProofGenerator::getProof(...).
178 TrustNode
assertConflict(PfRule id
,
179 const std::vector
<Node
>& exp
,
180 const std::vector
<Node
>& args
);
181 /** Multi-step version */
182 TrustNode
assertConflict(const std::vector
<Node
>& exp
, ProofStepBuffer
& psb
);
183 //-------------------------- assert lemma
185 * Called when we have concluded conc, typically via theory specific
186 * reasoning. The purpose of this method is to construct a TrustNode of
187 * kind TrustNodeKind::LEMMA or TrustNodeKind::CONFLICT corresponding to the
188 * lemma or conflict to be sent on the output channel of the Theory.
190 * The user provides the explanation of conc in two parts:
191 * (1) (exp \ noExplain), which are literals that hold in the equality engine
193 * (2) noExplain, which do not necessarily hold in the equality engine of this
195 * Notice that noExplain is a subset of exp.
197 * The proof for conc follows from exp by proof rule with the given
200 * This call corresponds to a conflict if conc is false and noExplain is
203 * This returns the TrustNode corresponding to the formula corresonding to
204 * the call to this method [*], for which a proof can be provided by this
205 * generator in the remainder of the user context.
208 * a. If this call does not correspond to a conflict, then this formula is:
209 * ( ^_{e in exp \ noExplain} <explain>(e) ^ noExplain ) => conc
210 * where <explain>(e) is a conjunction of literals L1 ^ ... ^ Ln such that
211 * L1 ^ ... ^ Ln entail e, and each Li was passed as an explanation to a
212 * call to assertFact in the current SAT context. This explanation method
213 * always succeeds, provided that e is a literal that currently holds in
214 * the equality engine of this class. Notice that if the antecedant is empty,
215 * the formula above is assumed to be conc itself. The above formula is
216 * intended to be valid in Theory that owns this class.
217 * b. If this call is a conflict, then this formula is:
218 * ^_{e in exp} <explain>(e)
219 * The formula can be queried via TrustNode::getProven in the standard way.
221 TrustNode
assertLemma(Node conc
,
223 const std::vector
<Node
>& exp
,
224 const std::vector
<Node
>& noExplain
,
225 const std::vector
<Node
>& args
);
226 /** Multi-step version */
227 TrustNode
assertLemma(Node conc
,
228 const std::vector
<Node
>& exp
,
229 const std::vector
<Node
>& noExplain
,
230 ProofStepBuffer
& psb
);
231 /** Generator version, where pg has a proof of conc */
232 TrustNode
assertLemma(Node conc
,
233 const std::vector
<Node
>& exp
,
234 const std::vector
<Node
>& noExplain
,
236 //-------------------------- explain
238 * Explain literal conc. This calls the appropriate methods in the underlying
239 * equality engine of this class to construct the explanation of why conc
242 * It returns a trust node of kind TrustNodeKind::PROP_EXP whose node
243 * is the explanation of conc (a conjunction of literals that implies it).
244 * The proof that can be proven by this generator is then (=> exp conc), see
245 * TrustNode::getPropExpProven(conc,exp);
247 * @param conc The conclusion to explain
248 * @return The trust node indicating the explanation of conc and the generator
249 * (this class) that can prove the implication.
251 TrustNode
explain(Node conc
);
255 * The default proof generator (for simple facts). This class is a context
256 * dependent mapping from formulas to proof steps. It does not generate
257 * ProofNode until it is asked to provide a proof for a given fact.
259 class FactProofGenerator
: public ProofGenerator
262 CDHashMap
<Node
, std::shared_ptr
<ProofStep
>, NodeHashFunction
>
266 FactProofGenerator(context::Context
* c
, ProofNodeManager
* pnm
);
267 ~FactProofGenerator() {}
269 bool addStep(Node fact
, ProofStep ps
);
271 std::shared_ptr
<ProofNode
> getProofFor(Node f
) override
;
273 std::string
identify() const override
{ return "FactProofGenerator"; }
276 /** maps expected to ProofStep */
277 NodeProofStepMap d_facts
;
278 /** the proof node manager */
279 ProofNodeManager
* d_pnm
;
281 /** Assert internal */
282 bool assertFactInternal(TNode pred
, bool polarity
, TNode reason
);
284 bool holds(TNode pred
, bool polarity
);
286 * Assert lemma internal. This method is called for ensuring the proof of
287 * conc exists in curr, where exp / noExplain are the its explanation (see
288 * assertLemma). This method is used for conflicts as well, where noExplain
289 * must be empty and conc = d_false.
291 * If curr is null, no proof is constructed.
293 * This method returns the trust node of the lemma or conflict with this
294 * class as the proof generator.
296 TrustNode
assertLemmaInternal(Node conc
,
297 const std::vector
<Node
>& exp
,
298 const std::vector
<Node
>& noExplain
,
301 * Ensure proof for fact. This is called by the above method after we have
302 * determined the final set of assumptions used for showing conc. This
303 * method is used for lemmas, conflicts, and explanations for propagations.
304 * The argument tnk is the kind of trust node to return.
306 TrustNode
ensureProofForFact(Node conc
,
307 const std::vector
<TNode
>& assumps
,
311 * Make the conjunction of nodes in a. Returns true if a is empty, and a
312 * single literal if a has size 1.
314 Node
mkAnd(const std::vector
<Node
>& a
);
315 Node
mkAnd(const std::vector
<TNode
>& a
);
316 /** Reference to the equality engine */
317 eq::EqualityEngine
& d_ee
;
318 /** The default proof generator (for simple facts) */
319 FactProofGenerator d_factPg
;
323 /** the proof node manager */
324 ProofNodeManager
* d_pnm
;
325 /** The SAT-context-dependent proof object */
328 * The keep set of this class. This set is maintained to ensure that
329 * facts and their explanations are reference counted. Since facts and their
330 * explanations are SAT-context-dependent, this set is also
331 * SAT-context-dependent.
335 * Whether proofs are enabled. If this flag is false, then this class acts
336 * as a simplified interface to the EqualityEngine, without proofs.
341 * This adds to assumps the set of facts that were asserted to this
342 * class in the current SAT context by calls to assertAssume that are
343 * required for showing lit.
345 * This additionally registers the equality proof steps required to
346 * regress the explanation of lit.
348 void explainWithProof(Node lit
,
349 std::vector
<TNode
>& assumps
,
354 } // namespace theory
357 #endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */