1 

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

/*! \file eq_proof.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Haniel Barbosa, Dejan Jovanovic, Morgan Deters 
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 A proof as produced by the equality engine. 
13 

** 
14 

**/ 
15 


16 

#include "cvc4_private.h" 
17 

#include "expr/node.h" 
18 

#include "theory/uf/equality_engine_types.h" 
19 


20 

namespace CVC4 { 
21 


22 

class CDProof; 
23 


24 

namespace theory { 
25 

namespace eq { 
26 


27 

/** 
28 

* An equality proof. 
29 

* 
30 

* This represents the reasoning performed by the Equality Engine to derive 
31 

* facts, represented in terms of the rules in MergeReasonType. Each proof step 
32 

* is annotated with the rule id, the conclusion node and a vector of proofs of 
33 

* the rule's premises. 
34 

**/ 
35 
2652818 
class EqProof 
36 

{ 
37 

public: 
38 
2508493 
EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY) {} 
39 

/** The proof rule for concluding d_node */ 
40 

MergeReasonType d_id; 
41 

/** The conclusion of this EqProof */ 
42 

Node d_node; 
43 

/** The proofs of the premises for deriving d_node with d_id */ 
44 

std::vector<std::shared_ptr<EqProof>> d_children; 
45 

/** 
46 

* Debug print this proof on debug trace c with tabulation tb. 
47 

*/ 
48 

void debug_print(const char* c, unsigned tb = 0) const; 
49 

/** 
50 

* Debug print this proof on output stream os with tabulation tb. 
51 

*/ 
52 

void debug_print(std::ostream& os, unsigned tb = 0) const; 
53 


54 

/** Add to proof 
55 

* 
56 

* Converts EqProof into ProofNode via a series of steps to be stored in 
57 

* CDProof* p. 
58 

* 
59 

* This method can be seen as a besteffort solution until the EqualityEngine 
60 

* is updated to produce ProofNodes directly, if ever. Note that since the 
61 

* original EqProof steps can be coarsegrained (e.g. without proper order, 
62 

* implicit inferences related to disequelaties) and are phrased over curried 
63 

* terms, the transformation requires significant, although cheap (mostly 
64 

* linear on the DAGsize of EqProof), postprocessing. 
65 

* 
66 

* An important invariant of the resulting ProofNode is that neither its 
67 

* assumptions nor its conclusion are predicate equalities, i.e. of the form 
68 

* (= t true/false), modulo symmetry. This is so that users of the converted 
69 

* ProofNode don't need to do case analysis on whether assumptions/conclusion 
70 

* are either t or (= t true/false). 
71 

* 
72 

* @param p a pointer to a CDProof to store the conversion of this EqProof 
73 

* @return the node that is the conclusion of the proof as added to p. 
74 

*/ 
75 

Node addToProof(CDProof* p) const; 
76 


77 

private: 
78 

/** 
79 

* As above, but with a cache of previously processed nodes and their results 
80 

* (for DAG traversal). The caching is in terms of the original conclusions of 
81 

* EqProof. 
82 

* 
83 

* @param p a pointer to a CDProof to store the conversion of this EqProof 
84 

* @param visited a cache of the original EqProof conclusions and the 
85 

* resulting conclusion after conversion. 
86 

* @param assumptions the assumptions of the original EqProof (and their 
87 

* variations in terms of symmetry and conversion to/from predicate 
88 

* equalities) 
89 

* @return the node that is the conclusion of the proof as added to p. 
90 

*/ 
91 

Node addToProof( 
92 

CDProof* p, 
93 

std::unordered_map<Node, Node, NodeHashFunction>& visited, 
94 

std::unordered_set<Node, NodeHashFunction>& assumptions) const; 
95 


96 

/** Removes all reflexivity steps, i.e. (= t t), from premises. */ 
97 

void cleanReflPremises(std::vector<Node>& premises) const; 
98 


99 

/** Expand coarsegrained transitivity steps for disequalities 
100 

* 
101 

* Currently the equality engine can represent disequality reasoning in a 
102 

* rather coarsegrained manner with EqProof. This is always the case when the 
103 

* transitivity step contains a disequality, (= (= t t') false) or its 
104 

* symmetric, as a premise. 
105 

* 
106 

* There are two cases. In the simplest one the general shape of the EqProof 
107 

* is 
108 

* (= t1 t2) (= t3 t2) (= (t1 t3) false) 
109 

*  EQP::TR 
110 

* false = true 
111 

* 
112 

* which is expanded into 
113 

* (= t3 t2) 
114 

*  SYMM 
115 

* (= t1 t2) (= t2 t3) 
116 

*  TRANS 
117 

* (= (= t1 t3) false) (= t1 t3) 
118 

*  SYMM  TRUE_INTRO 
119 

* (= false (= t1 t3)) (= (= t1 t3) true) 
120 

*  TRANS 
121 

* false = true 
122 

* 
123 

* by explicitly adding the transitivity step for inferring (= t1 t3) and its 
124 

* predicate equality. Note that we differentiate (from now on) the EqProof 
125 

* rules ids from those of ProofRule by adding the prefix EQP:: to the former. 
126 

* 
127 

* In the other case, the general shape of the EqProof is 
128 

* 
129 

* (= (= t1 t2) false) (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4) 
130 

*  EQP::TR 
131 

* (= (= t4 t3) false) 
132 

* 
133 

* which is converted into 
134 

* 
135 

* (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4) 
136 

*  TR  TR 
137 

* (= t1 t3) (= t2 t4) 
138 

*  SYMM  SYMM 
139 

* (= t3 t1) (= t4 t2) 
140 

*  CONG 
141 

* (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false) 
142 

*  TR 
143 

* (= (= t3 t4) false) 
144 

*  MACRO_SR_PRED_TRANSFORM 
145 

* (= (= t4 t3) false) 
146 

* 
147 

* whereas the last step is only necessary if the conclusion has the arguments 
148 

* in reverse order than expected. Note that the original step represents two 
149 

* substitutions happening on the disequality, from t1>t3 and t2>t4, which 
150 

* are implicitly justified by transitivity steps that need to be made 
151 

* explicity. Since there is no sense of ordering among which premisis (other 
152 

* than (= (= t1 t2) false)) are used for which substitution, the transitivity 
153 

* proofs are built greedly by searching the sets of premises. 
154 

* 
155 

* If in either of the above cases then the conclusion is directly derived 
156 

* in the call, so only in the other cases we try to build a transitivity 
157 

* step below 
158 

* 
159 

* @param conclusion the conclusion of the (possibly) coarsegrained 
160 

* transitivity step 
161 

* @param premises the premises of the (possibly) coarsegrained 
162 

* transitivity step 
163 

* @param p a pointer to a CDProof to store the conversion of this EqProof 
164 

* @param assumptions the assumptions (and variants) of the original 
165 

* EqProof. These are necessary to avoid cyclic proofs, which could be 
166 

* generated by creating transitivity steps for assumptions (which depend on 
167 

* themselves). 
168 

* @return True if the EqProof transitivity step is in either of the above 
169 

* cases, symbolizing that the ProofNode justifying the conclusion has already 
170 

* been produced. 
171 

*/ 
172 

bool expandTransitivityForDisequalities( 
173 

Node conclusion, 
174 

std::vector<Node>& premises, 
175 

CDProof* p, 
176 

std::unordered_set<Node, NodeHashFunction>& assumptions) const; 
177 


178 

/** Expand coarsegrained transitivity steps for theory disequalities 
179 

* 
180 

* Currently the equality engine can represent disequality reasoning of theory 
181 

* symbols in a rather coarsegrained manner with EqProof. This is the case 
182 

* when EqProof is 
183 

* (= t1 c1) (= t2 c2) 
184 

*  EQP::TR 
185 

* (= (t1 t2) false) 
186 

* 
187 

* which is converted into 
188 

* 
189 

* (= t1 c1) (= t2 c2) 
190 

*  CONG  MACRO_SR_PRED_INTRO 
191 

* (= (= t1 t2) (= c1 t2)) (= (= c1 c2) false) 
192 

*  TR 
193 

* (= (= t1 t2) false) 
194 

* 
195 

* @param conclusion the conclusion of the (possibly) coarsegrained 
196 

* transitivity step 
197 

* @param premises the premises of the (possibly) coarsegrained 
198 

* transitivity step 
199 

* @param p a pointer to a CDProof to store the conversion of this EqProof 
200 

* @return True if the EqProof transitivity step is the above case, 
201 

* indicating that the ProofNode justifying the conclusion has already been 
202 

* produced. 
203 

*/ 
204 

bool expandTransitivityForTheoryDisequalities(Node conclusion, 
205 

std::vector<Node>& premises, 
206 

CDProof* p) const; 
207 


208 

/** Builds a transitivity chain from equalities to derive a conclusion 
209 

* 
210 

* Given an equality (= t1 tn), and a list of equalities premises, attempts to 
211 

* build a chain (= t1 t2) ... (= tn1 tn) from premises. This is done in a 
212 

* greedy manner by finding one "link" in the chain at a time, updating the 
213 

* conclusion to be the next link and the premises by removing the used 
214 

* premise, and searching recursively. 
215 

* 
216 

* Consider for example 
217 

*  conclusion: (= t1 t4) 
218 

*  premises: (= t4 t2), (= t2 t3), (= t2 t1), (= t3 t4) 
219 

* 
220 

* It proceeds by searching for t1 in an equality in the premises, in order, 
221 

* which is found in the equality (= t2 t1). Since t2 != t4, it attempts to 
222 

* build a chain with 
223 

*  conclusion (= t2 t4) 
224 

*  premises (= t4 t2), (= t2 t3), (= t3 t4) 
225 

* 
226 

* In the first equality it finds t2 and also t4, which closes the chain, so 
227 

* that premises is updated to (= t2 t4) and the method returns true. Since 
228 

* the recursive call was successful, the original conclusion (= t1 t4) is 
229 

* justified with (= t1 t2) plus the chain built in the recursive call, 
230 

* i.e. (= t1 t2), (= t2 t4). 
231 

* 
232 

* Note that not all the premises were necessary to build a successful 
233 

* chain. Moreover, note that building a successful chain can depend on the 
234 

* order in which the equalities are chosen. When a recursive call fails to 
235 

* close a chain, the chosen equality is dismissed and another is searched for 
236 

* among the remaining ones. 
237 

* 
238 

* This method assumes that premises does not contain reflexivity premises. 
239 

* This is without loss of generality since such premises are spurious for a 
240 

* transitivity step. 
241 

* 
242 

* @param conclusion the conclusion of the transitivity chain of equalities 
243 

* @param premises the list of equalities to build a chain with 
244 

* @return whether premises successfully build a transitivity chain for the 
245 

* conclusion 
246 

*/ 
247 

bool buildTransitivityChain(Node conclusion, 
248 

std::vector<Node>& premises) const; 
249 


250 

/** Reduce the a congruence EqProof into a transitivity matrix 
251 

* 
252 

* Given a congruence EqProof of (= (f a0 ... an1) (f b0 ... bn1)), reduce 
253 

* its justification into a matrix 
254 

* 
255 

* [0] > p_{0,0} ... p_{m_0,0} 
256 

* ... 
257 

* [n1] > p_{0,n} ... p_{m_n1,n1} 
258 

* 
259 

* where f has arity n and each p_{0,i} ... p_{m_i, i} is a transitivity chain 
260 

* (modulo ordering) justifying (= ai bi). 
261 

* 
262 

* Congruence steps in EqProof are binary, representing reasoning over curried 
263 

* applications. In the simplest case the general shape of a congruence 
264 

* EqProof is: 
265 

* P0 
266 

*  EQP::REFL  
267 

* P1 [] (= a0 b0) 
268 

*   EQP::CONG 
269 

* (= a1 b1) [] P2 
270 

*  EQP::CONG  
271 

* [] (= a2 b2) 
272 

*  EQP::CONG 
273 

* (= (f a0 a1 a2) (f b0 b1 b2)) 
274 

* 
275 

* where [] stands for the null node, symbolizing "equality between partial 
276 

* applications". 
277 

* 
278 

* The reduction of such a proof is done by 
279 

*  converting the proof of the second CONG premise (via addToProof) and 
280 

* adding the resulting node to row i of the matrix 
281 

*  recursively reducing the first proof with i1 
282 

* 
283 

* In the above case the transitivity matrix would thus be 
284 

* [0] > (= a0 b0) 
285 

* [1] > (= a1 b1) 
286 

* [2] > (= a2 b2) 
287 

* 
288 

* The more complex case of congruence proofs has transitivity steps as the 
289 

* first child of CONG steps. For example 
290 

* P0 
291 

*  EQP::REFL  
292 

* P' [] (= a0 c) 
293 

*   EQP::CONG 
294 

* (= b0 c) [] P1 
295 

*  EQP::TRANS  
296 

* [] (= a1 b1) 
297 

*  EQP::CONG 
298 

* (= (f a0 a1) (f b0 b1)) 
299 

* 
300 

* where when the first child of CONG is a transitivity step 
301 

*  the premises that are CONG steps are recursively reduced with *the same* 
302 

argument i 
303 

*  the other premises are processed with addToProof and added to the i row 
304 

* in the matrix 
305 

* 
306 

* In the above example the to which the transitivity matrix is 
307 

* [0] > (= a0 c), (= b0 c) 
308 

* [1] > (= a1 b1) 
309 

* 
310 

* The remaining complication is that when conclusion is an equality of nary 
311 

* applications of *different* arities, there is, necessarily, a transitivity 
312 

* step as a first child a CONG step whose conclusion is an equality of nary 
313 

* applications of different arities. For example 
314 

* P0 P1 
315 

*  EQP::TRANS  
316 

* (= (f a0 a1) (f b0)) (= a2 b1) 
317 

*  EQP::CONG 
318 

* (= (f a0 a1 a2) (f b0 b1)) 
319 

* 
320 

* will be first reduced with i = 2 (maximal arity amorg the original 
321 

* conclusion's applications), adding (= a2 b1) to row 2 after processing 
322 

* P1. The first child is reduced with i = 1. Since it is a TRANS step whose 
323 

* conclusion is an equality of nary applications with mismatching arity, P0 
324 

* is processed with addToProof and the result is added to row 1. Thus the 
325 

* transitivity matrix is 
326 

* [0] > 
327 

* [1] > (= (f a0 a1) (f b0)) 
328 

* [2] > (= a2 b1) 
329 

* 
330 

* The empty row 0 is used by the original caller of reduceNestedCongruence to 
331 

* compute that the above congruence proof's conclusion is 
332 

* (= (f (f a0 a1) a2) (f (f b0) b1)) 
333 

* 
334 

* @param i the ith argument of the congruent applications, initially being 
335 

* the maximal arity among conclusion's applications. 
336 

* @param conclusion the original congruence conclusion 
337 

* @param transitivityMatrix a matrix of equalities with each row justifying 
338 

* an equality between the congruent applications 
339 

* @param p a pointer to a CDProof to store the conversion of this EqProof 
340 

* @param visited a cache of the original EqProof conclusions and the 
341 

* resulting conclusion after conversion. 
342 

* @param assumptions the assumptions (and variants) of the original EqProof 
343 

* @param isNary whether conclusion is an equality of nary applications 
344 

*/ 
345 

void reduceNestedCongruence( 
346 

unsigned i, 
347 

Node conclusion, 
348 

std::vector<std::vector<Node>>& transitivityMatrix, 
349 

CDProof* p, 
350 

std::unordered_map<Node, Node, NodeHashFunction>& visited, 
351 

std::unordered_set<Node, NodeHashFunction>& assumptions, 
352 

bool isNary) const; 
353 


354 

}; /* class EqProof */ 
355 


356 

} // Namespace eq 
357 

} // Namespace theory 
358 

} // Namespace CVC4 