1 

/********************* */ 
2 

/*! \file proof_equality_engine.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Haniel Barbosa 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief The proofproducing equality engine 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H 
18 

#define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H 
19 


20 

#include <vector> 
21 


22 

#include "context/cdhashmap.h" 
23 

#include "context/cdhashset.h" 
24 

#include "expr/buffered_proof_generator.h" 
25 

#include "expr/lazy_proof.h" 
26 

#include "expr/node.h" 
27 

#include "theory/eager_proof_generator.h" 
28 


29 

namespace CVC4 { 
30 


31 

class ProofNode; 
32 

class ProofNodeManager; 
33 


34 

namespace theory { 
35 

namespace eq { 
36 


37 

class EqualityEngine; 
38 


39 

/** 
40 

* A layer on top of an EqualityEngine. The goal of this class is manage the 
41 

* use of an EqualityEngine object in such a way that the proper proofs are 
42 

* internally constructed, and can be retrieved from this class when 
43 

* necessary. 
44 

* 
45 

* Notice that this class is intended to be a *partial layer* on top of 
46 

* equality engine. A user of this class should still issue lowlevel calls 
47 

* (getRepresentative, areEqual, areDisequal, etc.) on the underlying equality 
48 

* engine directly. The methods that should *not* be called directly on the 
49 

* underlying equality engine are: 
50 

*  assertEquality/assertPredicate [*] 
51 

*  explain 
52 

* Instead, the user should use variants of the above methods provided by 
53 

* the public interface of this class. 
54 

* 
55 

* [*] the exception is that assertions from the fact queue (who are their own 
56 

* explanation) should be sent directly to the underlying equality engine. This 
57 

* is for the sake of efficiency. 
58 

* 
59 

* This class tracks the reason for why all facts are added to an EqualityEngine 
60 

* in a SATcontext dependent manner in a contextdependent (CDProof) object. 
61 

* It furthermore maintains an internal FactProofGenerator class for managing 
62 

* proofs of facts whose steps are explicitly provided (those that are given 
63 

* concrete PfRule, children, and args). Call these "simple facts". 
64 

* 
65 

* Overall, this class is an eager proof generator (theory/proof_generator.h), 
66 

* in that it stores (copies) of proofs for lemmas at the moment they are sent 
67 

* out. 
68 

* 
69 

* A theory that is proof producing and uses the equality engine may use this 
70 

* class to manage proofs that are justified by its underlying equality engine. 
71 

* In particular, the following interfaces are available for constructing 
72 

* a TrustNode: 
73 

*  assertConflict, when the user of the equality engine has discovered that 
74 

* false can be derived from the current state, 
75 

*  assertLemma, for lemmas/conflicts that can be (partially) explained in the 
76 

* current state, 
77 

*  explain, for explaining why a literal is true in the current state. 
78 

* Details on these methods can be found below. 
79 

*/ 
80 

class ProofEqEngine : public EagerProofGenerator 
81 

