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