Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Mathias Preiner
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 : : * A proof as produced by the equality engine.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : : #include "expr/node.h"
18 : : #include "theory/uf/equality_engine_types.h"
19 : :
20 : : namespace cvc5::internal {
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 : : class EqProof
36 : : {
37 : : public:
38 : 7408740 : 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 best-effort solution until the EqualityEngine
60 : : * is updated to produce ProofNodes directly, if ever. Note that since the
61 : : * original EqProof steps can be coarse-grained (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 DAG-size of EqProof), post-processing.
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(CDProof* p,
92 : : std::unordered_map<Node, Node>& visited,
93 : : std::unordered_set<Node>& assumptions) const;
94 : :
95 : : /** Removes all reflexivity steps, i.e. (= t t), from premises. */
96 : : void cleanReflPremises(std::vector<Node>& premises) const;
97 : :
98 : : /** Expand coarse-grained transitivity steps for disequalities
99 : : *
100 : : * Currently the equality engine can represent disequality reasoning in a
101 : : * rather coarse-grained manner with EqProof. This is always the case when the
102 : : * transitivity step contains a disequality, (= (= t t') false) or its
103 : : * symmetric, as a premise.
104 : : *
105 : : * There are two cases. In the simplest one the general shape of the EqProof
106 : : * is
107 : : * (= t1 t2) (= t3 t2) (= (t1 t3) false)
108 : : * ------------------------------------- EQP::TR
109 : : * false = true
110 : : *
111 : : * which is expanded into
112 : : * (= t3 t2)
113 : : * --------- SYMM
114 : : * (= t1 t2) (= t2 t3)
115 : : * ------------------- TRANS
116 : : * (= (= t1 t3) false) (= t1 t3)
117 : : * --------------------- SYMM ------------------ TRUE_INTRO
118 : : * (= false (= t1 t3)) (= (= t1 t3) true)
119 : : * ----------------------------------------------- TRANS
120 : : * false = true
121 : : *
122 : : * by explicitly adding the transitivity step for inferring (= t1 t3) and its
123 : : * predicate equality. Note that we differentiate (from now on) the EqProof
124 : : * rules ids from those of ProofRule by adding the prefix EQP:: to the former.
125 : : *
126 : : * In the other case, the general shape of the EqProof is
127 : : *
128 : : * (= (= t1 t2) false) (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
129 : : * ------------------------------------------------------------------- EQP::TR
130 : : * (= (= t4 t3) false)
131 : : *
132 : : * which is converted into
133 : : *
134 : : * (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
135 : : * ------------------------ TR ------------------------ TR
136 : : * (= t1 t3) (= t2 t4)
137 : : * ----------- SYMM ----------- SYMM
138 : : * (= t3 t1) (= t4 t2)
139 : : * ---------------------------------------- CONG
140 : : * (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
141 : : * --------------------------------------------------------------------- TR
142 : : * (= (= t3 t4) false)
143 : : * --------------------- MACRO_SR_PRED_TRANSFORM
144 : : * (= (= t4 t3) false)
145 : : *
146 : : * whereas the last step is only necessary if the conclusion has the arguments
147 : : * in reverse order than expected. Note that the original step represents two
148 : : * substitutions happening on the disequality, from t1->t3 and t2->t4, which
149 : : * are implicitly justified by transitivity steps that need to be made
150 : : * explicity. Since there is no sense of ordering among which premisis (other
151 : : * than (= (= t1 t2) false)) are used for which substitution, the transitivity
152 : : * proofs are built greedly by searching the sets of premises.
153 : : *
154 : : * If in either of the above cases then the conclusion is directly derived
155 : : * in the call, so only in the other cases we try to build a transitivity
156 : : * step below
157 : : *
158 : : * @param conclusion the conclusion of the (possibly) coarse-grained
159 : : * transitivity step
160 : : * @param premises the premises of the (possibly) coarse-grained
161 : : * transitivity step
162 : : * @param p a pointer to a CDProof to store the conversion of this EqProof
163 : : * @param assumptions the assumptions (and variants) of the original
164 : : * EqProof. These are necessary to avoid cyclic proofs, which could be
165 : : * generated by creating transitivity steps for assumptions (which depend on
166 : : * themselves).
167 : : * @return True if the EqProof transitivity step is in either of the above
168 : : * cases, symbolizing that the ProofNode justifying the conclusion has already
169 : : * been produced.
170 : : */
171 : : bool expandTransitivityForDisequalities(
172 : : Node conclusion,
173 : : std::vector<Node>& premises,
174 : : CDProof* p,
175 : : std::unordered_set<Node>& assumptions) const;
176 : :
177 : : /** Expand coarse-grained transitivity steps for theory disequalities
178 : : *
179 : : * Currently the equality engine can represent disequality reasoning of theory
180 : : * symbols in a rather coarse-grained manner with EqProof. This is the case
181 : : * when EqProof is
182 : : * (= t1 c1) (= t2 c2)
183 : : * ------------------------------------- EQP::TR
184 : : * (= (t1 t2) false)
185 : : *
186 : : * which is converted into
187 : : *
188 : : * (= t1 c1) (= t2 c2)
189 : : * -------------------------- CONG --------------------- MACRO_SR_PRED_INTRO
190 : : * (= (= t1 t2) (= c1 t2)) (= (= c1 c2) false)
191 : : * --------------------------------------------------------- TR
192 : : * (= (= t1 t2) false)
193 : : *
194 : : * @param conclusion the conclusion of the (possibly) coarse-grained
195 : : * transitivity step
196 : : * @param premises the premises of the (possibly) coarse-grained
197 : : * transitivity step
198 : : * @param p a pointer to a CDProof to store the conversion of this EqProof
199 : : * @return True if the EqProof transitivity step is the above case,
200 : : * indicating that the ProofNode justifying the conclusion has already been
201 : : * produced.
202 : : */
203 : : bool expandTransitivityForTheoryDisequalities(Node conclusion,
204 : : std::vector<Node>& premises,
205 : : CDProof* p) const;
206 : :
207 : : /** Builds a transitivity chain from equalities to derive a conclusion
208 : : *
209 : : * Given an equality (= t1 tn), and a list of equalities premises, attempts to
210 : : * build a chain (= t1 t2) ... (= tn-1 tn) from premises. This is done in a
211 : : * greedy manner by finding one "link" in the chain at a time, updating the
212 : : * conclusion to be the next link and the premises by removing the used
213 : : * premise, and searching recursively.
214 : : *
215 : : * Consider for example
216 : : * - conclusion: (= t1 t4)
217 : : * - premises: (= t4 t2), (= t2 t3), (= t2 t1), (= t3 t4)
218 : : *
219 : : * It proceeds by searching for t1 in an equality in the premises, in order,
220 : : * which is found in the equality (= t2 t1). Since t2 != t4, it attempts to
221 : : * build a chain with
222 : : * - conclusion (= t2 t4)
223 : : * - premises (= t4 t2), (= t2 t3), (= t3 t4)
224 : : *
225 : : * In the first equality it finds t2 and also t4, which closes the chain, so
226 : : * that premises is updated to (= t2 t4) and the method returns true. Since
227 : : * the recursive call was successful, the original conclusion (= t1 t4) is
228 : : * justified with (= t1 t2) plus the chain built in the recursive call,
229 : : * i.e. (= t1 t2), (= t2 t4).
230 : : *
231 : : * Note that not all the premises were necessary to build a successful
232 : : * chain. Moreover, note that building a successful chain can depend on the
233 : : * order in which the equalities are chosen. When a recursive call fails to
234 : : * close a chain, the chosen equality is dismissed and another is searched for
235 : : * among the remaining ones.
236 : : *
237 : : * This method assumes that premises does not contain reflexivity premises.
238 : : * This is without loss of generality since such premises are spurious for a
239 : : * transitivity step.
240 : : *
241 : : * @param conclusion the conclusion of the transitivity chain of equalities
242 : : * @param premises the list of equalities to build a chain with
243 : : * @return whether premises successfully build a transitivity chain for the
244 : : * conclusion
245 : : */
246 : : bool buildTransitivityChain(Node conclusion,
247 : : std::vector<Node>& premises) const;
248 : :
249 : : /** Reduce a congruence EqProof into a transitivity matrix
250 : : *
251 : : * Given a congruence EqProof of (= (f a0 ... an-1) (f b0 ... bn-1)), reduce
252 : : * its justification into a matrix
253 : : *
254 : : * [0] -> p_{0,0} ... p_{m_0,0}
255 : : * ...
256 : : * [n-1] -> p_{0,n} ... p_{m_n-1,n-1}
257 : : *
258 : : * where f has arity n and each p_{0,i} ... p_{m_i, i} is a transitivity chain
259 : : * (modulo ordering) justifying (= ai bi).
260 : : *
261 : : * Congruence steps in EqProof are binary, representing reasoning over curried
262 : : * applications. In the simplest case the general shape of a congruence
263 : : * EqProof is:
264 : : * P0
265 : : * ------- EQP::REFL ----------
266 : : * P1 [] (= a0 b0)
267 : : * --------- ----------------------- EQP::CONG
268 : : * (= a1 b1) [] P2
269 : : * ------------------------- EQP::CONG -----------
270 : : * [] (= a2 b2)
271 : : * ------------------------------------------------ EQP::CONG
272 : : * (= (f a0 a1 a2) (f b0 b1 b2))
273 : : *
274 : : * where [] stands for the null node, symbolizing "equality between partial
275 : : * applications".
276 : : *
277 : : * The reduction of such a proof is done by
278 : : * - converting the proof of the second CONG premise (via addToProof) and
279 : : * adding the resulting node to row i of the matrix
280 : : * - recursively reducing the first proof with i-1
281 : : *
282 : : * In the above case the transitivity matrix would thus be
283 : : * [0] -> (= a0 b0)
284 : : * [1] -> (= a1 b1)
285 : : * [2] -> (= a2 b2)
286 : : *
287 : : * The more complex case of congruence proofs has transitivity steps as the
288 : : * first child of CONG steps. For example
289 : : * P0
290 : : * ------- EQP::REFL ----------
291 : : * P' [] (= a0 c)
292 : : * --------- ----------------------------- EQP::CONG
293 : : * (= b0 c) [] P1
294 : : * ------------------------- EQP::TRANS -----------
295 : : * [] (= a1 b1)
296 : : * ----------------------------------------------------- EQP::CONG
297 : : * (= (f a0 a1) (f b0 b1))
298 : : *
299 : : * where when the first child of CONG is a transitivity step
300 : : * - the premises that are CONG steps are recursively reduced with *the same*
301 : : * argument i
302 : : * - the other premises are processed with addToProof and added to the i row
303 : : * in the matrix
304 : : *
305 : : * In the above example the corresponding transitivity matrix is
306 : : * [0] -> (= a0 c), (= b0 c)
307 : : * [1] -> (= a1 b1)
308 : : *
309 : : * The remaining complication is when the conclusion is an equality of n-ary
310 : : * applications of *different* arities. Then there necessarily is a
311 : : * transitivity step as a first child a CONG step whose conclusion is an
312 : : * equality of n-ary applications of different arities. For example
313 : : *
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 among 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 n-ary 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 i-th 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 n-ary 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>& visited,
351 : : std::unordered_set<Node>& assumptions,
352 : : bool isNary) const;
353 : :
354 : : }; /* class EqProof */
355 : :
356 : : } // Namespace eq
357 : : } // Namespace theory
358 : : } // namespace cvc5::internal
|