{ 
82 

typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 
83 

typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction> 
84 

NodeProofMap; 
85 


86 

public: 
87 

ProofEqEngine(context::Context* c, 
88 

context::UserContext* u, 
89 

EqualityEngine& ee, 
90 

ProofNodeManager* pnm); 
91 
14330 
~ProofEqEngine() {} 
92 

// assert fact 
93 

/** 
94 

* Assert the literal lit by proof step id, given explanation exp and 
95 

* arguments args. This fact is 
96 

* 
97 

* @param lit The literal to assert to the equality engine 
98 

* @param id The proof rule of the proof step concluding lit 
99 

* @param exp The premises of the proof step concluding lit. These are also 
100 

* the premises that are used when calling explain(lit). 
101 

* @param args The arguments to the proof step concluding lit. 
102 

* @return true if this fact was processed by this method. If lit already 
103 

* holds in the equality engine, this method returns false. 
104 

*/ 
105 

bool assertFact(Node lit, 
106 

PfRule id, 
107 

const std::vector<Node>& exp, 
108 

const std::vector<Node>& args); 
109 

/** Same as above but where exp is (conjunctive) node */ 
110 

bool assertFact(Node lit, PfRule id, Node exp, const std::vector<Node>& args); 
111 

/** 
112 

* Multistep version of assert fact via a proof step buffer. This method 
113 

* is similar to above, but the justification for lit may have multiple steps. 
114 

* In particular, we assume that psb has a list of proof steps where the 
115 

* proof step concluding lit has free assumptions exp. 
116 

* 
117 

* For example, a legal call to this method is such that: 
118 

* lit: A 
119 

* exp: B 
120 

* psb.d_steps: { A by (step id1 {B,C} {}), C by (step id2 {} {}) ) 
121 

* In other words, A holds by a proof step with rule id1 and premises 
122 

* B and C, and C holds by proof step with rule id2 and no premises. 
123 

* 
124 

* @param lit The literal to assert to the equality engine. 
125 

* @param exp The premises of the proof steps concluding lit. These are also 
126 

* the premises that are used when calling explain(lit). 
127 

* @param psb The proof step buffer containing the proof steps. 
128 

* @return true if this fact was processed by this method. If lit already 
129 

* holds in the equality engine, this method returns false. 
130 

*/ 
131 

bool assertFact(Node lit, Node exp, ProofStepBuffer& psb); 
132 

/** 
133 

* Assert fact via generator pg. This method asserts lit with explanation exp 
134 

* to the equality engine of this class. It must be the case that pg can 
135 

* provide a proof for lit in terms of exp. More precisely, pg should be 
136 

* prepared in the remainder of the SAT context to respond to a call to 
137 

* ProofGenerator::getProofFor(lit), and return a proof whose free 
138 

* assumptions are a subset of the conjuncts of exp. 
139 

* 
140 

* @param lit The literal to assert to the equality engine. 
141 

* @param exp The premises of the proof concluding lit. These are also 
142 

* the premises that are used when calling explain(lit). 
143 

* @param pg The proof generator that can provide a proof concluding lit 
144 

* from free asumptions in exp. 
145 

* @return true if this fact was processed by this method. If lit already 
146 

* holds in the equality engine, this method returns false. 
147 

*/ 
148 

bool assertFact(Node lit, Node exp, ProofGenerator* pg); 
149 

// assert conflicts 
150 

/** 
151 

* This method is called when the equality engine of this class is 
152 

* inconsistent (false has been proven) by a contradictory literal lit. This 
153 

* returns the trust node corresponding to the current conflict. 
154 

* 
155 

* @param lit The conflicting literal, which must rewrite to false. 
156 

* @return The trust node capturing the fact that this class can provide a 
157 

* proof for this conflict. 
158 

*/ 
159 

TrustNode assertConflict(Node lit); 
160 

/** 
161 

* Get proven conflict from contradictory facts. This method is called when 
162 

* the proof rule with premises exp and arguments args implies a contradiction 
163 

* by proof rule id. 
164 

* 
165 

* This method returns the TrustNode containing the corresponding conflict 
166 

* resulting from adding this step, and ensures that a proof has been stored 
167 

* internally so that this class may respond to a call to 
168 

* ProofGenerator::getProof(...). 
169 

*/ 
170 

TrustNode assertConflict(PfRule id, 
171 

const std::vector<Node>& exp, 
172 

const std::vector<Node>& args); 
173 

/** Generator version, where pg has a proof of false from assumptions exp */ 
174 

TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg); 
175 

// assert lemma 
176 

/** 
177 

* Called when we have concluded conc, typically via theory specific 
178 

* reasoning. The purpose of this method is to construct a TrustNode of 
179 

* kind TrustNodeKind::LEMMA or TrustNodeKind::CONFLICT corresponding to the 
180 

* lemma or conflict to be sent on the output channel of the Theory. 
181 

* 
182 

* The user provides the explanation of conc in two parts: 
183 

* (1) (exp \ noExplain), which are literals that hold in the equality engine 
184 

* of this class, 
185 

* (2) noExplain, which do not necessarily hold in the equality engine of this 
186 

* class. 
187 

* Notice that noExplain is a subset of exp. 
188 

* 
189 

* The proof for conc follows from exp by proof rule with the given 
190 

* id and arguments. 
191 

* 
192 

* This call corresponds to a conflict if conc is false and noExplain is 
193 

* empty. 
194 

* 
195 

* This returns the TrustNode corresponding to the formula corresonding to 
196 

* the call to this method [*], for which a proof can be provided by this 
197 

* generator in the remainder of the user context. 
198 

* 
199 

* [*] 
200 

* a. If this call does not correspond to a conflict, then this formula is: 
201 

* ( ^_{e in exp \ noExplain} <explain>(e) ^ noExplain ) => conc 
202 

* where <explain>(e) is a conjunction of literals L1 ^ ... ^ Ln such that 
203 

* L1 ^ ... ^ Ln entail e, and each Li was passed as an explanation to a 
204 

* call to assertFact in the current SAT context. This explanation method 
205 

* always succeeds, provided that e is a literal that currently holds in 
206 

* the equality engine of this class. Notice that if the antecedant is empty, 
207 

* the formula above is assumed to be conc itself. The above formula is 
208 

* intended to be valid in Theory that owns this class. 
209 

* b. If this call is a conflict, then this formula is: 
210 

* ^_{e in exp} <explain>(e) 
211 

* The formula can be queried via TrustNode::getProven in the standard way. 
212 

*/ 
213 

