Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of a proof as produced by the equality engine.
11 : : */
12 : :
13 : : #include "theory/uf/eq_proof.h"
14 : :
15 : : #include "base/configuration.h"
16 : : #include "options/uf_options.h"
17 : : #include "proof/proof.h"
18 : : #include "proof/proof_checker.h"
19 : : #include "proof/proof_node_algorithm.h"
20 : : #include "proof/proof_node_manager.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace eq {
25 : :
26 : 0 : void EqProof::debug_print(CVC5_UNUSED const char* c, unsigned tb) const
27 : : {
28 : 0 : std::stringstream ss;
29 : 0 : debug_print(ss, tb);
30 : 0 : Trace(c) << ss.str();
31 : 0 : }
32 : :
33 : 0 : void EqProof::debug_print(std::ostream& os, unsigned tb) const
34 : : {
35 [ - - ]: 0 : for (unsigned i = 0; i < tb; i++)
36 : : {
37 : 0 : os << " ";
38 : : }
39 : 0 : os << d_id << "(";
40 [ - - ][ - - ]: 0 : if (d_children.empty() && d_node.isNull())
[ - - ]
41 : : {
42 : 0 : os << ")";
43 : 0 : return;
44 : : }
45 [ - - ]: 0 : if (!d_node.isNull())
46 : : {
47 : 0 : os << std::endl;
48 [ - - ]: 0 : for (unsigned i = 0; i < tb + 1; ++i)
49 : : {
50 : 0 : os << " ";
51 : : }
52 [ - - ]: 0 : os << d_node << (!d_children.empty() ? "," : "");
53 : : }
54 : 0 : unsigned size = d_children.size();
55 [ - - ]: 0 : for (unsigned i = 0; i < size; ++i)
56 : : {
57 : 0 : os << std::endl;
58 : 0 : d_children[i]->debug_print(os, tb + 1);
59 [ - - ]: 0 : if (i < size - 1)
60 : : {
61 [ - - ]: 0 : for (unsigned j = 0; j < tb + 1; ++j)
62 : : {
63 : 0 : os << " ";
64 : : }
65 : 0 : os << ",";
66 : : }
67 : : }
68 [ - - ]: 0 : if (size > 0)
69 : : {
70 [ - - ]: 0 : for (unsigned i = 0; i < tb; ++i)
71 : : {
72 : 0 : os << " ";
73 : : }
74 : : }
75 : 0 : os << ")" << std::endl;
76 : : }
77 : :
78 : 1789941 : void EqProof::cleanReflPremises(std::vector<Node>& premises) const
79 : : {
80 : 1789941 : std::vector<Node> newPremises;
81 : 1789941 : unsigned size = premises.size();
82 [ + + ]: 6196580 : for (unsigned i = 0; i < size; ++i)
83 : : {
84 [ + + ]: 4406639 : if (premises[i][0] == premises[i][1])
85 : : {
86 : 393409 : continue;
87 : : }
88 : 4013230 : newPremises.push_back(premises[i]);
89 : : }
90 [ + + ]: 1789941 : if (newPremises.size() != size)
91 : : {
92 [ + - ]: 378600 : Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed "
93 : 0 : << (size >= newPremises.size()
94 [ - - ]: 189300 : ? size - newPremises.size()
95 : 0 : : 0)
96 : 189300 : << " refl premises from " << premises << "\n";
97 : 189300 : premises.clear();
98 : 189300 : premises.insert(premises.end(), newPremises.begin(), newPremises.end());
99 [ + - ]: 378600 : Trace("eqproof-conv") << "EqProof::cleanReflPremises: new premises "
100 : 189300 : << premises << "\n";
101 : : }
102 : 1789941 : }
103 : :
104 : 710721 : bool EqProof::expandTransitivityForDisequalities(
105 : : Node conclusion,
106 : : std::vector<Node>& premises,
107 : : CDProof* p,
108 : : std::unordered_set<Node>& assumptions) const
109 : : {
110 [ + - ]: 1421442 : Trace("eqproof-conv")
111 : : << "EqProof::expandTransitivityForDisequalities: check if need "
112 : 0 : "to expand transitivity step to conclude "
113 : 710721 : << conclusion << " from premises " << premises << "\n";
114 : : // Check premises to see if any of the form (= (= t1 t2) false), modulo
115 : : // symmetry
116 : 710721 : unsigned size = premises.size();
117 : : // termPos is, in (= (= t1 t2) false) or (= false (= t1 t2)), the position of
118 : : // the equality. When the i-th premise has that form, offending = i
119 : 710721 : unsigned termPos = 2, offending = size;
120 [ + + ]: 3569869 : for (unsigned i = 0; i < size; ++i)
121 : : {
122 [ - + ][ - + ]: 2859148 : Assert(premises[i].getKind() == Kind::EQUAL);
[ - - ]
123 [ + + ]: 8516255 : for (unsigned j = 0; j < 2; ++j)
124 : : {
125 [ + + ][ - - ]: 11384476 : if (premises[i][j].getKind() == Kind::CONST_BOOLEAN
126 [ + + ][ + - ]: 5740763 : && !premises[i][j].getConst<bool>()
[ - - ]
127 [ + + ][ + + ]: 11433001 : && premises[i][1 - j].getKind() == Kind::EQUAL)
[ + + ][ + + ]
[ - - ]
128 : : {
129 : : // there is only one offending equality
130 [ - + ][ - + ]: 35131 : Assert(offending == size);
[ - - ]
131 : 35131 : offending = i;
132 : 35131 : termPos = 1 - j;
133 : 35131 : break;
134 : : }
135 : : }
136 : : }
137 : : // if no equality of the searched form, nothing to do
138 [ + + ]: 710721 : if (offending == size)
139 : : {
140 [ + - ]: 1351180 : Trace("eqproof-conv")
141 : 675590 : << "EqProof::expandTransitivityForDisequalities: no need.\n";
142 : 675590 : return false;
143 : : }
144 : 35131 : NodeManager* nm = conclusion.getNodeManager();
145 [ + + ][ + - ]: 35131 : Assert(termPos == 0 || termPos == 1);
[ - + ][ - + ]
[ - - ]
146 [ + - ]: 70262 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found "
147 : 0 : "offending equality at index "
148 : 35131 : << offending << " : " << premises[offending] << "\n";
149 : : // collect the premises to be used in the expansion, which are all but the
150 : : // offending one
151 : 35131 : std::vector<Node> expansionPremises;
152 [ + + ]: 144714 : for (unsigned i = 0; i < size; ++i)
153 : : {
154 [ + + ]: 109583 : if (i != offending)
155 : : {
156 : 74452 : expansionPremises.push_back(premises[i]);
157 : : }
158 : : }
159 : : // Eliminate spurious premises. Reasoning below assumes no refl steps.
160 : 35131 : cleanReflPremises(expansionPremises);
161 [ - + ][ - + ]: 35131 : Assert(!expansionPremises.empty());
[ - - ]
162 : : // Check if we are in the substitution case
163 : 35131 : Node expansionConclusion;
164 : 35131 : std::vector<Node> substPremises;
165 : 35131 : bool inSubstCase = false, substConclusionInReverseOrder = false;
166 [ + + ]: 70262 : if ((conclusion[0].getKind() == Kind::CONST_BOOLEAN)
167 : 35131 : != (conclusion[1].getKind() == Kind::CONST_BOOLEAN))
168 : : {
169 : 26234 : inSubstCase = true;
170 : : // reorder offending premise if constant is the first argument
171 [ + + ]: 26234 : if (termPos == 1)
172 : : {
173 : 25064 : premises[offending] =
174 : 50128 : premises[offending][1].eqNode(premises[offending][0]);
175 : : }
176 : : // reorder conclusion if constant is the first argument
177 : 26234 : conclusion = conclusion[1].getKind() == Kind::CONST_BOOLEAN
178 : 52468 : ? conclusion
179 : 26234 : : conclusion[1].eqNode(conclusion[0]);
180 : : // equality term in premise disequality
181 : 26234 : Node premiseTermEq = premises[offending][0];
182 : : // equality term in conclusion disequality
183 : 26234 : Node conclusionTermEq = conclusion[0];
184 [ + - ]: 52468 : Trace("eqproof-conv")
185 : : << "EqProof::expandTransitivityForDisequalities: Substitition "
186 : 0 : "case. Need to build subst from "
187 : 26234 : << premiseTermEq << " to " << conclusionTermEq << "\n";
188 : : // If only one argument in the premise is substituted, premiseTermEq and
189 : : // conclusionTermEq will share one argument and the other argument change
190 : : // defines the single substitution. Otherwise both arguments are replaced,
191 : : // so there are two substitutions.
192 [ + + ]: 131170 : std::vector<Node> subs[2];
193 : 26234 : subs[0].push_back(premiseTermEq[0]);
194 : 26234 : subs[1].push_back(premiseTermEq[1]);
195 : : // which of the arguments of premiseTermEq, if any, is equal to one argument
196 : : // of conclusionTermEq
197 : 26234 : int equalArg = -1;
198 [ + + ]: 78702 : for (unsigned i = 0; i < 2; ++i)
199 : : {
200 [ + + ]: 132629 : for (unsigned j = 0; j < 2; ++j)
201 : : {
202 [ + + ]: 96902 : if (premiseTermEq[i] == conclusionTermEq[j])
203 : : {
204 : 16741 : equalArg = i;
205 : : // identity sub
206 : 16741 : subs[i].push_back(conclusionTermEq[j]);
207 : : // sub that changes argument
208 : 16741 : subs[1 - i].push_back(conclusionTermEq[1 - j]);
209 : : // wither e.g. (= t1 t2), with sub t1->t3, becomes (= t2 t3)
210 : 16741 : substConclusionInReverseOrder = i != j;
211 : 16741 : break;
212 : : }
213 : : }
214 : : }
215 : : // simple case of single substitution
216 [ + + ]: 26234 : if (equalArg >= 0)
217 : : {
218 : : // case of
219 : : // (= (= t1 t2) false) (= t1 x1) ... (= xn t3)
220 : : // -------------------------------------------- EQP::TR
221 : : // (= (= t3 t2) false)
222 : : // where
223 : : //
224 : : // (= t1 x1) ... (= xn t3) - expansion premises
225 : : // ------------------------ TRANS
226 : : // (= t1 t3) - expansion conclusion
227 : : //
228 : : // will be the expansion made to justify the substitution for t1->t3.
229 : 16741 : expansionConclusion = subs[1 - equalArg][0].eqNode(subs[1 - equalArg][1]);
230 [ + - ]: 33482 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
231 : 0 : "Need to expand premises into "
232 : 16741 : << expansionConclusion << "\n";
233 : : // add refl step for the substitition t2->t2
234 : 33482 : p->addStep(subs[equalArg][0].eqNode(subs[equalArg][1]),
235 : : ProofRule::REFL,
236 : : {},
237 : 16741 : {subs[equalArg][0]});
238 : : }
239 : : else
240 : : {
241 : : // Hard case. We determine, and justify, the substitutions t1->t3/t4 and
242 : : // t2->t3/t4 based on the expansion premises.
243 [ + - ]: 18986 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
244 : 0 : "Need two substitutions. Look for "
245 : 9493 : << premiseTermEq[0] << " and " << premiseTermEq[1]
246 : 9493 : << " in premises " << expansionPremises << "\n";
247 [ - + ][ - - ]: 9493 : Assert(expansionPremises.size() >= 2)
248 : : << "Less than 2 expansion premises for substituting BOTH terms in "
249 : 0 : "disequality.\nDisequality: "
250 [ - + ][ - - ]: 9493 : << premises[offending]
251 : 0 : << "\nExpansion premises: " << expansionPremises
252 [ - + ][ - + ]: 9493 : << "\nConclusion: " << conclusion << "\n";
[ - - ]
253 : : // Easier case where we can determine the substitutions by directly
254 : : // looking at the premises, i.e. the two expansion premises are for
255 : : // example (= t1 t3) and (= t2 t4)
256 [ + + ]: 9493 : if (expansionPremises.size() == 2)
257 : : {
258 : : // iterate over args to be substituted
259 [ + + ]: 17502 : for (unsigned i = 0; i < 2; ++i)
260 : : {
261 : : // iterate over premises
262 [ + + ]: 35004 : for (unsigned j = 0; j < 2; ++j)
263 : : {
264 : : // iterate over args in premise
265 [ + + ]: 55991 : for (unsigned k = 0; k < 2; ++k)
266 : : {
267 [ + + ]: 44323 : if (premiseTermEq[i] == expansionPremises[j][k])
268 : : {
269 : 11668 : subs[i].push_back(expansionPremises[j][1 - k]);
270 : 11668 : break;
271 : : }
272 : : }
273 : : }
274 [ - + ][ - - ]: 11668 : Assert(subs[i].size() == 2)
275 [ - + ][ - + ]: 11668 : << " did not find term " << subs[i][0] << "\n";
[ - - ]
276 : : // check if argument to be substituted is in the same order in the
277 : : // conclusion
278 : : substConclusionInReverseOrder =
279 : 11668 : premiseTermEq[i] != conclusionTermEq[i];
280 : : }
281 : : }
282 : : else
283 : : {
284 [ + - ]: 7318 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
285 : : "Build transitivity chains "
286 : 0 : "for two subs among more than 2 premises: "
287 : 3659 : << expansionPremises << "\n";
288 : : // Hardest case. Try building a transitivity chain for (= t1 t3). If it
289 : : // can be built, use the remaining expansion premises to build a chain
290 : : // for (= t2 t4). Otherwise build it for (= t1 t4) and then build it for
291 : : // (= t2 t3). It should always succeed.
292 : 3659 : subs[0].push_back(conclusionTermEq[0]);
293 : 3659 : subs[1].push_back(conclusionTermEq[1]);
294 [ + + ]: 10977 : for (unsigned i = 0; i < 2; ++i)
295 : : {
296 : : // copy premises, since buildTransitivityChain is destructive
297 : : std::vector<Node> copy1ofExpPremises(expansionPremises.begin(),
298 : 7318 : expansionPremises.end());
299 : 7318 : Node transConclusion1 = subs[0][0].eqNode(subs[0][1]);
300 [ - + ]: 7318 : if (!buildTransitivityChain(transConclusion1, copy1ofExpPremises))
301 : : {
302 : 0 : AlwaysAssert(i == 0)
303 : : << "Couldn't find sub at all for substituting BOTH terms in "
304 : 0 : "disequality.\nDisequality: "
305 : 0 : << premises[offending]
306 : 0 : << "\nExpansion premises: " << expansionPremises
307 : 0 : << "\nConclusion: " << conclusion << "\n";
308 : : // Failed. So flip sub and try again
309 : 0 : subs[0][1] = conclusionTermEq[1];
310 : 0 : subs[1][1] = conclusionTermEq[0];
311 : 0 : substConclusionInReverseOrder = false;
312 : 0 : continue;
313 : : }
314 : : // build next chain
315 : : std::vector<Node> copy2ofExpPremises(expansionPremises.begin(),
316 : 7318 : expansionPremises.end());
317 : 7318 : Node transConclusion2 = subs[1][0].eqNode(subs[1][1]);
318 [ - + ]: 7318 : if (!buildTransitivityChain(transConclusion2, copy2ofExpPremises))
319 : : {
320 : 0 : Unreachable() << "Found sub " << transConclusion1
321 : 0 : << " but not other sub " << transConclusion2
322 : 0 : << ".\nDisequality: " << premises[offending]
323 : 0 : << "\nExpansion premises: " << expansionPremises
324 : 0 : << "\nConclusion: " << conclusion << "\n";
325 : : }
326 [ + - ]: 14636 : Trace("eqproof-conv")
327 : : << "EqProof::expandTransitivityForDisequalities: Built trans "
328 : : "chains: "
329 : 7318 : "for two subs among more than 2 premises:\n";
330 [ + - ]: 14636 : Trace("eqproof-conv")
331 : 0 : << "EqProof::expandTransitivityForDisequalities: "
332 : 7318 : << transConclusion1 << " <- " << copy1ofExpPremises << "\n";
333 [ + - ]: 14636 : Trace("eqproof-conv")
334 : 0 : << "EqProof::expandTransitivityForDisequalities: "
335 : 7318 : << transConclusion2 << " <- " << copy2ofExpPremises << "\n";
336 : : // do transitivity steps if need be to justify each substitution
337 : 7318 : if (copy1ofExpPremises.size() > 1
338 [ + + ][ + + ]: 7318 : && !assumptions.count(transConclusion1))
[ + + ]
339 : : {
340 : 6296 : p->addStep(transConclusion1,
341 : : ProofRule::TRANS,
342 : : copy1ofExpPremises,
343 : : {},
344 : : true);
345 : : }
346 : 7318 : if (copy2ofExpPremises.size() > 1
347 [ + + ][ + + ]: 7318 : && !assumptions.count(transConclusion2))
[ + + ]
348 : : {
349 : 6402 : p->addStep(transConclusion2,
350 : : ProofRule::TRANS,
351 : : copy2ofExpPremises,
352 : : {},
353 : : true);
354 : : }
355 [ + - ][ + - ]: 7318 : }
356 : : }
357 : : }
358 [ + - ]: 52468 : Trace("eqproof-conv")
359 : 0 : << "EqProof::expandTransitivityForDisequalities: Built substutitions "
360 : 0 : << subs[0] << " and " << subs[1] << " to map " << premiseTermEq
361 : 26234 : << " -> " << conclusionTermEq << "\n";
362 : 52468 : Assert(subs[0][1] == conclusion[0][0] || subs[0][1] == conclusion[0][1])
363 : 0 : << "EqProof::expandTransitivityForDisequalities: First substitution "
364 [ - + ][ - + ]: 26234 : << subs[0] << " doest not map to conclusion " << conclusion << "\n";
[ - - ]
365 : 52468 : Assert(subs[1][1] == conclusion[0][0] || subs[1][1] == conclusion[0][1])
366 : 0 : << "EqProof::expandTransitivityForDisequalities: Second substitution "
367 [ - + ][ - + ]: 26234 : << subs[1] << " doest not map to conclusion " << conclusion << "\n";
[ - - ]
368 : : // In the premises for the original conclusion, the substitution of
369 : : // premiseTermEq (= t1 t2) into conclusionTermEq (= t3 t4) is stored
370 : : // reversed, i.e. as (= (= t3 t4) (= t1 t2)), since the transitivity with
371 : : // the disequality is built as as
372 : : // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
373 : : // --------------------------------------------------------------------- TR
374 : : // (= (= t3 t4) false)
375 : 26234 : substPremises.push_back(subs[0][1].eqNode(subs[0][0]));
376 : 26234 : substPremises.push_back(subs[1][1].eqNode(subs[1][0]));
377 [ + + ][ - - ]: 104936 : }
378 : : else
379 : : {
380 : : // In simple case the conclusion is always, modulo symmetry, false = true
381 : 8897 : Assert(conclusion[0].getKind() == Kind::CONST_BOOLEAN
382 : : && conclusion[1].getKind() == Kind::CONST_BOOLEAN);
383 : : // The expansion conclusion is the same as the equality term in the
384 : : // disequality, which is going to be justified by a transitivity step from
385 : : // the expansion premises
386 : 8897 : expansionConclusion = premises[offending][termPos];
387 : : }
388 : : // Unless we are in the double-substitution case, the proof has the shape
389 : : //
390 : : // ... ... ... ... - expansionPremises
391 : : // ------------------ TRANS
392 : : // (= (= (t t') false) (= t'' t''') - expansionConclusion
393 : : // ---------------------------------------------- TRANS or PRED_TRANSFORM
394 : : // conclusion
395 : : //
396 : : // although note that if it's a TRANS step, (= t'' t''') will be turned into a
397 : : // predicate equality and the premises are ordered.
398 : : //
399 : : // We build the transitivity step for the expansionConclusion here. It being
400 : : // non-null marks that we are not in the double-substitution case.
401 [ + + ]: 35131 : if (!expansionConclusion.isNull())
402 : : {
403 [ + - ]: 51276 : Trace("eqproof-conv")
404 : 0 : << "EqProof::expandTransitivityForDisequalities: need to derive "
405 : 0 : << expansionConclusion << " with premises " << expansionPremises
406 : 25638 : << "\n";
407 : 51276 : Assert(expansionPremises.size() > 1
408 : : || expansionConclusion == expansionPremises.back()
409 : : || (expansionConclusion[0] == expansionPremises.back()[1]
410 : : && expansionConclusion[1] == expansionPremises.back()[0]))
411 [ - + ][ - - ]: 25638 : << "single expansion premise " << expansionPremises.back()
412 [ - + ][ - + ]: 25638 : << " is not the same as expansionConclusion " << expansionConclusion
[ - - ]
413 : 0 : << " and not its symmetric\n";
414 : : // We track assumptions to avoid cyclic proofs, which can happen in EqProofs
415 : : // such as:
416 : : //
417 : : // (= l1 "") (= "" t)
418 : : // ----------------------- EQP::TR
419 : : // (= l1 "") (= l1 t) (= (= "" t) false)
420 : : // ----------------------------------------------------------------- EQP::TR
421 : : // (= false true)
422 : : //
423 : : // which would lead to the cyclic expansion proof:
424 : : //
425 : : // (= l1 "") (= l1 "") (= "" t)
426 : : // --------- SYMM ----------------------- TRANS
427 : : // (= "" l1) (= l1 t)
428 : : // ------------------------------------------ TRANS
429 : : // (= "" t)
430 [ + + ][ + + ]: 25638 : if (expansionPremises.size() > 1 && !assumptions.count(expansionConclusion))
[ + + ]
431 : : {
432 : : // create transitivity step to derive expected premise
433 : 7585 : buildTransitivityChain(expansionConclusion, expansionPremises);
434 [ + - ]: 15170 : Trace("eqproof-conv")
435 : : << "EqProof::expandTransitivityForDisequalities: add transitivity "
436 : 0 : "step for "
437 : 0 : << expansionConclusion << " with premises " << expansionPremises
438 : 7585 : << "\n";
439 : : // create expansion step
440 : 7585 : p->addStep(
441 : : expansionConclusion, ProofRule::TRANS, expansionPremises, {}, true);
442 : : }
443 : : }
444 [ + - ]: 70262 : Trace("eqproof-conv")
445 : 0 : << "EqProof::expandTransitivityForDisequalities: now derive conclusion "
446 : 35131 : << conclusion;
447 : 35131 : Node offendingNode = premises[offending];
448 : 35131 : premises.clear();
449 : 35131 : premises.push_back(offendingNode);
450 [ + + ]: 35131 : if (inSubstCase)
451 : : {
452 [ + - ][ - - ]: 52468 : Trace("eqproof-conv") << (substConclusionInReverseOrder ? " [inverted]"
453 : 0 : : "")
454 : 0 : << " via subsitution from " << premises[0]
455 : 26234 : << " and (inverted subst) " << substPremises << "\n";
456 : : // By this point, for premise disequality (= (= t1 t2) false), we have
457 : : // potentially already built
458 : : //
459 : : // (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
460 : : // ------------------------ TR ------------------------ TR
461 : : // (= t1 t3) (= t2 t4)
462 : : //
463 : : // to justify the substitutions t1->t3 and t2->t4 (where note that if t1=t3
464 : : // or t2=4, the step will actually be a REFL one). Not do
465 : : //
466 : : // ----------- SYMM ----------- SYMM
467 : : // (= t3 t1) (= t4 t2)
468 : : // ---------------------------------------- CONG
469 : : // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
470 : : // --------------------------------------------------------------------- TR
471 : : // (= (= t3 t4) false)
472 : : //
473 : : // where note that the SYMM steps are implicitly added by CDProof.
474 : : Node congConclusion = nm->mkNode(
475 : : Kind::EQUAL,
476 : 52468 : nm->mkNode(Kind::EQUAL, substPremises[0][0], substPremises[1][0]),
477 : 104936 : premises[0][0]);
478 : 26234 : std::vector<Node> cargs;
479 : 26234 : ProofRule rule = expr::getCongRule(congConclusion[0], cargs);
480 : 26234 : p->addStep(congConclusion, rule, substPremises, cargs, true);
481 [ + - ]: 52468 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
482 : 0 : "congruence derived "
483 : 26234 : << congConclusion << "\n";
484 : : // transitivity step between that and the original premise
485 : 26234 : premises.insert(premises.begin(), congConclusion);
486 : : Node transConclusion =
487 : 26234 : !substConclusionInReverseOrder
488 : : ? conclusion
489 : 48950 : : nm->mkNode(Kind::EQUAL, congConclusion[0], conclusion[1]);
490 : : // check to avoid cyclic proofs
491 [ + - ]: 26234 : if (!assumptions.count(transConclusion))
492 : : {
493 : 26234 : p->addStep(transConclusion, ProofRule::TRANS, premises, {}, true);
494 [ + - ]: 52468 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
495 : 0 : "via transitivity derived "
496 : 26234 : << transConclusion << "\n";
497 : : }
498 : : // if order is reversed, finish the proof of conclusion with
499 : : // (= (= t3 t4) false)
500 : : // --------------------- MACRO_SR_PRED_TRANSFORM
501 : : // (= (= t4 t3) false)
502 [ + + ]: 26234 : if (substConclusionInReverseOrder)
503 : : {
504 : 22716 : p->addStep(conclusion,
505 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
506 : : {transConclusion},
507 : : {conclusion},
508 : : true);
509 [ + - ]: 15144 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
510 : 0 : "via macro transform derived "
511 : 7572 : << conclusion << "\n";
512 : : }
513 : 26234 : }
514 : : else
515 : : {
516 : : // create TRUE_INTRO step for expansionConclusion and add it to the premises
517 [ + - ]: 17794 : Trace("eqproof-conv")
518 : : << " via transitivity.\nEqProof::expandTransitivityForDisequalities: "
519 : 0 : "adding "
520 [ - + ][ - - ]: 8897 : << ProofRule::TRUE_INTRO << " step for " << expansionConclusion[0]
521 : 8897 : << "\n";
522 : : Node newExpansionConclusion =
523 : 8897 : expansionConclusion.eqNode(nm->mkConst<bool>(true));
524 : 17794 : p->addStep(newExpansionConclusion,
525 : : ProofRule::TRUE_INTRO,
526 : : {expansionConclusion},
527 : : {});
528 : 8897 : premises.push_back(newExpansionConclusion);
529 [ + - ]: 8897 : Trace("eqproof-conv") << ProofRule::TRANS << " from " << premises << "\n";
530 : 8897 : buildTransitivityChain(conclusion, premises);
531 : : // create final transitivity step
532 : 8897 : p->addStep(conclusion, ProofRule::TRANS, premises, {}, true);
533 : 8897 : }
534 : 35131 : return true;
535 : 35131 : }
536 : :
537 : : // TEMPORARY NOTE: This may not be enough. Worst case scenario I need to
538 : : // reproduce here a search for arbitrary chains between each of the variables in
539 : : // the conclusion and a constant
540 : 675590 : bool EqProof::expandTransitivityForTheoryDisequalities(
541 : : Node conclusion, std::vector<Node>& premises, CDProof* p) const
542 : : {
543 : : // whether conclusion is a disequality (= (= t1 t2) false), modulo symmetry
544 : 675590 : unsigned termPos = -1;
545 [ + + ]: 2026755 : for (unsigned i = 0; i < 2; ++i)
546 : : {
547 [ + + ][ - - ]: 1351180 : if (conclusion[i].getKind() == Kind::CONST_BOOLEAN
548 [ + + ][ + - ]: 1363045 : && !conclusion[i].getConst<bool>()
[ - - ]
549 [ + + ][ + + ]: 1363045 : && conclusion[1 - i].getKind() == Kind::EQUAL)
[ + + ][ + + ]
[ - - ]
550 : : {
551 : 15 : termPos = i - 1;
552 : 15 : break;
553 : : }
554 : : }
555 : : // no disequality
556 [ + + ]: 675590 : if (termPos == static_cast<unsigned>(-1))
557 : : {
558 : 675575 : return false;
559 : : }
560 [ + - ]: 30 : Trace("eqproof-conv")
561 : : << "EqProof::expandTransitivityForTheoryDisequalities: check if need "
562 : 0 : "to expand transitivity step to conclude disequality "
563 : 15 : << conclusion << " from premises " << premises << "\n";
564 : :
565 : : // Check if the premises are (= t1 c1) and (= t2 c2), modulo symmetry
566 : 15 : std::vector<Node> subChildren, constChildren;
567 [ + + ]: 45 : for (unsigned i = 0; i < 2; ++i)
568 : : {
569 : 30 : Node term = conclusion[termPos][i];
570 [ + + ]: 90 : for (const Node& premise : premises)
571 : : {
572 [ + + ]: 138 : for (unsigned j = 0; j < 2; ++j)
573 : : {
574 : 108 : if (premise[j] == term && premise[1 - j].isConst())
575 : : {
576 : 30 : subChildren.push_back(premise[j].eqNode(premise[1 - j]));
577 : 30 : constChildren.push_back(premise[1 - j]);
578 : 30 : break;
579 : : }
580 : : }
581 : : }
582 : 30 : }
583 [ - + ]: 15 : if (subChildren.size() < 2)
584 : : {
585 : 0 : return false;
586 : : }
587 : : // Now build
588 : : // (= t1 c1) (= t2 c2)
589 : : // ------------------------- CONG ------------------- MACRO_SR_PRED_INTRO
590 : : // (= (= t1 t2) (= c1 c2)) (= (= c1 c2) false)
591 : : // --------------------------------------------------------------------- TR
592 : : // (= (= t1 t2) false)
593 : : Node constApp =
594 : 15 : conclusion.getNodeManager()->mkNode(Kind::EQUAL, constChildren);
595 : 15 : Node constEquality = constApp.eqNode(conclusion[1 - termPos]);
596 [ + - ]: 30 : Trace("eqproof-conv")
597 : 0 : << "EqProof::expandTransitivityForTheoryDisequalities: adding "
598 : 0 : << ProofRule::MACRO_SR_PRED_INTRO << " step for " << constApp << " = "
599 [ - + ][ - - ]: 15 : << conclusion[1 - termPos] << "\n";
600 : 30 : p->addStep(
601 : : constEquality, ProofRule::MACRO_SR_PRED_INTRO, {}, {constEquality});
602 : : // build congruence conclusion (= (= t1 t2) (t c1 c2))
603 : 15 : Node congConclusion = conclusion[termPos].eqNode(constApp);
604 [ + - ]: 30 : Trace("eqproof-conv")
605 : 0 : << "EqProof::expandTransitivityForTheoryDisequalities: adding "
606 : 15 : << ProofRule::CONG << " step for " << congConclusion << " from "
607 : 15 : << subChildren << "\n";
608 : 15 : std::vector<Node> cargs;
609 : 15 : ProofRule rule = expr::getCongRule(conclusion[termPos], cargs);
610 : 15 : p->addStep(congConclusion, rule, {subChildren}, cargs, true);
611 [ + - ]: 30 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
612 : 0 : "congruence derived "
613 : 15 : << congConclusion << "\n";
614 : 60 : std::vector<Node> transitivityChildren{congConclusion, constEquality};
615 : 15 : p->addStep(conclusion, ProofRule::TRANS, {transitivityChildren}, {});
616 : 15 : return true;
617 : 15 : }
618 : :
619 : 2863315 : bool EqProof::buildTransitivityChain(Node conclusion,
620 : : std::vector<Node>& premises) const
621 : : {
622 [ + - ]: 5726630 : Trace("eqproof-conv") << push
623 : 0 : << "EqProof::buildTransitivityChain: Build chain for "
624 : 2863315 : << conclusion << " with premises " << premises << "\n";
625 [ + - ]: 21777484 : for (unsigned i = 0, size = premises.size(); i < size; ++i)
626 : : {
627 : 21777484 : bool occurs = false, correctlyOrdered = false;
628 [ + + ]: 21777484 : if (conclusion[0] == premises[i][0])
629 : : {
630 : 929997 : occurs = correctlyOrdered = true;
631 : : }
632 [ + + ]: 20847487 : else if (conclusion[0] == premises[i][1])
633 : : {
634 : 1933318 : occurs = true;
635 : : }
636 [ + + ]: 21777484 : if (occurs)
637 : : {
638 [ + - ]: 5726630 : Trace("eqproof-conv")
639 [ - - ]: 2863315 : << "EqProof::buildTransitivityChain: found " << conclusion[0] << " in"
640 [ - - ][ - + ]: 2863315 : << (correctlyOrdered ? "" : " non-") << " ordered premise "
641 : 2863315 : << premises[i] << "\n";
642 [ + + ][ + + ]: 2863315 : if (conclusion[1] == premises[i][correctlyOrdered ? 1 : 0])
643 : : {
644 [ + - ]: 1452680 : Trace("eqproof-conv")
645 [ - + ][ - - ]: 726340 : << "EqProof::buildTransitivityChain: found " << conclusion[1]
646 : 0 : << " in same premise. Closed chain.\n"
647 : 726340 : << pop;
648 : 726340 : premises.clear();
649 : 726340 : premises.push_back(conclusion);
650 : 2863315 : return true;
651 : : }
652 : : // Build chain with remaining equalities
653 : 2136975 : std::vector<Node> recursivePremises;
654 [ + + ]: 23235446 : for (unsigned j = 0; j < size; ++j)
655 : : {
656 [ + + ]: 21098471 : if (j != i)
657 : : {
658 : 18961496 : recursivePremises.push_back(premises[j]);
659 : : }
660 : : }
661 : : Node newTarget =
662 [ + + ]: 4273950 : premises[i][correctlyOrdered ? 1 : 0].eqNode(conclusion[1]);
663 [ + - ]: 4273950 : Trace("eqproof-conv")
664 : 0 : << "EqProof::buildTransitivityChain: search recursively for "
665 : 2136975 : << newTarget << "\n";
666 [ + - ]: 2136975 : if (buildTransitivityChain(newTarget, recursivePremises))
667 : : {
668 [ + - ]: 4273950 : Trace("eqproof-conv")
669 : 0 : << "EqProof::buildTransitivityChain: closed chain with "
670 : 0 : << 1 + recursivePremises.size() << " of the original "
671 : 2136975 : << premises.size() << " premises\n"
672 : 2136975 : << pop;
673 : : Node premiseNode = correctlyOrdered
674 : 679407 : ? premises[i]
675 : 4273950 : : premises[i][1].eqNode(premises[i][0]);
676 : 2136975 : premises.clear();
677 : 2136975 : premises.push_back(premiseNode);
678 : 4273950 : premises.insert(
679 : 2136975 : premises.end(), recursivePremises.begin(), recursivePremises.end());
680 : 2136975 : return true;
681 : 2136975 : }
682 [ - + ][ - + ]: 4273950 : }
683 : : }
684 [ - - ]: 0 : Trace("eqproof-conv")
685 : 0 : << "EqProof::buildTransitivityChain: Could not build chain for"
686 : 0 : << conclusion << " with premises " << premises << "\n";
687 [ - - ]: 0 : Trace("eqproof-conv") << pop;
688 : 0 : return false;
689 : : }
690 : :
691 : 2716409 : void EqProof::reduceNestedCongruence(
692 : : unsigned i,
693 : : Node conclusion,
694 : : std::vector<std::vector<Node>>& transitivityMatrix,
695 : : CDProof* p,
696 : : std::unordered_map<Node, Node>& visited,
697 : : std::unordered_set<Node>& assumptions,
698 : : bool isNary) const
699 : : {
700 [ + - ]: 5432818 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i
701 : 2716409 : << "-th arg\n";
702 [ + + ]: 2716409 : if (d_id == MERGED_THROUGH_CONGRUENCE)
703 : : {
704 [ - + ][ - + ]: 2260202 : Assert(d_children.size() == 2);
[ - - ]
705 [ + - ]: 4520404 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
706 : 0 : "congruence step. Reduce second child\n"
707 : 2260202 : << push;
708 : 4520404 : transitivityMatrix[i].push_back(
709 : 4520404 : d_children[1]->addToProof(p, visited, assumptions));
710 [ + - ]: 4520404 : Trace("eqproof-conv")
711 : 0 : << pop << "EqProof::reduceNestedCongruence: child conclusion "
712 : 2260202 : << transitivityMatrix[i].back() << "\n";
713 : : // if i == 0, first child must be REFL step, standing for (= f f), which can
714 : : // be ignored in a first-order calculus
715 : : // Notice if higher-order is disabled, the following holds:
716 : : // i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY
717 : : // We don't have access to whether we are higher-order in this context,
718 : : // so the above cannot be an assertion.
719 : : // recurse
720 [ + + ]: 2260202 : if (i > 1)
721 : : {
722 [ + - ]: 1365818 : Trace("eqproof-conv")
723 : 0 : << "EqProof::reduceNestedCongruence: Reduce first child\n"
724 : 682909 : << push;
725 : 682909 : d_children[0]->reduceNestedCongruence(i - 1,
726 : : conclusion,
727 : : transitivityMatrix,
728 : : p,
729 : : visited,
730 : : assumptions,
731 : : isNary);
732 [ + - ]: 682909 : Trace("eqproof-conv") << pop;
733 : : }
734 : : // higher-order case
735 [ + + ]: 1577293 : else if (d_children[0]->d_id != MERGED_THROUGH_REFLEXIVITY)
736 : : {
737 [ + - ]: 690 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: HO case. "
738 : 345 : "Processing first child\n";
739 : : // we only handle these cases
740 [ + + ][ + - ]: 345 : Assert(d_children[0]->d_id == MERGED_THROUGH_EQUALITY
[ - + ][ - + ]
[ - - ]
741 : : || d_children[0]->d_id == MERGED_THROUGH_TRANS);
742 : 690 : transitivityMatrix[0].push_back(
743 : 690 : d_children[0]->addToProof(p, visited, assumptions));
744 : : }
745 : 2260202 : return;
746 : : }
747 [ - + ][ - + ]: 456207 : Assert(d_id == MERGED_THROUGH_TRANS)
[ - - ]
748 : 0 : << "id is " << static_cast<MergeReasonType>(d_id) << "\n";
749 [ + - ]: 912414 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
750 : 456207 : "transitivity step.\n";
751 : 456207 : Assert(d_node.isNull()
752 : : || d_node[0].getNumChildren() == d_node[1].getNumChildren() || isNary)
753 : : << "Non-null (internal cong) transitivity conclusion of different arity "
754 : 0 : "but not marked by isNary flag\n";
755 : : // If handling n-ary kinds and got a transitivity conclusion, we process it
756 : : // with addToProof, store the result into row i, and stop. This marks an
757 : : // "adjustment" of the arity, with empty rows 0..i-1 in the matrix determining
758 : : // the adjustment in addToProof processing the congruence of the original
759 : : // conclusion. See details there.
760 [ + + ][ + + ]: 456207 : if (isNary && !d_node.isNull())
[ + + ]
761 : : {
762 [ + - ]: 1740 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: n-ary case, "
763 : 0 : "break recursion and indepedently process "
764 : 0 : << d_node << "\n"
765 : 870 : << push;
766 : 870 : transitivityMatrix[i].push_back(addToProof(p, visited, assumptions));
767 [ + - ]: 1740 : Trace("eqproof-conv") << pop
768 : 0 : << "EqProof::reduceNestedCongruence: Got conclusion "
769 : 0 : << transitivityMatrix[i].back()
770 : 870 : << " from n-ary transitivity processing\n";
771 : 870 : return;
772 : : }
773 : : // Regular recursive processing of each transitivity premise
774 [ + + ]: 1592236 : for (unsigned j = 0, sizeTrans = d_children.size(); j < sizeTrans; ++j)
775 : : {
776 [ + - ]: 1136899 : if (d_children[j]->d_id == MERGED_THROUGH_CONGRUENCE)
777 : : {
778 [ + - ]: 2273798 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce " << j
779 : 0 : << "-th transitivity congruence child\n"
780 : 1136899 : << push;
781 : 1136899 : d_children[j]->reduceNestedCongruence(
782 : : i, conclusion, transitivityMatrix, p, visited, assumptions, isNary);
783 [ + - ]: 1136899 : Trace("eqproof-conv") << pop;
784 : : }
785 : : else
786 : : {
787 [ - - ]: 0 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Add " << j
788 : 0 : << "-th transitivity child to proof\n"
789 : 0 : << push;
790 : 0 : transitivityMatrix[i].push_back(
791 : 0 : d_children[j]->addToProof(p, visited, assumptions));
792 [ - - ]: 0 : Trace("eqproof-conv") << pop;
793 : : }
794 : : }
795 : : }
796 : :
797 : 390238 : Node EqProof::addToProof(CDProof* p) const
798 : : {
799 : 390238 : std::unordered_map<Node, Node> cache;
800 : 390238 : std::unordered_set<Node> assumptions;
801 : 390238 : Node conclusion = addToProof(p, cache, assumptions);
802 [ + - ]: 780476 : Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion
803 : 390238 : << "\n";
804 [ + - ]: 780476 : Trace("eqproof-conv") << "EqProof::addToProof: tracked assumptions: "
805 : 390238 : << assumptions << "\n";
806 : : // If conclusion t1 = tn is, modulo symmetry, of the form (= t true/false), in
807 : : // which t is not true/false, it must be turned into t or (not t) with
808 : : // TRUE/FALSE_ELIM.
809 : 390238 : Node newConclusion = conclusion;
810 [ - + ][ - + ]: 390238 : Assert(conclusion.getKind() == Kind::EQUAL);
[ - - ]
811 [ + + ]: 780476 : if ((conclusion[0].getKind() == Kind::CONST_BOOLEAN)
812 : 390238 : != (conclusion[1].getKind() == Kind::CONST_BOOLEAN))
813 : : {
814 [ + - ]: 83552 : Trace("eqproof-conv")
815 : 41776 : << "EqProof::addToProof: process root for TRUE/FALSE_ELIM\n";
816 : : // Index of constant in equality
817 : : unsigned constIndex =
818 : 41776 : conclusion[0].getKind() == Kind::CONST_BOOLEAN ? 0 : 1;
819 : : // The premise for the elimination rule must have the constant as the second
820 : : // argument of the equality. If that's not the case, build it as such,
821 : : // relying on an implicit SYMM step to be added to the proof when justifying
822 : : // t / (not t).
823 : : Node elimPremise =
824 : 52709 : constIndex == 1 ? conclusion : conclusion[1].eqNode(conclusion[0]);
825 : : // Determine whether TRUE_ELIM or FALSE_ELIM, depending on the constant
826 : : // value. The new conclusion, whether t or (not t), is also determined
827 : : // accordingly.
828 : : ProofRule elimRule;
829 [ + + ]: 41776 : if (conclusion[constIndex].getConst<bool>())
830 : : {
831 : 9001 : elimRule = ProofRule::TRUE_ELIM;
832 : 9001 : newConclusion = conclusion[1 - constIndex];
833 : : }
834 : : else
835 : : {
836 : 32775 : elimRule = ProofRule::FALSE_ELIM;
837 : 32775 : newConclusion = conclusion[1 - constIndex].notNode();
838 : : }
839 : : // We also check if the final conclusion t / (not t) has already been
840 : : // justified, so that we can avoid a cyclic proof, which can be due to
841 : : // either t / (not t) being assumption in the original EqProof or it having
842 : : // a non-assumption proof step in the proof of (= t true/false).
843 [ + + ][ + + ]: 41776 : if (!assumptions.count(newConclusion) && !p->hasStep(newConclusion))
[ + + ][ + + ]
[ - - ]
844 : : {
845 [ + - ]: 60052 : Trace("eqproof-conv")
846 : 0 : << "EqProof::addToProof: conclude " << newConclusion << " via "
847 : 30026 : << elimRule << " step for " << elimPremise << "\n";
848 : 60052 : p->addStep(newConclusion, elimRule, {elimPremise}, {});
849 : : }
850 : 41776 : }
851 : 780476 : return newConclusion;
852 : 390238 : }
853 : :
854 : 5571057 : Node EqProof::addToProof(CDProof* p,
855 : : std::unordered_map<Node, Node>& visited,
856 : : std::unordered_set<Node>& assumptions) const
857 : : {
858 : 5571057 : std::unordered_map<Node, Node>::const_iterator it = visited.find(d_node);
859 [ + + ]: 5571057 : if (it != visited.end())
860 : : {
861 [ + - ]: 2313956 : Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node
862 : 1156978 : << ", returning " << it->second << "\n";
863 : 1156978 : return it->second;
864 : : }
865 [ + - ]: 8828158 : Trace("eqproof-conv") << "EqProof::addToProof: adding step for " << d_id
866 : 4414079 : << " with conclusion " << d_node << "\n";
867 : : // Assumption
868 [ + + ]: 4414079 : if (d_id == MERGED_THROUGH_EQUALITY)
869 : : {
870 : : // Check that no (= true/false true/false) assumptions
871 [ + - ][ + - ]: 2284369 : if (Configuration::isDebugBuild() && d_node.getKind() == Kind::EQUAL)
[ + - ]
872 : : {
873 [ + + ]: 6853107 : for (unsigned i = 0; i < 2; ++i)
874 : : {
875 : 9137476 : Assert(d_node[i].getKind() != Kind::CONST_BOOLEAN
876 : : || d_node[1 - i].getKind() != Kind::CONST_BOOLEAN)
877 : 0 : << "EqProof::addToProof: fully boolean constant assumption "
878 [ - + ][ - + ]: 4568738 : << d_node << " is disallowed\n";
[ - - ]
879 : : }
880 : : }
881 : : // If conclusion is (= t true/false), we add a proof step
882 : : // t
883 : : // ---------------- TRUE/FALSE_INTRO
884 : : // (= t true/false)
885 : : // according to the value of the Boolean constant
886 : 6853107 : if (d_node.getKind() == Kind::EQUAL
887 [ + - ][ + + ]: 6853107 : && ((d_node[0].getKind() == Kind::CONST_BOOLEAN)
[ - - ]
888 [ + + ][ + - ]: 4568738 : != (d_node[1].getKind() == Kind::CONST_BOOLEAN)))
[ + - ][ - - ]
889 : : {
890 [ + - ]: 117480 : Trace("eqproof-conv")
891 : 58740 : << "EqProof::addToProof: add an intro step for " << d_node << "\n";
892 : : // Index of constant in equality
893 : 58740 : unsigned constIndex = d_node[0].getKind() == Kind::CONST_BOOLEAN ? 0 : 1;
894 : : // The premise for the intro rule is either t or (not t), according to the
895 : : // Boolean constant.
896 : 58740 : Node introPremise;
897 : : ProofRule introRule;
898 [ + + ]: 58740 : if (d_node[constIndex].getConst<bool>())
899 : : {
900 : 14250 : introRule = ProofRule::TRUE_INTRO;
901 : 14250 : introPremise = d_node[1 - constIndex];
902 : : // Track the new assumption. If it's an equality, also its symmetric
903 : 14250 : assumptions.insert(introPremise);
904 [ - + ]: 14250 : if (introPremise.getKind() == Kind::EQUAL)
905 : : {
906 : 0 : assumptions.insert(introPremise[1].eqNode(introPremise[0]));
907 : : }
908 : : }
909 : : else
910 : : {
911 : 44490 : introRule = ProofRule::FALSE_INTRO;
912 : 44490 : introPremise = d_node[1 - constIndex].notNode();
913 : : // Track the new assumption. If it's a disequality, also its symmetric
914 : 44490 : assumptions.insert(introPremise);
915 [ + + ]: 44490 : if (introPremise[0].getKind() == Kind::EQUAL)
916 : : {
917 : 36880 : assumptions.insert(
918 : 73760 : introPremise[0][1].eqNode(introPremise[0][0]).notNode());
919 : : }
920 : : }
921 : : // The original assumption can be e.g. (= false (= t1 t2)) in which case
922 : : // the necessary proof to be built is
923 : : // (not (= t1 t2))
924 : : // -------------------- FALSE_INTRO
925 : : // (= (= t1 t2) false)
926 : : // -------------------- SYMM
927 : : // (= false (= t1 t2))
928 : : //
929 : : // with the SYMM step happening automatically whenever the assumption is
930 : : // used in the proof p
931 : : Node introConclusion =
932 : 103436 : constIndex == 1 ? d_node : d_node[1].eqNode(d_node[0]);
933 : 117480 : p->addStep(introConclusion, introRule, {introPremise}, {});
934 : 58740 : }
935 : : else
936 : : {
937 : 4451258 : p->addStep(d_node, ProofRule::ASSUME, {}, {d_node});
938 : : }
939 : : // If non-equality predicate, turn into one via TRUE/FALSE intro
940 : 2284369 : Node conclusion = d_node;
941 [ - + ]: 2284369 : if (d_node.getKind() != Kind::EQUAL)
942 : : {
943 : : // Track original assumption
944 : 0 : assumptions.insert(d_node);
945 : : ProofRule intro;
946 [ - - ]: 0 : if (d_node.getKind() == Kind::NOT)
947 : : {
948 : 0 : intro = ProofRule::FALSE_INTRO;
949 : : conclusion =
950 : 0 : d_node[0].eqNode(d_node.getNodeManager()->mkConst<bool>(false));
951 : : }
952 : : else
953 : : {
954 : 0 : intro = ProofRule::TRUE_INTRO;
955 : : conclusion =
956 : 0 : d_node.eqNode(d_node.getNodeManager()->mkConst<bool>(true));
957 : : }
958 [ - - ]: 0 : Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro
959 : 0 : << " step for " << d_node << "\n";
960 : 0 : p->addStep(conclusion, intro, {d_node}, {});
961 : : }
962 : : // Keep track of assumptions to avoid cyclic proofs. Both the assumption and
963 : : // its symmetric are added
964 : 2284369 : assumptions.insert(conclusion);
965 : 2284369 : assumptions.insert(conclusion[1].eqNode(conclusion[0]));
966 [ + - ]: 4568738 : Trace("eqproof-conv") << "EqProof::addToProof: tracking assumptions "
967 [ - - ]: 2284369 : << conclusion << ", (= " << conclusion[1] << " "
968 [ - + ][ - + ]: 2284369 : << conclusion[0] << ")\n";
[ - - ]
969 : 2284369 : visited[d_node] = conclusion;
970 : 2284369 : return conclusion;
971 : 2284369 : }
972 : : // Refl and laborious congruence steps for (= (f t1 ... tn) (f t1 ... tn)),
973 : : // which can be safely turned into reflexivity steps. These laborious
974 : : // congruence steps are currently generated in the equality engine because of
975 : : // the suboptimal handling of n-ary operators.
976 : 4259420 : if (d_id == MERGED_THROUGH_REFLEXIVITY
977 : 2129710 : || (d_node.getKind() == Kind::EQUAL && d_node[0] == d_node[1]))
978 : : {
979 [ + - ]: 502917 : Trace("eqproof-conv") << "EqProof::addToProof: refl step\n";
980 : : Node conclusion =
981 [ + - ]: 502917 : d_node.getKind() == Kind::EQUAL ? d_node : d_node.eqNode(d_node);
982 : 1005834 : p->addStep(conclusion, ProofRule::REFL, {}, {conclusion[0]});
983 : 502917 : visited[d_node] = conclusion;
984 : 502917 : return conclusion;
985 : 502917 : }
986 : : // Equalities due to theory reasoning
987 [ + + ]: 1626793 : if (d_id == MERGED_THROUGH_CONSTANTS)
988 : : {
989 : 38770 : Assert(!d_node.isNull()
990 : : && ((d_node.getKind() == Kind::EQUAL && d_node[1].isConst())
991 : : || (d_node.getKind() == Kind::NOT
992 : : && d_node[0].getKind() == Kind::EQUAL
993 : : && d_node[0][0].isConst() && d_node[0][1].isConst())))
994 [ - + ][ - + ]: 19385 : << ". Conclusion " << d_node << " from " << d_id
[ - - ]
995 : 0 : << " was expected to be (= (f t1 ... tn) c) or (not (= c1 c2))\n";
996 [ - + ][ - - ]: 19385 : Assert(!assumptions.count(d_node))
997 [ - + ][ - + ]: 19385 : << "Conclusion " << d_node << " from " << d_id << " is an assumption\n";
[ - - ]
998 : : // The step has the form (not (= c1 c2)). We conclude it via
999 : : // MACRO_SR_PRED_INTRO and turn it into an equality with false, so that the
1000 : : // rest of the reconstruction works
1001 [ + + ]: 19385 : if (d_children.empty())
1002 : : {
1003 : : Node conclusion =
1004 : 592 : d_node[0].eqNode(d_node.getNodeManager()->mkConst<bool>(false));
1005 : 592 : p->addStep(d_node, ProofRule::MACRO_SR_PRED_INTRO, {}, {d_node});
1006 : 592 : p->addStep(conclusion, ProofRule::FALSE_INTRO, {d_node}, {});
1007 : 296 : visited[d_node] = conclusion;
1008 : 296 : return conclusion;
1009 : 296 : }
1010 : : // The step has the form
1011 : : // [(= t1 c1)] ... [(= tn cn)]
1012 : : // ------------------------
1013 : : // (= (f t1 ... tn) c)
1014 : : // where premises equating ti to constants are present when they are not
1015 : : // already constants. Note that the premises may be in any order, e.g. with
1016 : : // the equality for the second term being justified in the first premise.
1017 : : // Moreover, they may be of the form (= ci ti).
1018 : : //
1019 : : // First recursively process premises, if any
1020 : 19089 : std::vector<Node> premises;
1021 [ + + ]: 56307 : for (unsigned i = 0; i < d_children.size(); ++i)
1022 : : {
1023 [ + - ]: 74436 : Trace("eqproof-conv")
1024 : 0 : << "EqProof::addToProof: recurse on child " << i << "\n"
1025 : 37218 : << push;
1026 : 37218 : premises.push_back(d_children[i]->addToProof(p, visited, assumptions));
1027 [ + - ]: 37218 : Trace("eqproof-conv") << pop;
1028 : : }
1029 : : // After building the proper premises we could build a step like
1030 : : // [(= t1 c1)] ... [(= tn cn)]
1031 : : // ---------------------------- MACRO_SR_PRED_INTRO
1032 : : // (= (f t1 ... tn) c)
1033 : : // but note that since the substitution applied by MACRO_SR_PRED_INTRO is
1034 : : // *not* simultenous this could lead to issues if t_{i+1} occurred in some
1035 : : // t_{i}. So we build proofs as
1036 : : //
1037 : : // [(= t1 c1)] ... [(= tn cn)]
1038 : : // ------------------------------- CONG -------------- MACRO_SR_PRED_INTRO
1039 : : // (= (f t1 ... tn) (f c1 ... cn)) (= (f c1 ... cn) c)
1040 : : // ---------------------------------------------------------- TRANS
1041 : : // (= (f t1 ... tn) c)
1042 : 19089 : std::vector<Node> subChildren, constChildren;
1043 [ + + ]: 56307 : for (unsigned i = 0, size = d_node[0].getNumChildren(); i < size; ++i)
1044 : : {
1045 : 37218 : Node term = d_node[0][i];
1046 : : // term already is a constant, add a REFL step
1047 [ + + ]: 37218 : if (term.isConst())
1048 : : {
1049 : 12564 : subChildren.push_back(term.eqNode(term));
1050 : 25128 : p->addStep(subChildren.back(), ProofRule::REFL, {}, {term});
1051 : 12564 : constChildren.push_back(term);
1052 : 12564 : continue;
1053 : : }
1054 : : // Build the equality (= ti ci) as a premise, finding the respective ci is
1055 : : // the original premises
1056 : 24654 : Node constant;
1057 [ + - ]: 38337 : for (const Node& premise : premises)
1058 : : {
1059 [ - + ][ - + ]: 38337 : Assert(premise.getKind() == Kind::EQUAL);
[ - - ]
1060 [ + + ]: 38337 : if (premise[0] == term)
1061 : : {
1062 [ - + ][ - + ]: 5380 : Assert(premise[1].isConst());
[ - - ]
1063 : 5380 : constant = premise[1];
1064 : 5380 : break;
1065 : : }
1066 [ + + ]: 32957 : if (premise[1] == term)
1067 : : {
1068 [ - + ][ - + ]: 19274 : Assert(premise[0].isConst());
[ - - ]
1069 : 19274 : constant = premise[0];
1070 : 19274 : break;
1071 : : }
1072 : : }
1073 [ - + ][ - + ]: 24654 : Assert(!constant.isNull());
[ - - ]
1074 : 24654 : subChildren.push_back(term.eqNode(constant));
1075 : 24654 : constChildren.push_back(constant);
1076 [ + + ]: 37218 : }
1077 : : // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c)
1078 : 19089 : Kind k = d_node[0].getKind();
1079 : 19089 : std::vector<Node> cargs;
1080 : 19089 : ProofRule rule = expr::getCongRule(d_node[0], cargs);
1081 [ + + ]: 19089 : if (d_node[0].getMetaKind() == kind::metakind::PARAMETERIZED)
1082 : : {
1083 : 4 : constChildren.insert(constChildren.begin(), d_node[0].getOperator());
1084 : : }
1085 : 19089 : Node constApp = d_node.getNodeManager()->mkNode(k, constChildren);
1086 : 19089 : Node constEquality = constApp.eqNode(d_node[1]);
1087 [ + - ]: 38178 : Trace("eqproof-conv") << "EqProof::addToProof: adding "
1088 : 0 : << ProofRule::MACRO_SR_PRED_INTRO << " step for "
1089 [ - + ][ - - ]: 19089 : << constApp << " = " << d_node[1] << "\n";
1090 : 38178 : p->addStep(
1091 : : constEquality, ProofRule::MACRO_SR_PRED_INTRO, {}, {constEquality});
1092 : : // build congruence conclusion (= (f t1 ... tn) (f c1 ... cn))
1093 : 19089 : Node congConclusion = d_node[0].eqNode(constApp);
1094 [ + - ]: 38178 : Trace("eqproof-conv") << "EqProof::addToProof: adding " << rule
1095 : 0 : << " step for " << congConclusion << " from "
1096 : 19089 : << subChildren << "\n";
1097 : 19089 : p->addStep(congConclusion, rule, {subChildren}, cargs, true);
1098 [ + - ]: 38178 : Trace("eqproof-conv") << "EqProof::addToProof: adding " << ProofRule::TRANS
1099 : 19089 : << " step for original conclusion " << d_node << "\n";
1100 : 76356 : std::vector<Node> transitivityChildren{congConclusion, constEquality};
1101 : 19089 : p->addStep(d_node, ProofRule::TRANS, {transitivityChildren}, {});
1102 : 19089 : visited[d_node] = d_node;
1103 : 19089 : return d_node;
1104 : 19089 : }
1105 : : // Transtivity and disequality reasoning steps
1106 [ + + ]: 1607408 : if (d_id == MERGED_THROUGH_TRANS)
1107 : : {
1108 : 1421614 : Assert(d_node.getKind() == Kind::EQUAL
1109 : : || (d_node.getKind() == Kind::NOT
1110 : : && d_node[0].getKind() == Kind::EQUAL))
1111 [ - + ][ - + ]: 710807 : << "EqProof::addToProof: transitivity step conclusion " << d_node
[ - - ]
1112 : 0 : << " is not equality or negated equality\n";
1113 : : // If conclusion is (not (= t1 t2)) change it to (= (= t1 t2) false), which
1114 : : // is the correct conclusion of the equality reasoning step. A FALSE_ELIM
1115 : : // step to revert this is only necessary when this is the root. That step is
1116 : : // done in the non-recursive caller of this function.
1117 : : Node conclusion =
1118 : 710807 : d_node.getKind() != Kind::NOT
1119 : 705973 : ? d_node
1120 : 715641 : : d_node[0].eqNode(d_node.getNodeManager()->mkConst<bool>(false));
1121 : : // If the conclusion is an assumption, its derivation was spurious, so it
1122 : : // can be discarded. Moreover, reconstructing the step may lead to cyclic
1123 : : // proofs, so we *must* cut here.
1124 [ + + ]: 710807 : if (assumptions.count(conclusion))
1125 : : {
1126 : 2 : visited[d_node] = conclusion;
1127 : 2 : return conclusion;
1128 : : }
1129 : : // Process premises recursively
1130 : 710805 : std::vector<Node> children;
1131 [ + + ]: 3582685 : for (unsigned i = 0, size = d_children.size(); i < size; ++i)
1132 : : {
1133 : : // If one of the steps is a "fake congruence" one, marked by a null
1134 : : // conclusion, it must deleted. Its premises are moved down to premises of
1135 : : // the transitivity step.
1136 : 2871880 : EqProof* childProof = d_children[i].get();
1137 : 5743760 : if (childProof->d_id == MERGED_THROUGH_CONGRUENCE
1138 [ + + ][ + + ]: 2871880 : && childProof->d_node.isNull())
[ + + ]
1139 : : {
1140 [ + - ]: 20608 : Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i
1141 : 10304 : << " is fake cong step. Fold it.\n";
1142 [ - + ][ - + ]: 10304 : Assert(childProof->d_children.size() == 2);
[ - - ]
1143 [ + - ]: 10304 : Trace("eqproof-conv") << push;
1144 [ + + ]: 30912 : for (unsigned j = 0, sizeJ = childProof->d_children.size(); j < sizeJ;
1145 : : ++j)
1146 : : {
1147 [ + - ]: 41216 : Trace("eqproof-conv")
1148 : 0 : << "EqProof::addToProof: recurse on child " << j << "\n"
1149 : 20608 : << push;
1150 : 20608 : children.push_back(
1151 : 41216 : childProof->d_children[j]->addToProof(p, visited, assumptions));
1152 [ + - ]: 20608 : Trace("eqproof-conv") << pop;
1153 : : }
1154 [ + - ]: 10304 : Trace("eqproof-conv") << pop;
1155 : 10304 : continue;
1156 : 10304 : }
1157 [ + - ]: 5723152 : Trace("eqproof-conv")
1158 : 0 : << "EqProof::addToProof: recurse on child " << i << "\n"
1159 : 2861576 : << push;
1160 : 2861576 : children.push_back(childProof->addToProof(p, visited, assumptions));
1161 [ + - ]: 2861576 : Trace("eqproof-conv") << pop;
1162 : : }
1163 : : // Eliminate spurious premises. Reasoning below assumes no refl steps.
1164 : 710805 : cleanReflPremises(children);
1165 : : // A recursive premise may have introduced the conclusion as an assumption
1166 : : // while reconstructing a nested congruence. In that case, deriving it here
1167 : : // would overwrite the assumption with a proof that depends on itself.
1168 [ + + ]: 710805 : if (assumptions.count(conclusion))
1169 : : {
1170 : 84 : visited[d_node] = conclusion;
1171 : 84 : return conclusion;
1172 : : }
1173 : : // If any premise is of the form (= (t1 t2) false), then the transitivity
1174 : : // step may be coarse-grained and needs to be expanded. If the expansion
1175 : : // happens it also finalizes the proof of conclusion.
1176 [ + + ]: 710721 : if (!expandTransitivityForDisequalities(
1177 : : conclusion, children, p, assumptions))
1178 : : {
1179 [ - + ][ - + ]: 675590 : Assert(!children.empty());
[ - - ]
1180 : : // similarly, if a disequality is concluded because of theory reasoning,
1181 : : // the step is coarse-grained and needs to be expanded, in which case the
1182 : : // proof is finalized in the call
1183 [ + + ]: 675590 : if (!expandTransitivityForTheoryDisequalities(conclusion, children, p))
1184 : : {
1185 [ + - ]: 1351150 : Trace("eqproof-conv")
1186 : 0 : << "EqProof::addToProof: build chain for transitivity premises"
1187 : 675575 : << children << " to conclude " << conclusion << "\n";
1188 : : // Build ordered transitivity chain from children to derive the
1189 : : // conclusion
1190 : 675575 : buildTransitivityChain(conclusion, children);
1191 : 675575 : Assert(
1192 : : children.size() > 1
1193 : : || (!children.empty()
1194 : : && (children[0] == conclusion
1195 : : || children[0][1].eqNode(children[0][0]) == conclusion)));
1196 : : // Only add transitivity step if there is more than one premise in the
1197 : : // chain. Otherwise the premise will be the conclusion itself and it'll
1198 : : // already have had a step added to it when the premises were
1199 : : // recursively processed.
1200 [ + + ]: 675575 : if (children.size() > 1)
1201 : : {
1202 : 675317 : p->addStep(conclusion, ProofRule::TRANS, children, {}, true);
1203 : : }
1204 : : }
1205 : : }
1206 : 1421442 : Assert(p->hasStep(conclusion) || assumptions.count(conclusion))
1207 [ - + ][ - + ]: 710721 : << "Conclusion " << conclusion
[ - - ]
1208 : 0 : << " does not have a step in the proof neither it's an assumption.\n";
1209 : 710721 : visited[d_node] = conclusion;
1210 : 710721 : return conclusion;
1211 : 710807 : }
1212 [ - + ][ - + ]: 896601 : Assert(d_id == MERGED_THROUGH_CONGRUENCE);
[ - - ]
1213 : : // The processing below is mainly dedicated to flattening congruence steps
1214 : : // (since EqProof assumes currying) and to prossibly reconstructing the
1215 : : // conclusion in case it involves n-ary steps.
1216 [ - + ][ - - ]: 896601 : Assert(d_node.getKind() == Kind::EQUAL)
1217 [ - + ][ - + ]: 896601 : << "EqProof::addToProof: conclusion " << d_node << " is not equality\n";
[ - - ]
1218 : : // The given conclusion is taken as ground truth. If the premises do not
1219 : : // align, for example with (= (f t1) (f t2)) but a premise being (= t2 t1), we
1220 : : // use (= t1 t2) as a premise and rely on a symmetry step to justify it.
1221 : 896601 : unsigned arity = d_node[0].getNumChildren();
1222 : 896601 : Kind k = d_node[0].getKind();
1223 : 896601 : bool isNary = NodeManager::isNAryKind(k);
1224 : :
1225 : : // N-ary operators are fun. The following proof is a valid EqProof
1226 : : //
1227 : : // (= (f t1 t2 t3) (f t6 t5)) (= (f t6 t5) (f t5 t6))
1228 : : // -------------------------------------------------- TRANS
1229 : : // (= (f t1 t2 t3) (f t5 t6)) (= t4 t7)
1230 : : // ------------------------------------------------------------ CONG
1231 : : // (= (f t1 t2 t3 t4) (f t5 t6 t7))
1232 : : //
1233 : : // We modify the above proof to conclude
1234 : : //
1235 : : // (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7))
1236 : : //
1237 : : // which is a valid congruence conclusion (applications of f with the same
1238 : : // arity). For the processing below to be// performed correctly we update
1239 : : // arity to be maximal one among the two applications (4 in the above
1240 : : // example).
1241 [ + + ]: 896601 : if (d_node[0].getNumChildren() != d_node[1].getNumChildren())
1242 : : {
1243 [ - + ][ - + ]: 134 : Assert(isNary) << "We only handle congruences of apps with different "
[ - - ]
1244 : 0 : "number of children for theory n-ary operators";
1245 : 46 : arity =
1246 [ + + ][ + + ]: 180 : d_node[1].getNumChildren() < arity ? arity : d_node[1].getNumChildren();
[ - - ]
1247 [ + - ]: 268 : Trace("eqproof-conv")
1248 : 0 : << "EqProof::addToProof: Mismatching arities in cong conclusion "
1249 : 134 : << d_node << ". Use tentative arity " << arity << "\n";
1250 : : }
1251 : : // For a congruence proof of (= (f a0 ... an-1) (g b0 ... bn-1)), build a
1252 : : // transitivity matrix of n rows where the first row contains a transitivity
1253 : : // chain justifying (= f g) and the next rows (= ai bi)
1254 : 896601 : std::vector<std::vector<Node>> transitivityChildren;
1255 [ + + ]: 3373243 : for (unsigned i = 0; i < arity + 1; ++i)
1256 : : {
1257 : 2476642 : transitivityChildren.push_back(std::vector<Node>());
1258 : : }
1259 : 896601 : reduceNestedCongruence(
1260 : 896601 : arity, d_node, transitivityChildren, p, visited, assumptions, isNary);
1261 : : // The process above may inadvertently make d_node be found to be an
1262 : : // assumption of the proof. In which case the construction of the proof below
1263 : : // would add a cyclic proof. So we test for short-circuit here.
1264 [ + + ]: 896601 : if (assumptions.count(d_node))
1265 : : {
1266 : 2 : visited[d_node] = d_node;
1267 : 2 : return d_node;
1268 : : }
1269 : : // Congruences over n-ary operators may require changing the conclusion (as in
1270 : : // the above example). This is handled in a general manner below according to
1271 : : // whether the transitivity matrix computed by reduceNestedCongruence contains
1272 : : // empty rows
1273 : 896599 : Node conclusion = d_node;
1274 : 896599 : NodeManager* nm = conclusion.getNodeManager();
1275 [ + + ]: 896599 : if (isNary)
1276 : : {
1277 : 492698 : unsigned emptyRows = 0;
1278 [ + + ]: 1328586 : for (unsigned i = 1; i <= arity; ++i)
1279 : : {
1280 [ + + ]: 835888 : if (transitivityChildren[i].empty())
1281 : : {
1282 : 1160 : emptyRows++;
1283 : : }
1284 : : }
1285 : : // Given two n-ary applications f1:(f a0 ... an-1), f2:(f b0 ... bm-1), of
1286 : : // arities n and m, arity = max(n,m), the number emptyRows establishes the
1287 : : // sizes of the prefixes of f1 of f2 that have been equated via a
1288 : : // transitivity step. The prefixes necessarily have different sizes. The
1289 : : // suffixes have the same sizes. The new conclusion will be of the form
1290 : : // (= (f (f a0 ... ak1) ... an-1) (f (f b0 ... bk2) ... bm-1))
1291 : : // where
1292 : : // k1 = emptyRows + 1 - (arity - n)
1293 : : // k2 = emptyRows + 1 - (arity - m)
1294 : : // k1 != k2
1295 : : // n - k1 == m - k2
1296 : : // Note that by construction the equality between the first emptyRows + 1
1297 : : // arguments of each application is justified by the transitivity step in
1298 : : // the row emptyRows + 1 in the matrix.
1299 : : //
1300 : : // All of the above is with the very first row in the matrix, reserved for
1301 : : // justifying the equality between the functions, which is not necessary in
1302 : : // the n-ary case, notwithstanding.
1303 [ + + ]: 492698 : if (emptyRows > 0)
1304 : : {
1305 [ + - ]: 1736 : Trace("eqproof-conv")
1306 : 0 : << "EqProof::addToProof: Found " << emptyRows
1307 : 868 : << " empty rows. Rebuild conclusion " << d_node << "\n";
1308 : : // New transitivity matrix is as before except that the empty rows in the
1309 : : // beginning are eliminated, as the new arity is the maximal arity among
1310 : : // the applications minus the number of empty rows.
1311 : : std::vector<std::vector<Node>> newTransitivityChildren{
1312 : 868 : transitivityChildren.begin() + 1 + emptyRows,
1313 : 868 : transitivityChildren.end()};
1314 : 868 : transitivityChildren.clear();
1315 : 868 : transitivityChildren.push_back(std::vector<Node>());
1316 : 868 : transitivityChildren.insert(transitivityChildren.end(),
1317 : : newTransitivityChildren.begin(),
1318 : : newTransitivityChildren.end());
1319 : : unsigned arityPrefix1 =
1320 : 868 : emptyRows + 1 - (arity - d_node[0].getNumChildren());
1321 [ - + ][ - - ]: 1736 : Assert(arityPrefix1 < d_node[0].getNumChildren())
1322 : 0 : << "arityPrefix1 " << arityPrefix1 << " not smaller than "
1323 : 868 : << d_node[0] << "'s arity " << d_node[0].getNumChildren() << "\n";
1324 : : unsigned arityPrefix2 =
1325 : 868 : emptyRows + 1 - (arity - d_node[1].getNumChildren());
1326 [ - + ][ - - ]: 1736 : Assert(arityPrefix2 < d_node[1].getNumChildren())
1327 : 0 : << "arityPrefix2 " << arityPrefix2 << " not smaller than "
1328 : 868 : << d_node[1] << "'s arity " << d_node[1].getNumChildren() << "\n";
1329 [ + - ]: 1736 : Trace("eqproof-conv") << "EqProof::addToProof: New internal "
1330 : 0 : "applications with arities "
1331 : 868 : << arityPrefix1 << ", " << arityPrefix2 << ":\n";
1332 : 868 : std::vector<Node> childrenPrefix1{d_node[0].begin(),
1333 : 1736 : d_node[0].begin() + arityPrefix1};
1334 : 868 : std::vector<Node> childrenPrefix2{d_node[1].begin(),
1335 : 1736 : d_node[1].begin() + arityPrefix2};
1336 : 868 : Node newFirstChild1 = nm->mkNode(k, childrenPrefix1);
1337 : 868 : Node newFirstChild2 = nm->mkNode(k, childrenPrefix2);
1338 [ + - ]: 1736 : Trace("eqproof-conv")
1339 : 868 : << "EqProof::addToProof:\t " << newFirstChild1 << "\n";
1340 [ + - ]: 1736 : Trace("eqproof-conv")
1341 : 868 : << "EqProof::addToProof:\t " << newFirstChild2 << "\n";
1342 : 2604 : std::vector<Node> newChildren1{newFirstChild1};
1343 : 1736 : newChildren1.insert(newChildren1.end(),
1344 : 1736 : d_node[0].begin() + arityPrefix1,
1345 : : d_node[0].end());
1346 : 2604 : std::vector<Node> newChildren2{newFirstChild2};
1347 : 1736 : newChildren2.insert(newChildren2.end(),
1348 : 1736 : d_node[1].begin() + arityPrefix2,
1349 : : d_node[1].end());
1350 [ + + ][ - - ]: 4340 : conclusion = nm->mkNode(
1351 : : Kind::EQUAL,
1352 : 3472 : {nm->mkNode(k, newChildren1), nm->mkNode(k, newChildren2)});
1353 : : // update arity
1354 [ - + ][ - + ]: 868 : Assert((arity - emptyRows) == conclusion[0].getNumChildren());
[ - - ]
1355 : 868 : arity = arity - emptyRows;
1356 [ + - ]: 1736 : Trace("eqproof-conv")
1357 : 868 : << "EqProof::addToProof: New conclusion " << conclusion << "\n";
1358 : 868 : }
1359 : : }
1360 [ - + ]: 896599 : if (TraceIsOn("eqproof-conv"))
1361 : : {
1362 [ - - ]: 0 : Trace("eqproof-conv")
1363 : 0 : << "EqProof::addToProof: premises from reduced cong of " << conclusion
1364 : 0 : << ":\n";
1365 [ - - ]: 0 : for (unsigned i = 0; i <= arity; ++i)
1366 : : {
1367 [ - - ]: 0 : Trace("eqproof-conv") << "EqProof::addToProof:\t" << i
1368 : 0 : << "-th arg: " << transitivityChildren[i] << "\n";
1369 : : }
1370 : : }
1371 : 896599 : std::vector<Node> children(arity + 1);
1372 : : // Process transitivity matrix to (possibly) generate transitivity steps for
1373 : : // congruence premises (= ai bi)
1374 [ + + ]: 3372071 : for (unsigned i = 0; i <= arity; ++i)
1375 : : {
1376 : 2475472 : Node transConclusion;
1377 : : // We special case the operator case because there is only ever the need to
1378 : : // do something when in some HO case
1379 [ + + ]: 2475472 : if (i == 0)
1380 : : {
1381 : : // no justification for equality between functions, skip
1382 [ + + ]: 896599 : if (transitivityChildren[0].empty())
1383 : : {
1384 : 896254 : continue;
1385 : : }
1386 : : // HO case
1387 [ - + ][ - + ]: 345 : Assert(k == Kind::APPLY_UF) << "Congruence with different functions only "
[ - - ]
1388 : 0 : "allowed for uninterpreted functions.\n";
1389 : : transConclusion =
1390 : 345 : conclusion[0].getOperator().eqNode(conclusion[1].getOperator());
1391 : : }
1392 : : else
1393 : : {
1394 : 1578873 : transConclusion = conclusion[0][i - 1].eqNode(conclusion[1][i - 1]);
1395 : : }
1396 : 1579218 : children[i] = transConclusion;
1397 [ - + ][ - - ]: 1579218 : Assert(!transitivityChildren[i].empty())
1398 : 0 : << "EqProof::addToProof: did not add any justification for " << i
1399 [ - + ][ - + ]: 1579218 : << "-th arg of congruence " << conclusion << "\n";
[ - - ]
1400 : : // If the transitivity conclusion is a reflexivity step, just add it. Note
1401 : : // that this can happen even with the respective transitivityChildren row
1402 : : // containing several equalities in the case of (= ai bi) being the same
1403 : : // n-ary application that was justified by a congruence step, which can
1404 : : // happen in the current equality engine.
1405 [ + + ]: 1579218 : if (transConclusion[0] == transConclusion[1])
1406 : : {
1407 : 1070426 : p->addStep(transConclusion, ProofRule::REFL, {}, {transConclusion[0]});
1408 : 535213 : continue;
1409 : : }
1410 : : // Remove spurious refl steps from the premises for (= ai bi)
1411 : 1044005 : cleanReflPremises(transitivityChildren[i]);
1412 : 2088010 : Assert(transitivityChildren[i].size() > 1 || transitivityChildren[i].empty()
1413 : : || CDProof::isSame(transitivityChildren[i][0], transConclusion))
1414 : 0 : << "EqProof::addToProof: premises " << transitivityChildren[i] << "for "
1415 [ - + ][ - + ]: 1044005 : << i << "-th cong premise " << transConclusion << " don't justify it\n";
[ - - ]
1416 : 1044005 : unsigned sizeTrans = transitivityChildren[i].size();
1417 : : // If no transitivity premise left or if (= ai bi) is already present in
1418 : : // the local proof, nothing else to do. Re-deriving it can create a cyclic
1419 : : // proof when a congruence premise reuses the same fact through
1420 : : // symmetry/rewriting.
1421 [ + + ]: 1044005 : if (sizeTrans == 0 || assumptions.count(transConclusion) > 0
1422 [ + - ][ + + ]: 2088010 : || p->hasFact(transConclusion))
[ + + ][ + + ]
[ - - ]
1423 : : {
1424 : 1024358 : continue;
1425 : : }
1426 : : // If the transitivity conclusion, or its symmetric, occurs in the
1427 : : // transitivity premises, nothing to do, as it is already justified and
1428 : : // doing so again would lead to a cycle.
1429 : 19647 : bool occurs = false;
1430 [ + + ][ + - ]: 61548 : for (unsigned j = 0; j < sizeTrans && !occurs; ++j)
1431 : : {
1432 [ - + ]: 41901 : if (CDProof::isSame(transitivityChildren[i][j], transConclusion))
1433 : : {
1434 : 0 : occurs = true;
1435 : : }
1436 : : }
1437 [ + - ]: 19647 : if (!occurs)
1438 : : {
1439 : : // Build transitivity step
1440 : 19647 : buildTransitivityChain(transConclusion, transitivityChildren[i]);
1441 [ + - ]: 39294 : Trace("eqproof-conv")
1442 : 0 : << "EqProof::addToProof: adding trans step for cong premise "
1443 : 0 : << transConclusion << " with children " << transitivityChildren[i]
1444 : 19647 : << "\n";
1445 : 39294 : p->addStep(
1446 : 19647 : transConclusion, ProofRule::TRANS, transitivityChildren[i], {}, true);
1447 : : }
1448 [ + + ]: 2475472 : }
1449 : : // first-order case
1450 [ + + ]: 896599 : if (children[0].isNull())
1451 : : {
1452 : : // remove placehold for function equality case
1453 : 896254 : children.erase(children.begin());
1454 : : // Get node of the function operator over which congruence is being
1455 : : // applied.
1456 : 896254 : std::vector<Node> args;
1457 : 896254 : ProofRule r = expr::getCongRule(conclusion[0], args);
1458 : : // Add congruence step
1459 [ - + ]: 896254 : if (TraceIsOn("eqproof-conv"))
1460 : : {
1461 [ - - ]: 0 : Trace("eqproof-conv")
1462 : 0 : << "EqProof::addToProof: build cong step of " << conclusion;
1463 [ - - ]: 0 : if (!args.empty())
1464 : : {
1465 [ - - ]: 0 : Trace("eqproof-conv") << " with op " << args[0];
1466 : : }
1467 [ - - ]: 0 : Trace("eqproof-conv") << " and children " << children << "\n";
1468 : : }
1469 : 896254 : p->addStep(conclusion, r, children, args, true);
1470 : 896254 : }
1471 : : // higher-order case
1472 : : else
1473 : : {
1474 : : // Add congruence step
1475 [ + - ]: 690 : Trace("eqproof-conv") << "EqProof::addToProof: build HO-cong step of "
1476 : 0 : << conclusion << " with children " << children
1477 : 345 : << "\n";
1478 : 690 : p->addStep(conclusion,
1479 : : ProofRule::HO_CONG,
1480 : : children,
1481 : : {ProofRuleChecker::mkKindNode(nm, Kind::APPLY_UF)},
1482 : : true);
1483 : : }
1484 : : // If the conclusion of the congruence step changed due to the n-ary handling,
1485 : : // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is
1486 : : // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via
1487 : : // rewriting
1488 [ + + ]: 896599 : if (!CDProof::isSame(conclusion, d_node))
1489 : : {
1490 [ + - ]: 1736 : Trace("eqproof-conv") << "EqProof::addToProof: try to flatten via a "
1491 : 868 : << ProofRule::MACRO_SR_PRED_TRANSFORM
1492 : 0 : << " step the rebuilt conclusion " << conclusion
1493 : 868 : << " into " << d_node << "\n";
1494 : 1736 : Node res = p->getManager()->getChecker()->checkDebug(
1495 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
1496 : : {conclusion},
1497 : 868 : {d_node},
1498 : 0 : Node::null(),
1499 : 3472 : "eqproof-conv");
1500 : : // If rewriting was not able to flatten the rebuilt conclusion into the
1501 : : // original one, we give up and use a TRUST_FLATTENING_REWRITE step,
1502 : : // generating a proof for the original conclusion d_node such as
1503 : : //
1504 : : // Converted EqProof
1505 : : // ---------------------- ------------------- TRUST_FLATTENING_REWRITE
1506 : : // conclusion conclusion = d_node
1507 : : // ------------------------------------------------------- EQ_RESOLVE
1508 : : // d_node
1509 : : //
1510 : : //
1511 : : // If rewriting was able to do it, however, we just add the macro step.
1512 [ + + ]: 868 : if (res.isNull())
1513 : : {
1514 [ + - ]: 24 : Trace("eqproof-conv")
1515 : 12 : << "EqProof::addToProof: adding a trust flattening rewrite step\n";
1516 : 12 : Node bridgeEq = conclusion.eqNode(d_node);
1517 : 12 : p->addTrustedStep(bridgeEq, TrustId::FLATTENING_REWRITE, {}, {});
1518 [ + + ][ - - ]: 36 : p->addStep(d_node, ProofRule::EQ_RESOLVE, {conclusion, bridgeEq}, {});
1519 : 12 : }
1520 : : else
1521 : : {
1522 : 2568 : p->addStep(d_node,
1523 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
1524 : : {conclusion},
1525 : 856 : {d_node},
1526 : : true);
1527 : : }
1528 : 868 : }
1529 : 896599 : visited[d_node] = d_node;
1530 : 896599 : return d_node;
1531 : 896601 : }
1532 : :
1533 : : } // namespace eq
1534 : : } // Namespace theory
1535 : : } // namespace cvc5::internal
|
