1 /********************* */
4 ** Top contributors (to current version):
5 ** Haniel Barbosa, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of a proof as produced by the equality engine.
16 #include "theory/uf/eq_proof.h"
18 #include "base/configuration.h"
19 #include "expr/proof.h"
20 #include "options/uf_options.h"
26 void EqProof::debug_print(const char* c
, unsigned tb
) const
33 void EqProof::debug_print(std::ostream
& os
, unsigned tb
) const
35 for (unsigned i
= 0; i
< tb
; i
++)
40 if (d_children
.empty() && d_node
.isNull())
48 for (unsigned i
= 0; i
< tb
+ 1; ++i
)
52 os
<< d_node
<< (!d_children
.empty() ? "," : "");
54 unsigned size
= d_children
.size();
55 for (unsigned i
= 0; i
< size
; ++i
)
58 d_children
[i
]->debug_print(os
, tb
+ 1);
61 for (unsigned j
= 0; j
< tb
+ 1; ++j
)
70 for (unsigned i
= 0; i
< tb
; ++i
)
75 os
<< ")" << std::endl
;
78 void EqProof::cleanReflPremises(std::vector
<Node
>& premises
) const
80 std::vector
<Node
> newPremises
;
81 unsigned size
= premises
.size();
82 for (unsigned i
= 0; i
< size
; ++i
)
84 if (premises
[i
][0] == premises
[i
][1])
88 newPremises
.push_back(premises
[i
]);
90 if (newPremises
.size() != size
)
92 Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed "
93 << (newPremises
.size() >= size
94 ? newPremises
.size() - size
96 << " refl premises from " << premises
<< "\n";
98 premises
.insert(premises
.end(), newPremises
.begin(), newPremises
.end());
99 Trace("eqproof-conv") << "EqProof::cleanReflPremises: new premises "
104 bool EqProof::expandTransitivityForDisequalities(
106 std::vector
<Node
>& premises
,
108 std::unordered_set
<Node
, NodeHashFunction
>& assumptions
) const
110 Trace("eqproof-conv")
111 << "EqProof::expandTransitivityForDisequalities: check if need "
112 "to expand transitivity step to conclude "
113 << conclusion
<< " from premises " << premises
<< "\n";
114 // Check premises to see if any of the form (= (= t1 t2) false), modulo
116 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 unsigned termPos
= 2, offending
= size
;
120 for (unsigned i
= 0; i
< size
; ++i
)
122 Assert(premises
[i
].getKind() == kind::EQUAL
);
123 for (unsigned j
= 0; j
< 2; ++j
)
125 if (premises
[i
][j
].getKind() == kind::CONST_BOOLEAN
126 && !premises
[i
][j
].getConst
<bool>()
127 && premises
[i
][1 - j
].getKind() == kind::EQUAL
)
129 // there is only one offending equality
130 Assert(offending
== size
);
137 // if no equality of the searched form, nothing to do
138 if (offending
== size
)
142 NodeManager
* nm
= NodeManager::currentNM();
143 Assert(termPos
== 0 || termPos
== 1);
144 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found "
145 "offending equality at index "
146 << offending
<< " : " << premises
[offending
] << "\n";
147 // collect the premises to be used in the expansion, which are all but the
149 std::vector
<Node
> expansionPremises
;
150 for (unsigned i
= 0; i
< size
; ++i
)
154 expansionPremises
.push_back(premises
[i
]);
157 // Eliminate spurious premises. Reasoning below assumes no refl steps.
158 cleanReflPremises(expansionPremises
);
159 Assert(!expansionPremises
.empty());
160 // Check if we are in the substitution case
161 Node expansionConclusion
;
162 std::vector
<Node
> substPremises
;
163 bool inSubstCase
= false, substConclusionInReverseOrder
= false;
164 if ((conclusion
[0].getKind() == kind::CONST_BOOLEAN
)
165 != (conclusion
[1].getKind() == kind::CONST_BOOLEAN
))
168 // reorder offending premise if constant is the first argument
171 premises
[offending
] =
172 premises
[offending
][1].eqNode(premises
[offending
][0]);
174 // reorder conclusion if constant is the first argument
175 conclusion
= conclusion
[1].getKind() == kind::CONST_BOOLEAN
177 : conclusion
[1].eqNode(conclusion
[0]);
178 // equality term in premise disequality
179 Node premiseTermEq
= premises
[offending
][0];
180 // equality term in conclusion disequality
181 Node conclusionTermEq
= conclusion
[0];
182 Trace("eqproof-conv")
183 << "EqProof::expandTransitivityForDisequalities: Substitition "
184 "case. Need to build subst from "
185 << premiseTermEq
<< " to " << conclusionTermEq
<< "\n";
186 // If only one argument in the premise is substituted, premiseTermEq and
187 // conclusionTermEq will share one argument and the other argument change
188 // defines the single substitution. Otherwise both arguments are replaced,
189 // so there are two substitutions.
190 std::vector
<Node
> subs
[2];
191 subs
[0].push_back(premiseTermEq
[0]);
192 subs
[1].push_back(premiseTermEq
[1]);
193 // which of the arguments of premiseTermEq, if any, is equal to one argument
194 // of conclusionTermEq
196 for (unsigned i
= 0; i
< 2; ++i
)
198 for (unsigned j
= 0; j
< 2; ++j
)
200 if (premiseTermEq
[i
] == conclusionTermEq
[j
])
204 subs
[i
].push_back(conclusionTermEq
[j
]);
205 // sub that changes argument
206 subs
[1 - i
].push_back(conclusionTermEq
[1 - j
]);
207 // wither e.g. (= t1 t2), with sub t1->t3, becomes (= t2 t3)
208 substConclusionInReverseOrder
= i
!= j
;
213 // simple case of single substitution
217 // (= (= t1 t2) false) (= t1 x1) ... (= xn t3)
218 // -------------------------------------------- EQP::TR
219 // (= (= t3 t2) false)
222 // (= t1 x1) ... (= xn t3) - expansion premises
223 // ------------------------ TRANS
224 // (= t1 t3) - expansion conclusion
226 // will be the expansion made to justify the substitution for t1->t3.
227 expansionConclusion
= subs
[1 - equalArg
][0].eqNode(subs
[1 - equalArg
][1]);
228 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
229 "Need to expand premises into "
230 << expansionConclusion
<< "\n";
231 // add refl step for the substitition t2->t2
232 p
->addStep(subs
[equalArg
][0].eqNode(subs
[equalArg
][1]),
235 {subs
[equalArg
][0]});
239 // Hard case. We determine, and justify, the substitutions t1->t3/t4 and
240 // t2->t3/t4 based on the expansion premises.
241 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
242 "Need two substitutions. Look for "
243 << premiseTermEq
[0] << " and " << premiseTermEq
[1]
244 << " in premises " << expansionPremises
<< "\n";
245 Assert(expansionPremises
.size() >= 2)
246 << "Less than 2 expansion premises for substituting BOTH terms in "
247 "disequality.\nDisequality: "
248 << premises
[offending
]
249 << "\nExpansion premises: " << expansionPremises
250 << "\nConclusion: " << conclusion
<< "\n";
251 // Easier case where we can determine the substitutions by directly
252 // looking at the premises, i.e. the two expansion premises are for
253 // example (= t1 t3) and (= t2 t4)
254 if (expansionPremises
.size() == 2)
256 // iterate over args to be substituted
257 for (unsigned i
= 0; i
< 2; ++i
)
259 // iterate over premises
260 for (unsigned j
= 0; j
< 2; ++j
)
262 // iterate over args in premise
263 for (unsigned k
= 0; k
< 2; ++k
)
265 if (premiseTermEq
[i
] == expansionPremises
[j
][k
])
267 subs
[i
].push_back(expansionPremises
[j
][1 - k
]);
272 Assert(subs
[i
].size() == 2)
273 << " did not find term " << subs
[i
][0] << "\n";
274 // check if argument to be substituted is in the same order in the
276 substConclusionInReverseOrder
=
277 premiseTermEq
[i
] != conclusionTermEq
[i
];
282 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
283 "Build transitivity chains "
284 "for two subs among more than 2 premises: "
285 << expansionPremises
<< "\n";
286 // Hardest case. Try building a transitivity chain for (= t1 t3). If it
287 // can be built, use the remaining expansion premises to build a chain
288 // for (= t2 t4). Otherwise build it for (= t1 t4) and then build it for
289 // (= t2 t3). It should always succeed.
290 subs
[0].push_back(conclusionTermEq
[0]);
291 subs
[1].push_back(conclusionTermEq
[1]);
292 for (unsigned i
= 0; i
< 2; ++i
)
294 // copy premises, since buildTransitivityChain is destructive
295 std::vector
<Node
> copy1ofExpPremises(expansionPremises
.begin(),
296 expansionPremises
.end());
297 Node transConclusion1
= subs
[0][0].eqNode(subs
[0][1]);
298 if (!buildTransitivityChain(transConclusion1
, copy1ofExpPremises
))
301 << "Couldn't find sub at all for substituting BOTH terms in "
302 "disequality.\nDisequality: "
303 << premises
[offending
]
304 << "\nExpansion premises: " << expansionPremises
305 << "\nConclusion: " << conclusion
<< "\n";
306 // Failed. So flip sub and try again
307 subs
[0][1] = conclusionTermEq
[1];
308 subs
[1][1] = conclusionTermEq
[0];
309 substConclusionInReverseOrder
= false;
313 std::vector
<Node
> copy2ofExpPremises(expansionPremises
.begin(),
314 expansionPremises
.end());
315 Node transConclusion2
= subs
[1][0].eqNode(subs
[1][1]);
316 if (!buildTransitivityChain(transConclusion2
, copy2ofExpPremises
))
318 Unreachable() << "Found sub " << transConclusion1
319 << " but not other sub " << transConclusion2
320 << ".\nDisequality: " << premises
[offending
]
321 << "\nExpansion premises: " << expansionPremises
322 << "\nConclusion: " << conclusion
<< "\n";
324 Trace("eqproof-conv")
325 << "EqProof::expandTransitivityForDisequalities: Built trans "
327 "for two subs among more than 2 premises:\n";
328 Trace("eqproof-conv")
329 << "EqProof::expandTransitivityForDisequalities: "
330 << transConclusion1
<< " <- " << copy1ofExpPremises
<< "\n";
331 Trace("eqproof-conv")
332 << "EqProof::expandTransitivityForDisequalities: "
333 << transConclusion2
<< " <- " << copy2ofExpPremises
<< "\n";
334 // do transitivity steps if need be to justify each substitution
335 if (copy1ofExpPremises
.size() > 1
336 && !assumptions
.count(transConclusion1
))
339 transConclusion1
, PfRule::TRANS
, copy1ofExpPremises
, {}, true);
341 if (copy2ofExpPremises
.size() > 1
342 && !assumptions
.count(transConclusion2
))
345 transConclusion2
, PfRule::TRANS
, copy2ofExpPremises
, {}, true);
350 Trace("eqproof-conv")
351 << "EqProof::expandTransitivityForDisequalities: Built substutitions "
352 << subs
[0] << " and " << subs
[1] << " to map " << premiseTermEq
353 << " -> " << conclusionTermEq
<< "\n";
354 Assert(subs
[0][1] == conclusion
[0][0] || subs
[0][1] == conclusion
[0][1])
355 << "EqProof::expandTransitivityForDisequalities: First substitution "
356 << subs
[0] << " doest not map to conclusion " << conclusion
<< "\n";
357 Assert(subs
[1][1] == conclusion
[0][0] || subs
[1][1] == conclusion
[0][1])
358 << "EqProof::expandTransitivityForDisequalities: Second substitution "
359 << subs
[1] << " doest not map to conclusion " << conclusion
<< "\n";
360 // In the premises for the original conclusion, the substitution of
361 // premiseTermEq (= t1 t2) into conclusionTermEq (= t3 t4) is stored
362 // reversed, i.e. as (= (= t3 t4) (= t1 t2)), since the transitivity with
363 // the disequality is built as as
364 // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
365 // --------------------------------------------------------------------- TR
366 // (= (= t3 t4) false)
367 substPremises
.push_back(subs
[0][1].eqNode(subs
[0][0]));
368 substPremises
.push_back(subs
[1][1].eqNode(subs
[1][0]));
372 // In simple case the conclusion is always, modulo symmetry, false = true
373 Assert(conclusion
[0].getKind() == kind::CONST_BOOLEAN
374 && conclusion
[1].getKind() == kind::CONST_BOOLEAN
);
375 // The expansion conclusion is the same as the equality term in the
376 // disequality, which is going to be justified by a transitivity step from
377 // the expansion premises
378 expansionConclusion
= premises
[offending
][termPos
];
380 // Unless we are in the double-substitution case, the proof has the shape
382 // ... ... ... ... - expansionPremises
383 // ------------------ TRANS
384 // (= (= (t t') false) (= t'' t''') - expansionConclusion
385 // ---------------------------------------------- TRANS or PRED_TRANSFORM
388 // although note that if it's a TRANS step, (= t'' t''') will be turned into a
389 // predicate equality and the premises are ordered.
391 // We build the transitivity step for the expansionConclusion here. It being
392 // non-null marks that we are not in the double-substitution case.
393 if (!expansionConclusion
.isNull())
395 Trace("eqproof-conv")
396 << "EqProof::expandTransitivityForDisequalities: need to derive "
397 << expansionConclusion
<< " with premises " << expansionPremises
399 Assert(expansionPremises
.size() > 1
400 || expansionConclusion
== expansionPremises
.back()
401 || (expansionConclusion
[0] == expansionPremises
.back()[1]
402 && expansionConclusion
[1] == expansionPremises
.back()[0]))
403 << "single expansion premise " << expansionPremises
.back()
404 << " is not the same as expansionConclusion " << expansionConclusion
405 << " and not its symmetric\n";
406 // We track assumptions to avoid cyclic proofs, which can happen in EqProofs
409 // (= l1 "") (= "" t)
410 // ----------------------- EQP::TR
411 // (= l1 "") (= l1 t) (= (= "" t) false)
412 // ----------------------------------------------------------------- EQP::TR
415 // which would lead to the cyclic expansion proof:
417 // (= l1 "") (= l1 "") (= "" t)
418 // --------- SYMM ----------------------- TRANS
419 // (= "" l1) (= l1 t)
420 // ------------------------------------------ TRANS
422 if (expansionPremises
.size() > 1 && !assumptions
.count(expansionConclusion
))
424 // create transitivity step to derive expected premise
425 buildTransitivityChain(expansionConclusion
, expansionPremises
);
426 Trace("eqproof-conv")
427 << "EqProof::expandTransitivityForDisequalities: add transitivity "
429 << expansionConclusion
<< " with premises " << expansionPremises
431 // create expansion step
433 expansionConclusion
, PfRule::TRANS
, expansionPremises
, {}, true);
436 Trace("eqproof-conv")
437 << "EqProof::expandTransitivityForDisequalities: now derive conclusion "
440 premises
.push_back(premises
[offending
]);
443 Trace("eqproof-conv") << (substConclusionInReverseOrder
? " [inverted]"
445 << " via subsitution from " << premises
[offending
]
446 << " and (inverted subst) " << substPremises
<< "\n";
447 // By this point, for premise disequality (= (= t1 t2) false), we have
448 // potentially already built
450 // (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
451 // ------------------------ TR ------------------------ TR
452 // (= t1 t3) (= t2 t4)
454 // to justify the substitutions t1->t3 and t2->t4 (where note that if t1=t3
455 // or t2=4, the step will actually be a REFL one). Not do
457 // ----------- SYMM ----------- SYMM
458 // (= t3 t1) (= t4 t2)
459 // ---------------------------------------- CONG
460 // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
461 // --------------------------------------------------------------------- TR
462 // (= (= t3 t4) false)
464 // where note that the SYMM steps are implicitly added by CDProof.
465 Node congConclusion
= nm
->mkNode(
467 nm
->mkNode(kind::EQUAL
, substPremises
[0][0], substPremises
[1][0]),
468 premises
[offending
][0]);
469 p
->addStep(congConclusion
,
472 {ProofRuleChecker::mkKindNode(kind::EQUAL
)},
474 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
475 "congruence derived "
476 << congConclusion
<< "\n";
477 // transitivity step between that and the original premise
478 premises
.insert(premises
.begin(), congConclusion
);
479 Node transConclusion
=
480 !substConclusionInReverseOrder
482 : nm
->mkNode(kind::EQUAL
, congConclusion
[0], conclusion
[1]);
483 // check to avoid cyclic proofs
484 if (!assumptions
.count(transConclusion
))
486 p
->addStep(transConclusion
, PfRule::TRANS
, premises
, {}, true);
487 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
488 "via transitivity derived "
489 << transConclusion
<< "\n";
491 // if order is reversed, finish the proof of conclusion with
492 // (= (= t3 t4) false)
493 // --------------------- MACRO_SR_PRED_TRANSFORM
494 // (= (= t4 t3) false)
495 if (substConclusionInReverseOrder
)
497 p
->addStep(conclusion
,
498 PfRule::MACRO_SR_PRED_TRANSFORM
,
502 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
503 "via macro transform derived "
504 << conclusion
<< "\n";
509 // create TRUE_INTRO step for expansionConclusion and add it to the premises
510 Trace("eqproof-conv")
511 << " via transitivity.\nEqProof::expandTransitivityForDisequalities: "
513 << PfRule::TRUE_INTRO
<< " step for " << expansionConclusion
[0] << "\n";
514 Node newExpansionConclusion
=
515 expansionConclusion
.eqNode(nm
->mkConst
<bool>(true));
517 newExpansionConclusion
, PfRule::TRUE_INTRO
, {expansionConclusion
}, {});
518 premises
.push_back(newExpansionConclusion
);
519 Trace("eqproof-conv") << PfRule::TRANS
<< " from " << premises
<< "\n";
520 buildTransitivityChain(conclusion
, premises
);
521 // create final transitivity step
522 p
->addStep(conclusion
, PfRule::TRANS
, premises
, {}, true);
527 // TEMPORARY NOTE: This may not be enough. Worst case scenario I need to
528 // reproduce here a search for arbitrary chains between each of the variables in
529 // the conclusion and a constant
530 bool EqProof::expandTransitivityForTheoryDisequalities(
531 Node conclusion
, std::vector
<Node
>& premises
, CDProof
* p
) const
533 // whether conclusion is a disequality (= (= t1 t2) false), modulo symmetry
534 unsigned termPos
= -1;
535 for (unsigned i
= 0; i
< 2; ++i
)
537 if (conclusion
[i
].getKind() == kind::CONST_BOOLEAN
538 && !conclusion
[i
].getConst
<bool>()
539 && conclusion
[1 - i
].getKind() == kind::EQUAL
)
546 if (termPos
== static_cast<unsigned>(-1))
550 Trace("eqproof-conv")
551 << "EqProof::expandTransitivityForTheoryDisequalities: check if need "
552 "to expand transitivity step to conclude disequality "
553 << conclusion
<< " from premises " << premises
<< "\n";
555 // Check if the premises are (= t1 c1) and (= t2 c2), modulo symmetry
556 std::vector
<Node
> subChildren
, constChildren
;
557 for (unsigned i
= 0; i
< 2; ++i
)
559 Node term
= conclusion
[termPos
][i
];
560 for (const Node
& premise
: premises
)
562 for (unsigned j
= 0; j
< 2; ++j
)
564 if (premise
[j
] == term
&& premise
[1 - j
].isConst())
566 subChildren
.push_back(premise
[j
].eqNode(premise
[1 - j
]));
567 constChildren
.push_back(premise
[1 - j
]);
573 if (subChildren
.size() < 2)
578 // (= t1 c1) (= t2 c2)
579 // ------------------------- CONG ------------------- MACRO_SR_PRED_INTRO
580 // (= (= t1 t2) (= c1 c2)) (= (= c1 c2) false)
581 // --------------------------------------------------------------------- TR
582 // (= (= t1 t2) false)
583 Node constApp
= NodeManager::currentNM()->mkNode(kind::EQUAL
, constChildren
);
584 Node constEquality
= constApp
.eqNode(conclusion
[1 - termPos
]);
585 Trace("eqproof-conv")
586 << "EqProof::expandTransitivityForTheoryDisequalities: adding "
587 << PfRule::MACRO_SR_PRED_INTRO
<< " step for " << constApp
<< " = "
588 << conclusion
[1 - termPos
] << "\n";
589 p
->addStep(constEquality
, PfRule::MACRO_SR_PRED_INTRO
, {}, {constEquality
});
590 // build congruence conclusion (= (= t1 t2) (t c1 c2))
591 Node congConclusion
= conclusion
[termPos
].eqNode(constApp
);
592 Trace("eqproof-conv")
593 << "EqProof::expandTransitivityForTheoryDisequalities: adding "
594 << PfRule::CONG
<< " step for " << congConclusion
<< " from "
595 << subChildren
<< "\n";
596 p
->addStep(congConclusion
,
599 {ProofRuleChecker::mkKindNode(kind::EQUAL
)},
601 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
602 "congruence derived "
603 << congConclusion
<< "\n";
604 std::vector
<Node
> transitivityChildren
{congConclusion
, constEquality
};
605 p
->addStep(conclusion
, PfRule::TRANS
, {transitivityChildren
}, {});
609 bool EqProof::buildTransitivityChain(Node conclusion
,
610 std::vector
<Node
>& premises
) const
612 Trace("eqproof-conv") << push
613 << "EqProof::buildTransitivityChain: Build chain for "
614 << conclusion
<< " with premises " << premises
<< "\n";
615 for (unsigned i
= 0, size
= premises
.size(); i
< size
; ++i
)
617 bool occurs
= false, correctlyOrdered
= false;
618 if (conclusion
[0] == premises
[i
][0])
620 occurs
= correctlyOrdered
= true;
622 else if (conclusion
[0] == premises
[i
][1])
628 Trace("eqproof-conv")
629 << "EqProof::buildTransitivityChain: found " << conclusion
[0] << " in"
630 << (correctlyOrdered
? "" : " non-") << " ordered premise "
631 << premises
[i
] << "\n";
632 if (conclusion
[1] == premises
[i
][correctlyOrdered
? 1 : 0])
634 Trace("eqproof-conv")
635 << "EqProof::buildTransitivityChain: found " << conclusion
[1]
636 << " in same premise. Closed chain.\n"
639 premises
.push_back(conclusion
);
642 // Build chain with remaining equalities
643 std::vector
<Node
> recursivePremises
;
644 for (unsigned j
= 0; j
< size
; ++j
)
648 recursivePremises
.push_back(premises
[j
]);
652 premises
[i
][correctlyOrdered
? 1 : 0].eqNode(conclusion
[1]);
653 Trace("eqproof-conv")
654 << "EqProof::buildTransitivityChain: search recursively for "
655 << newTarget
<< "\n";
656 if (buildTransitivityChain(newTarget
, recursivePremises
))
658 Trace("eqproof-conv")
659 << "EqProof::buildTransitivityChain: closed chain with "
660 << 1 + recursivePremises
.size() << " of the original "
661 << premises
.size() << " premises\n"
664 premises
.insert(premises
.begin(),
667 : premises
[i
][1].eqNode(premises
[i
][0]));
669 premises
.end(), recursivePremises
.begin(), recursivePremises
.end());
674 Trace("eqproof-conv")
675 << "EqProof::buildTransitivityChain: Could not build chain for"
676 << conclusion
<< " with premises " << premises
<< "\n";
677 Trace("eqproof-conv") << pop
;
681 void EqProof::reduceNestedCongruence(
684 std::vector
<std::vector
<Node
>>& transitivityMatrix
,
686 std::unordered_map
<Node
, Node
, NodeHashFunction
>& visited
,
687 std::unordered_set
<Node
, NodeHashFunction
>& assumptions
,
690 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i
692 if (d_id
== MERGED_THROUGH_CONGRUENCE
)
694 Assert(d_children
.size() == 2);
695 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
696 "congruence step. Reduce second child\n"
698 transitivityMatrix
[i
].push_back(
699 d_children
[1]->addToProof(p
, visited
, assumptions
));
700 Trace("eqproof-conv")
701 << pop
<< "EqProof::reduceNestedCongruence: child conclusion "
702 << transitivityMatrix
[i
].back() << "\n";
703 // if i == 0, first child must be REFL step, standing for (= f f), which can
704 // be ignored in a first-order calculus
705 Assert(i
> 0 || d_children
[0]->d_id
== MERGED_THROUGH_REFLEXIVITY
710 Trace("eqproof-conv")
711 << "EqProof::reduceNestedCongruence: Reduce first child\n"
713 d_children
[0]->reduceNestedCongruence(i
- 1,
720 Trace("eqproof-conv") << pop
;
723 else if (d_children
[0]->d_id
!= MERGED_THROUGH_REFLEXIVITY
)
725 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: HO case. "
726 "Processing first child\n";
727 // we only handle these cases
728 Assert(d_children
[0]->d_id
== MERGED_THROUGH_EQUALITY
729 || d_children
[0]->d_id
== MERGED_THROUGH_TRANS
);
730 transitivityMatrix
[0].push_back(
731 d_children
[0]->addToProof(p
, visited
, assumptions
));
735 Assert(d_id
== MERGED_THROUGH_TRANS
)
736 << "id is " << static_cast<MergeReasonType
>(d_id
) << "\n";
737 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
738 "transitivity step.\n";
739 Assert(d_node
.isNull()
740 || d_node
[0].getNumChildren() == d_node
[1].getNumChildren() || isNary
)
741 << "Non-null (internal cong) transitivity conclusion of different arity "
742 "but not marked by isNary flag\n";
743 // If handling n-ary kinds and got a transitivity conclusion, we process it
744 // with addToProof, store the result into row i, and stop. This marks an
745 // "adjustment" of the arity, with empty rows 0..i-1 in the matrix determining
746 // the adjustment in addToProof processing the congruence of the original
747 // conclusion. See details there.
748 if (isNary
&& !d_node
.isNull())
750 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: n-ary case, "
751 "break recursion and indepedently process "
754 transitivityMatrix
[i
].push_back(addToProof(p
, visited
, assumptions
));
755 Trace("eqproof-conv") << pop
756 << "EqProof::reduceNestedCongruence: Got conclusion "
757 << transitivityMatrix
[i
].back()
758 << " from n-ary transitivity processing\n";
761 // Regular recursive processing of each transitivity premise
762 for (unsigned j
= 0, sizeTrans
= d_children
.size(); j
< sizeTrans
; ++j
)
764 if (d_children
[j
]->d_id
== MERGED_THROUGH_CONGRUENCE
)
766 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce " << j
767 << "-th transitivity congruence child\n"
769 d_children
[j
]->reduceNestedCongruence(
770 i
, conclusion
, transitivityMatrix
, p
, visited
, assumptions
, isNary
);
771 Trace("eqproof-conv") << pop
;
775 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Add " << j
776 << "-th transitivity child to proof\n"
778 transitivityMatrix
[i
].push_back(
779 d_children
[j
]->addToProof(p
, visited
, assumptions
));
780 Trace("eqproof-conv") << pop
;
785 Node
EqProof::addToProof(CDProof
* p
) const
787 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
788 std::unordered_set
<Node
, NodeHashFunction
> assumptions
;
789 Node conclusion
= addToProof(p
, cache
, assumptions
);
790 Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion
792 Trace("eqproof-conv") << "EqProof::addToProof: tracked assumptions: "
793 << assumptions
<< "\n";
794 // If conclusion t1 = tn is, modulo symmetry, of the form (= t true/false), in
795 // which t is not true/false, it must be turned into t or (not t) with
797 Node newConclusion
= conclusion
;
798 Assert(conclusion
.getKind() == kind::EQUAL
);
799 if ((conclusion
[0].getKind() == kind::CONST_BOOLEAN
)
800 != (conclusion
[1].getKind() == kind::CONST_BOOLEAN
))
802 Trace("eqproof-conv")
803 << "EqProof::addToProof: process root for TRUE/FALSE_ELIM\n";
804 // Index of constant in equality
805 unsigned constIndex
=
806 conclusion
[0].getKind() == kind::CONST_BOOLEAN
? 0 : 1;
807 // The premise for the elimination rule must have the constant as the second
808 // argument of the equality. If that's not the case, build it as such,
809 // relying on an implicit SYMM step to be added to the proof when justifying
812 constIndex
== 1 ? conclusion
: conclusion
[1].eqNode(conclusion
[0]);
813 // Determine whether TRUE_ELIM or FALSE_ELIM, depending on the constant
814 // value. The new conclusion, whether t or (not t), is also determined
817 if (conclusion
[constIndex
].getConst
<bool>())
819 elimRule
= PfRule::TRUE_ELIM
;
820 newConclusion
= conclusion
[1 - constIndex
];
824 elimRule
= PfRule::FALSE_ELIM
;
825 newConclusion
= conclusion
[1 - constIndex
].notNode();
827 // We also check if the final conclusion t / (not t) has already been
828 // justified, so that we can avoid a cyclic proof, which can be due to
829 // either t / (not t) being assumption in the original EqProof or it having
830 // a non-assumption proof step in the proof of (= t true/false).
831 if (!assumptions
.count(newConclusion
) && !p
->hasStep(newConclusion
))
833 Trace("eqproof-conv")
834 << "EqProof::addToProof: conclude " << newConclusion
<< " via "
835 << elimRule
<< " step for " << elimPremise
<< "\n";
836 p
->addStep(newConclusion
, elimRule
, {elimPremise
}, {});
839 return newConclusion
;
842 Node
EqProof::addToProof(
844 std::unordered_map
<Node
, Node
, NodeHashFunction
>& visited
,
845 std::unordered_set
<Node
, NodeHashFunction
>& assumptions
) const
847 std::unordered_map
<Node
, Node
, NodeHashFunction
>::const_iterator it
=
848 visited
.find(d_node
);
849 if (it
!= visited
.end())
851 Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node
852 << ", returning " << it
->second
<< "\n";
855 Trace("eqproof-conv") << "EqProof::addToProof: adding step for " << d_id
856 << " with conclusion " << d_node
<< "\n";
858 if (d_id
== MERGED_THROUGH_EQUALITY
)
860 // Check that no (= true/false true/false) assumptions
861 if (Configuration::isDebugBuild() && d_node
.getKind() == kind::EQUAL
)
863 for (unsigned i
= 0; i
< 2; ++i
)
865 Assert(d_node
[i
].getKind() != kind::CONST_BOOLEAN
866 || d_node
[1 - i
].getKind() != kind::CONST_BOOLEAN
)
867 << "EqProof::addToProof: fully boolean constant assumption "
868 << d_node
<< " is disallowed\n";
871 // If conclusion is (= t true/false), we add a proof step
873 // ---------------- TRUE/FALSE_INTRO
875 // according to the value of the Boolean constant
876 if (d_node
.getKind() == kind::EQUAL
877 && ((d_node
[0].getKind() == kind::CONST_BOOLEAN
)
878 != (d_node
[1].getKind() == kind::CONST_BOOLEAN
)))
880 Trace("eqproof-conv")
881 << "EqProof::addToProof: add an intro step for " << d_node
<< "\n";
882 // Index of constant in equality
883 unsigned constIndex
= d_node
[0].getKind() == kind::CONST_BOOLEAN
? 0 : 1;
884 // The premise for the intro rule is either t or (not t), according to the
888 if (d_node
[constIndex
].getConst
<bool>())
890 introRule
= PfRule::TRUE_INTRO
;
891 introPremise
= d_node
[1 - constIndex
];
892 // Track the new assumption. If it's an equality, also its symmetric
893 assumptions
.insert(introPremise
);
894 if (introPremise
.getKind() == kind::EQUAL
)
896 assumptions
.insert(introPremise
[1].eqNode(introPremise
[0]));
901 introRule
= PfRule::FALSE_INTRO
;
902 introPremise
= d_node
[1 - constIndex
].notNode();
903 // Track the new assumption. If it's a disequality, also its symmetric
904 assumptions
.insert(introPremise
);
905 if (introPremise
[0].getKind() == kind::EQUAL
)
908 introPremise
[0][1].eqNode(introPremise
[0][0]).notNode());
911 // The original assumption can be e.g. (= false (= t1 t2)) in which case
912 // the necessary proof to be built is
914 // -------------------- FALSE_INTRO
915 // (= (= t1 t2) false)
916 // -------------------- SYMM
917 // (= false (= t1 t2))
919 // with the SYMM step happening automatically whenever the assumption is
920 // used in the proof p
921 Node introConclusion
=
922 constIndex
== 1 ? d_node
: d_node
[1].eqNode(d_node
[0]);
923 p
->addStep(introConclusion
, introRule
, {introPremise
}, {});
927 p
->addStep(d_node
, PfRule::ASSUME
, {}, {d_node
});
929 // If non-equality predicate, turn into one via TRUE/FALSE intro
930 Node conclusion
= d_node
;
931 if (d_node
.getKind() != kind::EQUAL
)
933 // Track original assumption
934 assumptions
.insert(d_node
);
936 if (d_node
.getKind() == kind::NOT
)
938 intro
= PfRule::FALSE_INTRO
;
940 d_node
[0].eqNode(NodeManager::currentNM()->mkConst
<bool>(false));
944 intro
= PfRule::TRUE_INTRO
;
946 d_node
.eqNode(NodeManager::currentNM()->mkConst
<bool>(true));
948 Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro
949 << " step for " << d_node
<< "\n";
950 p
->addStep(conclusion
, intro
, {d_node
}, {});
952 // Keep track of assumptions to avoid cyclic proofs. Both the assumption and
953 // its symmetric are added
954 assumptions
.insert(conclusion
);
955 assumptions
.insert(conclusion
[1].eqNode(conclusion
[0]));
956 Trace("eqproof-conv") << "EqProof::addToProof: tracking assumptions "
957 << conclusion
<< ", (= " << conclusion
[1] << " "
958 << conclusion
[0] << ")\n";
959 visited
[d_node
] = conclusion
;
962 // Refl and laborious congruence steps for (= (f t1 ... tn) (f t1 ... tn)),
963 // which can be safely turned into reflexivity steps. These laborious
964 // congruence steps are currently generated in the equality engine because of
965 // the suboptimal handling of n-ary operators.
966 if (d_id
== MERGED_THROUGH_REFLEXIVITY
967 || (d_node
.getKind() == kind::EQUAL
&& d_node
[0] == d_node
[1]))
970 d_node
.getKind() == kind::EQUAL
? d_node
: d_node
.eqNode(d_node
);
971 p
->addStep(conclusion
, PfRule::REFL
, {}, {conclusion
[0]});
972 visited
[d_node
] = conclusion
;
975 // Equalities due to theory reasoning
976 if (d_id
== MERGED_THROUGH_CONSTANTS
)
978 Assert(!d_node
.isNull() && d_node
.getKind() == kind::EQUAL
979 && d_node
[1].isConst())
980 << ". Conclusion " << d_node
<< " from " << d_id
981 << " was expected to be (= (f t1 ... tn) c)\n";
982 Assert(!assumptions
.count(d_node
))
983 << "Conclusion " << d_node
<< " from " << d_id
<< " is an assumption\n";
984 // The step has the form
985 // [(= t1 c1)] ... [(= tn cn)]
986 // ------------------------
987 // (= (f t1 ... tn) c)
988 // where premises equating ti to constants are present when they are not
989 // already constants. Note that the premises may be in any order, e.g. with
990 // the equality for the second term being justified in the first premise.
991 // Moreover, they may be of the form (= ci ti).
993 // First recursively process premises, if any
994 std::vector
<Node
> premises
;
995 for (unsigned i
= 0; i
< d_children
.size(); ++i
)
997 Trace("eqproof-conv")
998 << "EqProof::addToProof: recurse on child " << i
<< "\n"
1000 premises
.push_back(d_children
[i
]->addToProof(p
, visited
, assumptions
));
1001 Trace("eqproof-conv") << pop
;
1003 // After building the proper premises we could build a step like
1004 // [(= t1 c1)] ... [(= tn cn)]
1005 // ---------------------------- MACRO_SR_PRED_INTRO
1006 // (= (f t1 ... tn) c)
1007 // but note that since the substitution applied by MACRO_SR_PRED_INTRO is
1008 // *not* simultenous this could lead to issues if t_{i+1} occurred in some
1009 // t_{i}. So we build proofs as
1011 // [(= t1 c1)] ... [(= tn cn)]
1012 // ------------------------------- CONG -------------- MACRO_SR_PRED_INTRO
1013 // (= (f t1 ... tn) (f c1 ... cn)) (= (f c1 ... cn) c)
1014 // ---------------------------------------------------------- TRANS
1015 // (= (f t1 ... tn) c)
1016 std::vector
<Node
> subChildren
, constChildren
;
1017 for (unsigned i
= 0, size
= d_node
[0].getNumChildren(); i
< size
; ++i
)
1019 Node term
= d_node
[0][i
];
1020 // term already is a constant, add a REFL step
1023 subChildren
.push_back(term
.eqNode(term
));
1024 p
->addStep(subChildren
.back(), PfRule::REFL
, {}, {term
});
1025 constChildren
.push_back(term
);
1028 // Build the equality (= ti ci) as a premise, finding the respective ci is
1029 // the original premises
1031 for (const Node
& premise
: premises
)
1033 Assert(premise
.getKind() == kind::EQUAL
);
1034 if (premise
[0] == term
)
1036 Assert(premise
[1].isConst());
1037 constant
= premise
[1];
1040 if (premise
[1] == term
)
1042 Assert(premise
[0].isConst());
1043 constant
= premise
[0];
1047 Assert(!constant
.isNull());
1048 subChildren
.push_back(term
.eqNode(constant
));
1049 constChildren
.push_back(constant
);
1051 // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c)
1052 Kind k
= d_node
[0].getKind();
1053 Node constApp
= NodeManager::currentNM()->mkNode(k
, constChildren
);
1054 Node constEquality
= constApp
.eqNode(d_node
[1]);
1055 Trace("eqproof-conv") << "EqProof::addToProof: adding "
1056 << PfRule::MACRO_SR_PRED_INTRO
<< " step for "
1057 << constApp
<< " = " << d_node
[1] << "\n";
1058 p
->addStep(constEquality
, PfRule::MACRO_SR_PRED_INTRO
, {}, {constEquality
});
1059 // build congruence conclusion (= (f t1 ... tn) (f c1 ... cn))
1060 Node congConclusion
= d_node
[0].eqNode(constApp
);
1061 Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::CONG
1062 << " step for " << congConclusion
<< " from "
1063 << subChildren
<< "\n";
1064 p
->addStep(congConclusion
,
1067 {ProofRuleChecker::mkKindNode(k
)},
1069 Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::TRANS
1070 << " step for original conclusion " << d_node
<< "\n";
1071 std::vector
<Node
> transitivityChildren
{congConclusion
, constEquality
};
1072 p
->addStep(d_node
, PfRule::TRANS
, {transitivityChildren
}, {});
1073 visited
[d_node
] = d_node
;
1076 // Transtivity and disequality reasoning steps
1077 if (d_id
== MERGED_THROUGH_TRANS
)
1079 Assert(d_node
.getKind() == kind::EQUAL
1080 || (d_node
.getKind() == kind::NOT
1081 && d_node
[0].getKind() == kind::EQUAL
))
1082 << "EqProof::addToProof: transitivity step conclusion " << d_node
1083 << " is not equality or negated equality\n";
1084 // If conclusion is (not (= t1 t2)) change it to (= (= t1 t2) false), which
1085 // is the correct conclusion of the equality reasoning step. A FALSE_ELIM
1086 // step to revert this is only necessary when this is the root. That step is
1087 // done in the non-recursive caller of this function.
1089 d_node
.getKind() != kind::NOT
1091 : d_node
[0].eqNode(NodeManager::currentNM()->mkConst
<bool>(false));
1092 // If the conclusion is an assumption, its derivation was spurious, so it
1093 // can be discarded. Moreover, reconstructing the step may lead to cyclic
1094 // proofs, so we *must* cut here.
1095 if (assumptions
.count(conclusion
))
1097 visited
[d_node
] = conclusion
;
1100 // Process premises recursively
1101 std::vector
<Node
> children
;
1102 for (unsigned i
= 0, size
= d_children
.size(); i
< size
; ++i
)
1104 // If one of the steps is a "fake congruence" one, marked by a null
1105 // conclusion, it must deleted. Its premises are moved down to premises of
1106 // the transitivity step.
1107 EqProof
* childProof
= d_children
[i
].get();
1108 if (childProof
->d_id
== MERGED_THROUGH_CONGRUENCE
1109 && childProof
->d_node
.isNull())
1111 Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i
1112 << " is fake cong step. Fold it.\n";
1113 Assert(childProof
->d_children
.size() == 2);
1114 Trace("eqproof-conv") << push
;
1115 for (unsigned j
= 0, sizeJ
= childProof
->d_children
.size(); j
< sizeJ
;
1118 Trace("eqproof-conv")
1119 << "EqProof::addToProof: recurse on child " << j
<< "\n"
1122 childProof
->d_children
[j
]->addToProof(p
, visited
, assumptions
));
1123 Trace("eqproof-conv") << pop
;
1125 Trace("eqproof-conv") << pop
;
1128 Trace("eqproof-conv")
1129 << "EqProof::addToProof: recurse on child " << i
<< "\n"
1131 children
.push_back(childProof
->addToProof(p
, visited
, assumptions
));
1132 Trace("eqproof-conv") << pop
;
1134 // Eliminate spurious premises. Reasoning below assumes no refl steps.
1135 cleanReflPremises(children
);
1136 // If any premise is of the form (= (t1 t2) false), then the transitivity
1137 // step may be coarse-grained and needs to be expanded. If the expansion
1138 // happens it also finalizes the proof of conclusion.
1139 if (!expandTransitivityForDisequalities(
1140 conclusion
, children
, p
, assumptions
))
1142 Assert(!children
.empty());
1143 // similarly, if a disequality is concluded because of theory reasoning,
1144 // the step is coarse-grained and needs to be expanded, in which case the
1145 // proof is finalized in the call
1146 if (!expandTransitivityForTheoryDisequalities(conclusion
, children
, p
))
1148 Trace("eqproof-conv")
1149 << "EqProof::addToProof: build chain for transitivity premises"
1150 << children
<< " to conclude " << conclusion
<< "\n";
1151 // Build ordered transitivity chain from children to derive the
1153 buildTransitivityChain(conclusion
, children
);
1156 || (!children
.empty()
1157 && (children
[0] == conclusion
1158 || children
[0][1].eqNode(children
[0][0]) == conclusion
)));
1159 // Only add transitivity step if there is more than one premise in the
1160 // chain. Otherwise the premise will be the conclusion itself and it'll
1161 // already have had a step added to it when the premises were
1162 // recursively processed.
1163 if (children
.size() > 1)
1165 p
->addStep(conclusion
, PfRule::TRANS
, children
, {}, true);
1169 Assert(p
->hasStep(conclusion
));
1170 visited
[d_node
] = conclusion
;
1173 Assert(d_id
== MERGED_THROUGH_CONGRUENCE
);
1174 // The processing below is mainly dedicated to flattening congruence steps
1175 // (since EqProof assumes currying) and to prossibly reconstructing the
1176 // conclusion in case it involves n-ary steps.
1177 Assert(d_node
.getKind() == kind::EQUAL
)
1178 << "EqProof::addToProof: conclusion " << d_node
<< " is not equality\n";
1179 // The given conclusion is taken as ground truth. If the premises do not
1180 // align, for example with (= (f t1) (f t2)) but a premise being (= t2 t1), we
1181 // use (= t1 t2) as a premise and rely on a symmetry step to justify it.
1182 unsigned arity
= d_node
[0].getNumChildren();
1183 Kind k
= d_node
[0].getKind();
1184 bool isNary
= ExprManager::isNAryKind(k
);
1186 // N-ary operators are fun. The following proof is a valid EqProof
1188 // (= (f t1 t2 t3) (f t6 t5)) (= (f t6 t5) (f t5 t6))
1189 // -------------------------------------------------- TRANS
1190 // (= (f t1 t2 t3) (f t5 t6)) (= t4 t7)
1191 // ------------------------------------------------------------ CONG
1192 // (= (f t1 t2 t3 t4) (f t5 t6 t7))
1194 // We modify the above proof to conclude
1196 // (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7))
1198 // which is a valid congruence conclusion (applications of f with the same
1199 // arity). For the processing below to be// performed correctly we update
1200 // arity to be maximal one among the two applications (4 in the above
1202 if (d_node
[0].getNumChildren() != d_node
[1].getNumChildren())
1204 Assert(isNary
) << "We only handle congruences of apps with different "
1205 "number of children for theory n-ary operators";
1207 d_node
[1].getNumChildren() < arity
? arity
: d_node
[1].getNumChildren();
1208 Trace("eqproof-conv")
1209 << "EqProof::addToProof: Mismatching arities in cong conclusion "
1210 << d_node
<< ". Use tentative arity " << arity
<< "\n";
1212 // For a congruence proof of (= (f a0 ... an-1) (g b0 ... bn-1)), build a
1213 // transitivity matrix of n rows where the first row contains a transitivity
1214 // chain justifying (= f g) and the next rows (= ai bi)
1215 std::vector
<std::vector
<Node
>> transitivityChildren
;
1216 for (unsigned i
= 0; i
< arity
+ 1; ++i
)
1218 transitivityChildren
.push_back(std::vector
<Node
>());
1220 reduceNestedCongruence(
1221 arity
, d_node
, transitivityChildren
, p
, visited
, assumptions
, isNary
);
1222 // Congruences over n-ary operators may require changing the conclusion (as in
1223 // the above example). This is handled in a general manner below according to
1224 // whether the transitivity matrix computed by reduceNestedCongruence contains
1226 Node conclusion
= d_node
;
1227 NodeManager
* nm
= NodeManager::currentNM();
1230 unsigned emptyRows
= 0;
1231 for (unsigned i
= 1; i
<= arity
; ++i
)
1233 if (transitivityChildren
[i
].empty())
1238 // Given two n-ary applications f1:(f a0 ... an-1), f2:(f b0 ... bm-1), of
1239 // arities n and m, arity = max(n,m), the number emptyRows establishes the
1240 // sizes of the prefixes of f1 of f2 that have been equated via a
1241 // transitivity step. The prefixes necessarily have different sizes. The
1242 // suffixes have the same sizes. The new conclusion will be of the form
1243 // (= (f (f a0 ... ak1) ... an-1) (f (f b0 ... bk2) ... bm-1))
1245 // k1 = emptyRows + 1 - (arity - n)
1246 // k2 = emptyRows + 1 - (arity - m)
1249 // Note that by construction the equality between the first emptyRows + 1
1250 // arguments of each application is justified by the transitivity step in
1251 // the row emptyRows + 1 in the matrix.
1253 // All of the above is with the very first row in the matrix, reserved for
1254 // justifying the equality between the functions, which is not necessary in
1255 // the n-ary case, notwithstanding.
1258 Trace("eqproof-conv")
1259 << "EqProof::addToProof: Found " << emptyRows
1260 << " empty rows. Rebuild conclusion " << d_node
<< "\n";
1261 // New transitivity matrix is as before except that the empty rows in the
1262 // beginning are eliminated, as the new arity is the maximal arity among
1263 // the applications minus the number of empty rows.
1264 std::vector
<std::vector
<Node
>> newTransitivityChildren
{
1265 transitivityChildren
.begin() + 1 + emptyRows
,
1266 transitivityChildren
.end()};
1267 transitivityChildren
.clear();
1268 transitivityChildren
.push_back(std::vector
<Node
>());
1269 transitivityChildren
.insert(transitivityChildren
.end(),
1270 newTransitivityChildren
.begin(),
1271 newTransitivityChildren
.end());
1272 unsigned arityPrefix1
=
1273 emptyRows
+ 1 - (arity
- d_node
[0].getNumChildren());
1274 Assert(arityPrefix1
< d_node
[0].getNumChildren())
1275 << "arityPrefix1 " << arityPrefix1
<< " not smaller than "
1276 << d_node
[0] << "'s arity " << d_node
[0].getNumChildren() << "\n";
1277 unsigned arityPrefix2
=
1278 emptyRows
+ 1 - (arity
- d_node
[1].getNumChildren());
1279 Assert(arityPrefix2
< d_node
[1].getNumChildren())
1280 << "arityPrefix2 " << arityPrefix2
<< " not smaller than "
1281 << d_node
[1] << "'s arity " << d_node
[1].getNumChildren() << "\n";
1282 Trace("eqproof-conv") << "EqProof::addToProof: New internal "
1283 "applications with arities "
1284 << arityPrefix1
<< ", " << arityPrefix2
<< ":\n";
1285 std::vector
<Node
> childrenPrefix1
{d_node
[0].begin(),
1286 d_node
[0].begin() + arityPrefix1
};
1287 std::vector
<Node
> childrenPrefix2
{d_node
[1].begin(),
1288 d_node
[1].begin() + arityPrefix2
};
1289 Node newFirstChild1
= nm
->mkNode(k
, childrenPrefix1
);
1290 Node newFirstChild2
= nm
->mkNode(k
, childrenPrefix2
);
1291 Trace("eqproof-conv")
1292 << "EqProof::addToProof:\t " << newFirstChild1
<< "\n";
1293 Trace("eqproof-conv")
1294 << "EqProof::addToProof:\t " << newFirstChild2
<< "\n";
1295 std::vector
<Node
> newChildren1
{newFirstChild1
};
1296 newChildren1
.insert(newChildren1
.end(),
1297 d_node
[0].begin() + arityPrefix1
,
1299 std::vector
<Node
> newChildren2
{newFirstChild2
};
1300 newChildren2
.insert(newChildren2
.end(),
1301 d_node
[1].begin() + arityPrefix2
,
1303 conclusion
= nm
->mkNode(kind::EQUAL
,
1304 nm
->mkNode(k
, newChildren1
),
1305 nm
->mkNode(k
, newChildren2
));
1307 Assert((arity
- emptyRows
) == conclusion
[0].getNumChildren());
1308 arity
= arity
- emptyRows
;
1309 Trace("eqproof-conv")
1310 << "EqProof::addToProof: New conclusion " << conclusion
<< "\n";
1313 if (Trace
.isOn("eqproof-conv"))
1315 Trace("eqproof-conv")
1316 << "EqProof::addToProof: premises from reduced cong of " << conclusion
1318 for (unsigned i
= 0; i
<= arity
; ++i
)
1320 Trace("eqproof-conv") << "EqProof::addToProof:\t" << i
1321 << "-th arg: " << transitivityChildren
[i
] << "\n";
1324 std::vector
<Node
> children(arity
+ 1);
1325 // Check if there is a justification for equality between functions (HO case)
1326 if (!transitivityChildren
[0].empty())
1328 Assert(k
== kind::APPLY_UF
) << "Congruence with different functions only "
1329 "allowed for uninterpreted functions.\n";
1332 conclusion
[0].getOperator().eqNode(conclusion
[1].getOperator());
1333 Assert(transitivityChildren
[0].size() == 1
1334 && CDProof::isSame(children
[0], transitivityChildren
[0][0]))
1335 << "Justification of operators equality is wrong: "
1336 << transitivityChildren
[0] << "\n";
1338 // Proccess transitivity matrix to (possibly) generate transitivity steps for
1339 // congruence premises (= ai bi)
1340 for (unsigned i
= 1; i
<= arity
; ++i
)
1342 Node transConclusion
= conclusion
[0][i
- 1].eqNode(conclusion
[1][i
- 1]);
1343 children
[i
] = transConclusion
;
1344 Assert(!transitivityChildren
[i
].empty())
1345 << "EqProof::addToProof: did not add any justification for " << i
1346 << "-th arg of congruence " << conclusion
<< "\n";
1347 // If the transitivity conclusion is a reflexivity step, just add it. Note
1348 // that this can happen even with the respective transitivityChildren row
1349 // containing several equalities in the case of (= ai bi) being the same
1350 // n-ary application that was justified by a congruence step, which can
1351 // happen in the current equality engine.
1352 if (transConclusion
[0] == transConclusion
[1])
1354 p
->addStep(transConclusion
, PfRule::REFL
, {}, {transConclusion
[0]});
1357 // Remove spurious refl steps from the premises for (= ai bi)
1358 cleanReflPremises(transitivityChildren
[i
]);
1359 Assert(transitivityChildren
[i
].size() > 1 || transitivityChildren
[i
].empty()
1360 || CDProof::isSame(transitivityChildren
[i
][0], transConclusion
))
1361 << "EqProof::addToProof: premises " << transitivityChildren
[i
] << "for "
1362 << i
<< "-th cong premise " << transConclusion
<< " don't justify it\n";
1363 unsigned sizeTrans
= transitivityChildren
[i
].size();
1364 // If no transitivity premise left or if (= ai bi) is an assumption (which
1365 // might lead to a cycle with a transtivity step), nothing else to do.
1366 if (sizeTrans
== 0 || assumptions
.count(transConclusion
) > 0)
1370 // If the transitivity conclusion, or its symmetric, occurs in the
1371 // transitivity premises, nothing to do, as it is already justified and
1372 // doing so again would lead to a cycle.
1373 bool occurs
= false;
1374 for (unsigned j
= 0; j
< sizeTrans
&& !occurs
; ++j
)
1376 if (CDProof::isSame(transitivityChildren
[i
][j
], transConclusion
))
1383 // Build transitivity step
1384 buildTransitivityChain(transConclusion
, transitivityChildren
[i
]);
1385 Trace("eqproof-conv")
1386 << "EqProof::addToProof: adding trans step for cong premise "
1387 << transConclusion
<< " with children " << transitivityChildren
[i
]
1390 transConclusion
, PfRule::TRANS
, transitivityChildren
[i
], {}, true);
1394 if (children
[0].isNull())
1396 // remove placehold for function equality case
1397 children
.erase(children
.begin());
1398 // Get node of the function operator over which congruence is being
1400 std::vector
<Node
> args
;
1401 args
.push_back(ProofRuleChecker::mkKindNode(k
));
1402 if (kind::metaKindOf(k
) == kind::metakind::PARAMETERIZED
)
1404 args
.push_back(conclusion
[0].getOperator());
1406 // Add congruence step
1407 Trace("eqproof-conv") << "EqProof::addToProof: build cong step of "
1408 << conclusion
<< " with op " << args
[0]
1409 << " and children " << children
<< "\n";
1410 p
->addStep(conclusion
, PfRule::CONG
, children
, args
, true);
1412 // higher-order case
1415 // Add congruence step
1416 Trace("eqproof-conv") << "EqProof::addToProof: build HO-cong step of "
1417 << conclusion
<< " with children " << children
1419 p
->addStep(conclusion
, PfRule::HO_CONG
, children
, {}, true);
1421 // If the conclusion of the congruence step changed due to the n-ary handling,
1422 // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is
1423 // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via
1425 if (conclusion
!= d_node
)
1427 Trace("eqproof-conv") << "EqProof::addToProof: add "
1428 << PfRule::MACRO_SR_PRED_TRANSFORM
1429 << " step to flatten rebuilt conclusion "
1430 << conclusion
<< "into " << d_node
<< "\n";
1432 d_node
, PfRule::MACRO_SR_PRED_TRANSFORM
, {conclusion
}, {d_node
}, true);
1434 visited
[d_node
] = d_node
;
1439 } // Namespace theory