TrustNode assertLemma(Node conc, 
214 

PfRule id, 
215 

const std::vector<Node>& exp, 
216 

const std::vector<Node>& noExplain, 
217 

const std::vector<Node>& args); 
218 

/** Generator version, where pg has a proof of conc */ 
219 

TrustNode assertLemma(Node conc, 
220 

const std::vector<Node>& exp, 
221 

const std::vector<Node>& noExplain, 
222 

ProofGenerator* pg); 
223 

// explain 
224 

/** 
225 

* Explain literal conc. This calls the appropriate methods in the underlying 
226 

* equality engine of this class to construct the explanation of why conc 
227 

* currently holds. 
228 

* 
229 

* It returns a trust node of kind TrustNodeKind::PROP_EXP whose node 
230 

* is the explanation of conc (a conjunction of literals that implies it). 
231 

* The proof that can be proven by this generator is then (=> exp conc), see 
232 

* TrustNode::getPropExpProven(conc,exp); 
233 

* 
234 

* @param conc The conclusion to explain 
235 

* @return The trust node indicating the explanation of conc and the generator 
236 

* (this class) that can prove the implication. 
237 

*/ 
238 

TrustNode explain(Node conc); 
239 


240 

private: 
241 

/** Assert internal */ 
242 

bool assertFactInternal(TNode pred, bool polarity, TNode reason); 
243 

/** holds */ 
244 

bool holds(TNode pred, bool polarity); 
245 

/** 
246 

* Ensure proof for fact. This is called by the above method after we have 
247 

* determined the final set of assumptions used for showing conc. This 
248 

* method is used for lemmas, conflicts, and explanations for propagations. 
249 

* The argument tnk is the kind of trust node to return. 
250 

*/ 
251 

TrustNode ensureProofForFact(Node conc, 
252 

const std::vector<TNode>& assumps, 
253 

TrustNodeKind tnk, 
254 

ProofGenerator* curr); 
255 

/** 
256 

* This ensures the proof of the literals that are in exp but not in 
257 

* noExplain have been added to curr. This additionally adds the 
258 

* explanation of exp to assumps. It updates tnk to LEMMA if there 
259 

* are any literals in exp that are not in noExplain. 
260 

*/ 
261 

void explainVecWithProof(TrustNodeKind& tnk, 
262 

std::vector<TNode>& assumps, 
263 

const std::vector<Node>& exp, 
264 

const std::vector<Node>& noExplain, 
265 

LazyCDProof* curr); 
266 

/** Explain 
267 

* 
268 

* This adds to assumps the set of facts that were asserted to this 
269 

* class in the current SAT context that are required for showing lit. 
270 

* 
271 

* This additionally registers the equality proof steps required to 
272 

* regress the explanation of lit in curr. 
273 

*/ 
274 

void explainWithProof(Node lit, 
275 

std::vector<TNode>& assumps, 
276 

LazyCDProof* curr); 
277 

/** Reference to the equality engine */ 
278 

eq::EqualityEngine& d_ee; 
279 

/** The default proof generator (for simple facts) */ 
280 

BufferedProofGenerator d_factPg; 
281 

/** common nodes */ 
282 

Node d_true; 
283 

Node d_false; 
284 

/** the proof node manager */ 
285 

ProofNodeManager* d_pnm; 
286 

/** The SATcontextdependent proof object */ 
287 

LazyCDProof d_proof; 
288 

/** 
289 

* The keep set of this class. This set is maintained to ensure that 
290 

* facts and their explanations are reference counted. Since facts and their 
291 

* explanations are SATcontextdependent, this set is also 
292 

* SATcontextdependent. 
293 

*/ 
294 

NodeSet d_keep; 
295 

}; 
296 


297 

} // namespace eq 
298 

} // namespace theory 
299 

} // namespace CVC4 
300 


301 

#endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */ 