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 "expr/proof.h"
19 #include "options/uf_options.h"
25 void EqProof::debug_print(const char* c
, unsigned tb
) const
32 void EqProof::debug_print(std::ostream
& os
, unsigned tb
) const
34 for (unsigned i
= 0; i
< tb
; i
++)
39 if (d_children
.empty() && d_node
.isNull())
47 for (unsigned i
= 0; i
< tb
+ 1; ++i
)
51 os
<< d_node
<< (!d_children
.empty() ? "," : "");
53 unsigned size
= d_children
.size();
54 for (unsigned i
= 0; i
< size
; ++i
)
57 d_children
[i
]->debug_print(os
, tb
+ 1);
60 for (unsigned j
= 0; j
< tb
+ 1; ++j
)
69 for (unsigned i
= 0; i
< tb
; ++i
)
74 os
<< ")" << std::endl
;
77 void EqProof::cleanReflPremises(std::vector
<Node
>& premises
) const
79 std::vector
<Node
> newPremises
;
80 unsigned size
= premises
.size();
81 for (unsigned i
= 0; i
< size
; ++i
)
83 if (premises
[i
][0] == premises
[i
][1])
87 newPremises
.push_back(premises
[i
]);
89 if (newPremises
.size() != size
)
91 Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed "
92 << (newPremises
.size() >= size
93 ? newPremises
.size() - size
95 << " refl premises from " << premises
<< "\n";
97 premises
.insert(premises
.end(), newPremises
.begin(), newPremises
.end());
98 Trace("eqproof-conv") << "EqProof::cleanReflPremises: new premises "
103 bool EqProof::expandTransitivityForDisequalities(
105 std::vector
<Node
>& premises
,
107 std::unordered_set
<Node
, NodeHashFunction
>& assumptions
) const
109 Trace("eqproof-conv")
110 << "EqProof::expandTransitivityForDisequalities: check if need "
111 "to expand transitivity step to conclude "
112 << conclusion
<< " from premises " << premises
<< "\n";
113 // Check premises to see if any of the form (= (= t1 t2) false), modulo
115 unsigned size
= premises
.size();
116 // termPos is, in (= (= t1 t2) false) or (= false (= t1 t2)), the position of
117 // the equality. When the i-th premise has that form, offending = i
118 unsigned termPos
= 2, offending
= size
;
119 for (unsigned i
= 0; i
< size
; ++i
)
121 Assert(premises
[i
].getKind() == kind::EQUAL
);
122 for (unsigned j
= 0; j
< 2; ++j
)
124 if (premises
[i
][j
].getKind() == kind::CONST_BOOLEAN
125 && !premises
[i
][j
].getConst
<bool>()
126 && premises
[i
][1 - j
].getKind() == kind::EQUAL
)
128 // there is only one offending equality
129 Assert(offending
== size
);
136 // if no equality of the searched form, nothing to do
137 if (offending
== size
)
141 NodeManager
* nm
= NodeManager::currentNM();
142 Assert(termPos
== 0 || termPos
== 1);
143 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found "
144 "offending equality at index "
145 << offending
<< " : " << premises
[offending
] << "\n";
146 // collect the premises to be used in the expansion, which are all but the
148 std::vector
<Node
> expansionPremises
;
149 for (unsigned i
= 0; i
< size
; ++i
)
153 expansionPremises
.push_back(premises
[i
]);
156 // Eliminate spurious premises. Reasoning below assumes no refl steps.
157 cleanReflPremises(expansionPremises
);
158 Assert(!expansionPremises
.empty());
159 // Check if we are in the substitution case
160 Node expansionConclusion
;
161 std::vector
<Node
> substPremises
;
162 bool inSubstCase
= false, substConclusionInReverseOrder
= false;
163 if ((conclusion
[0].getKind() == kind::CONST_BOOLEAN
)
164 != (conclusion
[1].getKind() == kind::CONST_BOOLEAN
))
167 // reorder offending premise if constant is the first argument
170 premises
[offending
] =
171 premises
[offending
][1].eqNode(premises
[offending
][0]);
173 // reorder conclusion if constant is the first argument
174 conclusion
= conclusion
[1].getKind() == kind::CONST_BOOLEAN
176 : conclusion
[1].eqNode(conclusion
[0]);
177 // equality term in premise disequality
178 Node premiseTermEq
= premises
[offending
][0];
179 // equality term in conclusion disequality
180 Node conclusionTermEq
= conclusion
[0];
181 Trace("eqproof-conv")
182 << "EqProof::expandTransitivityForDisequalities: Substitition "
183 "case. Need to build subst from "
184 << premiseTermEq
<< " to " << conclusionTermEq
<< "\n";
185 // If only one argument in the premise is substituted, premiseTermEq and
186 // conclusionTermEq will share one argument and the other argument change
187 // defines the single substitution. Otherwise both arguments are replaced,
188 // so there are two substitutions.
189 std::vector
<Node
> subs
[2];
190 subs
[0].push_back(premiseTermEq
[0]);
191 subs
[1].push_back(premiseTermEq
[1]);
192 // which of the arguments of premiseTermEq, if any, is equal to one argument
193 // of conclusionTermEq
195 for (unsigned i
= 0; i
< 2; ++i
)
197 for (unsigned j
= 0; j
< 2; ++j
)
199 if (premiseTermEq
[i
] == conclusionTermEq
[j
])
203 subs
[i
].push_back(conclusionTermEq
[j
]);
204 // sub that changes argument
205 subs
[1 - i
].push_back(conclusionTermEq
[1 - j
]);
206 // wither e.g. (= t1 t2), with sub t1->t3, becomes (= t2 t3)
207 substConclusionInReverseOrder
= i
!= j
;
212 // simple case of single substitution
216 // (= (= t1 t2) false) (= t1 x1) ... (= xn t3)
217 // -------------------------------------------- EQP::TR
218 // (= (= t3 t2) false)
221 // (= t1 x1) ... (= xn t3) - expansion premises
222 // ------------------------ TRANS
223 // (= t1 t3) - expansion conclusion
225 // will be the expansion made to justify the substitution for t1->t3.
226 expansionConclusion
= subs
[1 - equalArg
][0].eqNode(subs
[1 - equalArg
][1]);
227 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
228 "Need to expand premises into "
229 << expansionConclusion
<< "\n";
230 // add refl step for the substitition t2->t2
231 p
->addStep(subs
[equalArg
][0].eqNode(subs
[equalArg
][1]),
234 {subs
[equalArg
][0]});
238 // Hard case. We determine, and justify, the substitutions t1->t3/t4 and
239 // t2->t3/t4 based on the expansion premises.
240 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
241 "Need two substitutions. Look for "
242 << premiseTermEq
[0] << " and " << premiseTermEq
[1]
243 << " in premises " << expansionPremises
<< "\n";
244 Assert(expansionPremises
.size() >= 2)
245 << "Less than 2 expansion premises for substituting BOTH terms in "
246 "disequality.\nDisequality: "
247 << premises
[offending
]
248 << "\nExpansion premises: " << expansionPremises
249 << "\nConclusion: " << conclusion
<< "\n";
250 // Easier case where we can determine the substitutions by directly
251 // looking at the premises, i.e. the two expansion premises are for
252 // example (= t1 t3) and (= t2 t4)
253 if (expansionPremises
.size() == 2)
255 // iterate over args to be substituted
256 for (unsigned i
= 0; i
< 2; ++i
)
258 // iterate over premises
259 for (unsigned j
= 0; j
< 2; ++j
)
261 // iterate over args in premise
262 for (unsigned k
= 0; k
< 2; ++k
)
264 if (premiseTermEq
[i
] == expansionPremises
[j
][k
])
266 subs
[i
].push_back(expansionPremises
[j
][1 - k
]);
271 Assert(subs
[i
].size() == 2)
272 << " did not find term " << subs
[i
][0] << "\n";
273 // check if argument to be substituted is in the same order in the
275 substConclusionInReverseOrder
=
276 premiseTermEq
[i
] != conclusionTermEq
[i
];
281 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
282 "Build transitivity chains "
283 "for two subs among more than 2 premises: "
284 << expansionPremises
<< "\n";
285 // Hardest case. Try building a transitivity chain for (= t1 t3). If it
286 // can be built, use the remaining expansion premises to build a chain
287 // for (= t2 t4). Otherwise build it for (= t1 t4) and then build it for
288 // (= t2 t3). It should always succeed.
289 subs
[0].push_back(conclusionTermEq
[0]);
290 subs
[1].push_back(conclusionTermEq
[1]);
291 for (unsigned i
= 0; i
< 2; ++i
)
293 // copy premises, since buildTransitivityChain is destructive
294 std::vector
<Node
> copy1ofExpPremises(expansionPremises
.begin(),
295 expansionPremises
.end());
296 Node transConclusion1
= subs
[0][0].eqNode(subs
[0][1]);
297 if (!buildTransitivityChain(transConclusion1
, copy1ofExpPremises
))
300 << "Couldn't find sub at all for substituting BOTH terms in "
301 "disequality.\nDisequality: "
302 << premises
[offending
]
303 << "\nExpansion premises: " << expansionPremises
304 << "\nConclusion: " << conclusion
<< "\n";
305 // Failed. So flip sub and try again
306 subs
[0][1] = conclusionTermEq
[1];
307 subs
[1][1] = conclusionTermEq
[0];
308 substConclusionInReverseOrder
= false;
312 std::vector
<Node
> copy2ofExpPremises(expansionPremises
.begin(),
313 expansionPremises
.end());
314 Node transConclusion2
= subs
[1][0].eqNode(subs
[1][1]);
315 if (!buildTransitivityChain(transConclusion2
, copy2ofExpPremises
))
317 Unreachable() << "Found sub " << transConclusion1
318 << " but not other sub " << transConclusion2
319 << ".\nDisequality: " << premises
[offending
]
320 << "\nExpansion premises: " << expansionPremises
321 << "\nConclusion: " << conclusion
<< "\n";
323 Trace("eqproof-conv")
324 << "EqProof::expandTransitivityForDisequalities: Built trans "
326 "for two subs among more than 2 premises:\n";
327 Trace("eqproof-conv")
328 << "EqProof::expandTransitivityForDisequalities: "
329 << transConclusion1
<< " <- " << copy1ofExpPremises
<< "\n";
330 Trace("eqproof-conv")
331 << "EqProof::expandTransitivityForDisequalities: "
332 << transConclusion2
<< " <- " << copy2ofExpPremises
<< "\n";
333 // do transitivity steps if need be to justify each substitution
334 if (copy1ofExpPremises
.size() > 1
335 && !assumptions
.count(transConclusion1
))
338 transConclusion1
, PfRule::TRANS
, copy1ofExpPremises
, {}, true);
340 if (copy2ofExpPremises
.size() > 1
341 && !assumptions
.count(transConclusion2
))
344 transConclusion2
, PfRule::TRANS
, copy2ofExpPremises
, {}, true);
349 Trace("eqproof-conv")
350 << "EqProof::expandTransitivityForDisequalities: Built substutitions "
351 << subs
[0] << " and " << subs
[1] << " to map " << premiseTermEq
352 << " -> " << conclusionTermEq
<< "\n";
353 Assert(subs
[0][1] == conclusion
[0][0] || subs
[0][1] == conclusion
[0][1])
354 << "EqProof::expandTransitivityForDisequalities: First substitution "
355 << subs
[0] << " doest not map to conclusion " << conclusion
<< "\n";
356 Assert(subs
[1][1] == conclusion
[0][0] || subs
[1][1] == conclusion
[0][1])
357 << "EqProof::expandTransitivityForDisequalities: Second substitution "
358 << subs
[1] << " doest not map to conclusion " << conclusion
<< "\n";
359 // In the premises for the original conclusion, the substitution of
360 // premiseTermEq (= t1 t2) into conclusionTermEq (= t3 t4) is stored
361 // reversed, i.e. as (= (= t3 t4) (= t1 t2)), since the transitivity with
362 // the disequality is built as as
363 // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
364 // --------------------------------------------------------------------- TR
365 // (= (= t3 t4) false)
366 substPremises
.push_back(subs
[0][1].eqNode(subs
[0][0]));
367 substPremises
.push_back(subs
[1][1].eqNode(subs
[1][0]));
371 // In simple case the conclusion is always, modulo symmetry, false = true
372 Assert(conclusion
[0].getKind() == kind::CONST_BOOLEAN
373 && conclusion
[1].getKind() == kind::CONST_BOOLEAN
);
374 // The expansion conclusion is the same as the equality term in the
375 // disequality, which is going to be justified by a transitivity step from
376 // the expansion premises
377 expansionConclusion
= premises
[offending
][termPos
];
379 // Unless we are in the double-substitution case, the proof has the shape
381 // ... ... ... ... - expansionPremises
382 // ------------------ TRANS
383 // (= (= (t t') false) (= t'' t''') - expansionConclusion
384 // ---------------------------------------------- TRANS or PRED_TRANSFORM
387 // although note that if it's a TRANS step, (= t'' t''') will be turned into a
388 // predicate equality and the premises are ordered.
390 // We build the transitivity step for the expansionConclusion here. It being
391 // non-null marks that we are not in the double-substitution case.
392 if (!expansionConclusion
.isNull())
394 Trace("eqproof-conv")
395 << "EqProof::expandTransitivityForDisequalities: need to derive "
396 << expansionConclusion
<< " with premises " << expansionPremises
398 Assert(expansionPremises
.size() > 1
399 || expansionConclusion
== expansionPremises
.back()
400 || (expansionConclusion
[0] == expansionPremises
.back()[1]
401 && expansionConclusion
[1] == expansionPremises
.back()[0]))
402 << "single expansion premise " << expansionPremises
.back()
403 << " is not the same as expansionConclusion " << expansionConclusion
404 << " and not its symmetric\n";
405 // We track assumptions to avoid cyclic proofs, which can happen in EqProofs
408 // (= l1 "") (= "" t)
409 // ----------------------- EQP::TR
410 // (= l1 "") (= l1 t) (= (= "" t) false)
411 // ----------------------------------------------------------------- EQP::TR
414 // which would lead to the cyclic expansion proof:
416 // (= l1 "") (= l1 "") (= "" t)
417 // --------- SYMM ----------------------- TRANS
418 // (= "" l1) (= l1 t)
419 // ------------------------------------------ TRANS
421 if (expansionPremises
.size() > 1 && !assumptions
.count(expansionConclusion
))
423 // create transitivity step to derive expected premise
424 buildTransitivityChain(expansionConclusion
, expansionPremises
);
425 Trace("eqproof-conv")
426 << "EqProof::expandTransitivityForDisequalities: add transitivity "
428 << expansionConclusion
<< " with premises " << expansionPremises
430 // create expansion step
432 expansionConclusion
, PfRule::TRANS
, expansionPremises
, {}, true);
435 Trace("eqproof-conv")
436 << "EqProof::expandTransitivityForDisequalities: now derive conclusion "
439 premises
.push_back(premises
[offending
]);
442 Trace("eqproof-conv") << (substConclusionInReverseOrder
? " [inverted]"
444 << " via subsitution from " << premises
[offending
]
445 << " and (inverted subst) " << substPremises
<< "\n";
446 // By this point, for premise disequality (= (= t1 t2) false), we have
447 // potentially already built
449 // (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
450 // ------------------------ TR ------------------------ TR
451 // (= t1 t3) (= t2 t4)
453 // to justify the substitutions t1->t3 and t2->t4 (where note that if t1=t3
454 // or t2=4, the step will actually be a REFL one). Not do
456 // ----------- SYMM ----------- SYMM
457 // (= t3 t1) (= t4 t2)
458 // ---------------------------------------- CONG
459 // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
460 // --------------------------------------------------------------------- TR
461 // (= (= t3 t4) false)
463 // where note that the SYMM steps are implicitly added by CDProof.
464 Node congConclusion
= nm
->mkNode(
466 nm
->mkNode(kind::EQUAL
, substPremises
[0][0], substPremises
[1][0]),
467 premises
[offending
][0]);
468 p
->addStep(congConclusion
,
471 {ProofRuleChecker::mkKindNode(kind::EQUAL
)},
473 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
474 "congruence derived "
475 << congConclusion
<< "\n";
476 // transitivity step between that and the original premise
477 premises
.insert(premises
.begin(), congConclusion
);
478 Node transConclusion
=
479 !substConclusionInReverseOrder
481 : nm
->mkNode(kind::EQUAL
, congConclusion
[0], conclusion
[1]);
482 // check to avoid cyclic proofs
483 if (!assumptions
.count(transConclusion
))
485 p
->addStep(transConclusion
, PfRule::TRANS
, premises
, {}, true);
486 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
487 "via transitivity derived "
488 << transConclusion
<< "\n";
490 // if order is reversed, finish the proof of conclusion with
491 // (= (= t3 t4) false)
492 // --------------------- MACRO_SR_PRED_TRANSFORM
493 // (= (= t4 t3) false)
494 if (substConclusionInReverseOrder
)
496 p
->addStep(conclusion
,
497 PfRule::MACRO_SR_PRED_TRANSFORM
,
501 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
502 "via macro transform derived "
503 << conclusion
<< "\n";
508 // create TRUE_INTRO step for expansionConclusion and add it to the premises
509 Trace("eqproof-conv")
510 << " via transitivity.\nEqProof::expandTransitivityForDisequalities: "
512 << PfRule::TRUE_INTRO
<< " step for " << expansionConclusion
[0] << "\n";
513 Node newExpansionConclusion
=
514 expansionConclusion
.eqNode(nm
->mkConst
<bool>(true));
516 newExpansionConclusion
, PfRule::TRUE_INTRO
, {expansionConclusion
}, {});
517 premises
.push_back(newExpansionConclusion
);
518 Trace("eqproof-conv") << PfRule::TRANS
<< " from " << premises
<< "\n";
519 buildTransitivityChain(conclusion
, premises
);
520 // create final transitivity step
521 p
->addStep(conclusion
, PfRule::TRANS
, premises
, {}, true);
526 // TEMPORARY NOTE: This may not be enough. Worst case scenario I need to
527 // reproduce here a search for arbitrary chains between each of the variables in
528 // the conclusion and a constant
529 bool EqProof::expandTransitivityForTheoryDisequalities(
530 Node conclusion
, std::vector
<Node
>& premises
, CDProof
* p
) const
532 // whether conclusion is a disequality (= (= t1 t2) false), modulo symmetry
533 unsigned termPos
= -1;
534 for (unsigned i
= 0; i
< 2; ++i
)
536 if (conclusion
[i
].getKind() == kind::CONST_BOOLEAN
537 && !conclusion
[i
].getConst
<bool>()
538 && conclusion
[1 - i
].getKind() == kind::EQUAL
)
545 if (termPos
== static_cast<unsigned>(-1))
549 Trace("eqproof-conv")
550 << "EqProof::expandTransitivityForTheoryDisequalities: check if need "
551 "to expand transitivity step to conclude disequality "
552 << conclusion
<< " from premises " << premises
<< "\n";
554 // Check if the premises are (= t1 c1) and (= t2 c2), modulo symmetry
555 std::vector
<Node
> subChildren
, constChildren
;
556 for (unsigned i
= 0; i
< 2; ++i
)
558 Node term
= conclusion
[termPos
][i
];
559 for (const Node
& premise
: premises
)
561 for (unsigned j
= 0; j
< 2; ++j
)
563 if (premise
[j
] == term
&& premise
[1 - j
].isConst())
565 subChildren
.push_back(premise
[j
].eqNode(premise
[1 - j
]));
566 constChildren
.push_back(premise
[1 - j
]);
572 if (subChildren
.size() < 2)
577 // (= t1 c1) (= t2 c2)
578 // ------------------------- CONG ------------------- MACRO_SR_PRED_INTRO
579 // (= (= t1 t2) (= c1 c2)) (= (= c1 c2) false)
580 // --------------------------------------------------------------------- TR
581 // (= (= t1 t2) false)
582 Node constApp
= NodeManager::currentNM()->mkNode(kind::EQUAL
, constChildren
);
583 Node constEquality
= constApp
.eqNode(conclusion
[1 - termPos
]);
584 Trace("eqproof-conv")
585 << "EqProof::expandTransitivityForTheoryDisequalities: adding "
586 << PfRule::MACRO_SR_PRED_INTRO
<< " step for " << constApp
<< " = "
587 << conclusion
[1 - termPos
] << "\n";
588 p
->addStep(constEquality
, PfRule::MACRO_SR_PRED_INTRO
, {}, {constEquality
});
589 // build congruence conclusion (= (= t1 t2) (t c1 c2))
590 Node congConclusion
= conclusion
[termPos
].eqNode(constApp
);
591 Trace("eqproof-conv")
592 << "EqProof::expandTransitivityForTheoryDisequalities: adding "
593 << PfRule::CONG
<< " step for " << congConclusion
<< " from "
594 << subChildren
<< "\n";
595 p
->addStep(congConclusion
,
598 {ProofRuleChecker::mkKindNode(kind::EQUAL
)},
600 Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
601 "congruence derived "
602 << congConclusion
<< "\n";
603 std::vector
<Node
> transitivityChildren
{congConclusion
, constEquality
};
604 p
->addStep(conclusion
, PfRule::TRANS
, {transitivityChildren
}, {});
608 bool EqProof::buildTransitivityChain(Node conclusion
,
609 std::vector
<Node
>& premises
) const
611 Trace("eqproof-conv") << push
612 << "EqProof::buildTransitivityChain: Build chain for "
613 << conclusion
<< " with premises " << premises
<< "\n";
614 for (unsigned i
= 0, size
= premises
.size(); i
< size
; ++i
)
616 bool occurs
= false, correctlyOrdered
= false;
617 if (conclusion
[0] == premises
[i
][0])
619 occurs
= correctlyOrdered
= true;
621 else if (conclusion
[0] == premises
[i
][1])
627 Trace("eqproof-conv")
628 << "EqProof::buildTransitivityChain: found " << conclusion
[0] << " in"
629 << (correctlyOrdered
? "" : " non-") << " ordered premise "
630 << premises
[i
] << "\n";
631 if (conclusion
[1] == premises
[i
][correctlyOrdered
? 1 : 0])
633 Trace("eqproof-conv")
634 << "EqProof::buildTransitivityChain: found " << conclusion
[1]
635 << " in same premise. Closed chain.\n"
638 premises
.push_back(conclusion
);
641 // Build chain with remaining equalities
642 std::vector
<Node
> recursivePremises
;
643 for (unsigned j
= 0; j
< size
; ++j
)
647 recursivePremises
.push_back(premises
[j
]);
651 premises
[i
][correctlyOrdered
? 1 : 0].eqNode(conclusion
[1]);
652 Trace("eqproof-conv")
653 << "EqProof::buildTransitivityChain: search recursively for "
654 << newTarget
<< "\n";
655 if (buildTransitivityChain(newTarget
, recursivePremises
))
657 Trace("eqproof-conv")
658 << "EqProof::buildTransitivityChain: closed chain with "
659 << 1 + recursivePremises
.size() << " of the original "
660 << premises
.size() << " premises\n"
663 premises
.insert(premises
.begin(),
666 : premises
[i
][1].eqNode(premises
[i
][0]));
668 premises
.end(), recursivePremises
.begin(), recursivePremises
.end());
673 Trace("eqproof-conv")
674 << "EqProof::buildTransitivityChain: Could not build chain for"
675 << conclusion
<< " with premises " << premises
<< "\n";
676 Trace("eqproof-conv") << pop
;
680 void EqProof::reduceNestedCongruence(
683 std::vector
<std::vector
<Node
>>& transitivityMatrix
,
685 std::unordered_map
<Node
, Node
, NodeHashFunction
>& visited
,
686 std::unordered_set
<Node
, NodeHashFunction
>& assumptions
,
689 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i
691 if (d_id
== MERGED_THROUGH_CONGRUENCE
)
693 Assert(d_children
.size() == 2);
694 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
695 "congruence step. Reduce second child\n"
697 transitivityMatrix
[i
].push_back(
698 d_children
[1]->addToProof(p
, visited
, assumptions
));
699 Trace("eqproof-conv")
700 << pop
<< "EqProof::reduceNestedCongruence: child conclusion "
701 << transitivityMatrix
[i
].back() << "\n";
702 // if i == 0, first child must be REFL step, standing for (= f f), which can
703 // be ignored in a first-order calculus
704 Assert(i
> 0 || d_children
[0]->d_id
== MERGED_THROUGH_REFLEXIVITY
709 Trace("eqproof-conv")
710 << "EqProof::reduceNestedCongruence: Reduce first child\n"
712 d_children
[0]->reduceNestedCongruence(i
- 1,
719 Trace("eqproof-conv") << pop
;
722 else if (d_children
[0]->d_id
!= MERGED_THROUGH_REFLEXIVITY
)
724 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: HO case. "
725 "Processing first child\n";
726 // we only handle these cases
727 Assert(d_children
[0]->d_id
== MERGED_THROUGH_EQUALITY
728 || d_children
[0]->d_id
== MERGED_THROUGH_TRANS
);
729 transitivityMatrix
[0].push_back(
730 d_children
[0]->addToProof(p
, visited
, assumptions
));
734 Assert(d_id
== MERGED_THROUGH_TRANS
)
735 << "id is " << static_cast<MergeReasonType
>(d_id
) << "\n";
736 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
737 "transitivity step.\n";
738 Assert(d_node
.isNull()
739 || d_node
[0].getNumChildren() == d_node
[1].getNumChildren() || isNary
)
740 << "Non-null (internal cong) transitivity conclusion of different arity "
741 "but not marked by isNary flag\n";
742 // If handling n-ary kinds and got a transitivity conclusion, we process it
743 // with addToProof, store the result into row i, and stop. This marks an
744 // "adjustment" of the arity, with empty rows 0..i-1 in the matrix determining
745 // the adjustment in addToProof processing the congruence of the original
746 // conclusion. See details there.
747 if (isNary
&& !d_node
.isNull())
749 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: n-ary case, "
750 "break recursion and indepedently process "
753 transitivityMatrix
[i
].push_back(addToProof(p
, visited
, assumptions
));
754 Trace("eqproof-conv") << pop
755 << "EqProof::reduceNestedCongruence: Got conclusion "
756 << transitivityMatrix
[i
].back()
757 << " from n-ary transitivity processing\n";
760 // Regular recursive processing of each transitivity premise
761 for (unsigned j
= 0, sizeTrans
= d_children
.size(); j
< sizeTrans
; ++j
)
763 if (d_children
[j
]->d_id
== MERGED_THROUGH_CONGRUENCE
)
765 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce " << j
766 << "-th transitivity congruence child\n"
768 d_children
[j
]->reduceNestedCongruence(
769 i
, conclusion
, transitivityMatrix
, p
, visited
, assumptions
, isNary
);
770 Trace("eqproof-conv") << pop
;
774 Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Add " << j
775 << "-th transitivity child to proof\n"
777 transitivityMatrix
[i
].push_back(
778 d_children
[j
]->addToProof(p
, visited
, assumptions
));
779 Trace("eqproof-conv") << pop
;
784 Node
EqProof::addToProof(CDProof
* p
) const
786 std::unordered_map
<Node
, Node
, NodeHashFunction
> cache
;
787 std::unordered_set
<Node
, NodeHashFunction
> assumptions
;
788 Node conclusion
= addToProof(p
, cache
, assumptions
);
789 Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion
791 Trace("eqproof-conv") << "EqProof::addToProof: tracked assumptions: "
792 << assumptions
<< "\n";
793 // If conclusion t1 = tn is, modulo symmetry, of the form (= t true/false), in
794 // which t is not true/false, it must be turned into t or (not t) with
796 Node newConclusion
= conclusion
;
797 Assert(conclusion
.getKind() == kind::EQUAL
);
798 if ((conclusion
[0].getKind() == kind::CONST_BOOLEAN
)
799 != (conclusion
[1].getKind() == kind::CONST_BOOLEAN
))
801 Trace("eqproof-conv")
802 << "EqProof::addToProof: process root for TRUE/FALSE_ELIM\n";
803 // Index of constant in equality
804 unsigned constIndex
=
805 conclusion
[0].getKind() == kind::CONST_BOOLEAN
? 0 : 1;
806 // The premise for the elimination rule must have the constant as the second
807 // argument of the equality. If that's not the case, build it as such,
808 // relying on an implicit SYMM step to be added to the proof when justifying
811 constIndex
== 1 ? conclusion
: conclusion
[1].eqNode(conclusion
[0]);
812 // Determine whether TRUE_ELIM or FALSE_ELIM, depending on the constant
813 // value. The new conclusion, whether t or (not t), is also determined
816 if (conclusion
[constIndex
].getConst
<bool>())
818 elimRule
= PfRule::TRUE_ELIM
;
819 newConclusion
= conclusion
[1 - constIndex
];
823 elimRule
= PfRule::FALSE_ELIM
;
824 newConclusion
= conclusion
[1 - constIndex
].notNode();
826 // We also check if the final conclusion t / (not t) has already been
827 // justified, so that we can avoid a cyclic proof, which can be due to
828 // either t / (not t) being assumption in the original EqProof or it having
829 // a non-assumption proof step in the proof of (= t true/false).
830 if (!assumptions
.count(newConclusion
) && !p
->hasStep(newConclusion
))
832 Trace("eqproof-conv")
833 << "EqProof::addToProof: conclude " << newConclusion
<< " via "
834 << elimRule
<< " step for " << elimPremise
<< "\n";
835 p
->addStep(newConclusion
, elimRule
, {elimPremise
}, {});
838 return newConclusion
;
841 Node
EqProof::addToProof(
843 std::unordered_map
<Node
, Node
, NodeHashFunction
>& visited
,
844 std::unordered_set
<Node
, NodeHashFunction
>& assumptions
) const
846 std::unordered_map
<Node
, Node
, NodeHashFunction
>::const_iterator it
=
847 visited
.find(d_node
);
848 if (it
!= visited
.end())
850 Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node
851 << ", returning " << it
->second
<< "\n";
854 Trace("eqproof-conv") << "EqProof::addToProof: adding step for " << d_id
855 << " with conclusion " << d_node
<< "\n";
857 if (d_id
== MERGED_THROUGH_EQUALITY
)
859 // Check that no (= true/false true/false) assumptions
860 if (Configuration::isDebugBuild() && d_node
.getKind() == kind::EQUAL
)
862 for (unsigned i
= 0; i
< 2; ++i
)
864 Assert(d_node
[i
].getKind() != kind::CONST_BOOLEAN
865 || d_node
[1 - i
].getKind() != kind::CONST_BOOLEAN
)
866 << "EqProof::addToProof: fully boolean constant assumption "
867 << d_node
<< " is disallowed\n";
870 // If conclusion is (= t true/false), we add a proof step
872 // ---------------- TRUE/FALSE_INTRO
874 // according to the value of the Boolean constant
875 if (d_node
.getKind() == kind::EQUAL
876 && ((d_node
[0].getKind() == kind::CONST_BOOLEAN
)
877 != (d_node
[1].getKind() == kind::CONST_BOOLEAN
)))
879 Trace("eqproof-conv")
880 << "EqProof::addToProof: add an intro step for " << d_node
<< "\n";
881 // Index of constant in equality
882 unsigned constIndex
= d_node
[0].getKind() == kind::CONST_BOOLEAN
? 0 : 1;
883 // The premise for the intro rule is either t or (not t), according to the
887 if (d_node
[constIndex
].getConst
<bool>())
889 introRule
= PfRule::TRUE_INTRO
;
890 introPremise
= d_node
[1 - constIndex
];
891 // Track the new assumption. If it's an equality, also its symmetric
892 assumptions
.insert(introPremise
);
893 if (introPremise
.getKind() == kind::EQUAL
)
895 assumptions
.insert(introPremise
[1].eqNode(introPremise
[0]));
900 introRule
= PfRule::FALSE_INTRO
;
901 introPremise
= d_node
[1 - constIndex
].notNode();
902 // Track the new assumption. If it's a disequality, also its symmetric
903 assumptions
.insert(introPremise
);
904 if (introPremise
[0].getKind() == kind::EQUAL
)
907 introPremise
[0][1].eqNode(introPremise
[0][0]).notNode());
910 // The original assumption can be e.g. (= false (= t1 t2)) in which case
911 // the necessary proof to be built is
913 // -------------------- FALSE_INTRO
914 // (= (= t1 t2) false)
915 // -------------------- SYMM
916 // (= false (= t1 t2))
918 // with the SYMM step happening automatically whenever the assumption is
919 // used in the proof p
920 Node introConclusion
=
921 constIndex
== 1 ? d_node
: d_node
[1].eqNode(d_node
[0]);
922 p
->addStep(introConclusion
, introRule
, {introPremise
}, {});
926 p
->addStep(d_node
, PfRule::ASSUME
, {}, {d_node
});
928 // If non-equality predicate, turn into one via TRUE/FALSE intro
929 Node conclusion
= d_node
;
930 if (d_node
.getKind() != kind::EQUAL
)
932 // Track original assumption
933 assumptions
.insert(d_node
);
935 if (d_node
.getKind() == kind::NOT
)
937 intro
= PfRule::FALSE_INTRO
;
939 d_node
[0].eqNode(NodeManager::currentNM()->mkConst
<bool>(false));
943 intro
= PfRule::TRUE_INTRO
;
945 d_node
.eqNode(NodeManager::currentNM()->mkConst
<bool>(true));
947 Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro
948 << " step for " << d_node
<< "\n";
949 p
->addStep(conclusion
, intro
, {d_node
}, {});
951 // Keep track of assumptions to avoid cyclic proofs. Both the assumption and
952 // its symmetric are added
953 assumptions
.insert(conclusion
);
954 assumptions
.insert(conclusion
[1].eqNode(conclusion
[0]));
955 Trace("eqproof-conv") << "EqProof::addToProof: tracking assumptions "
956 << conclusion
<< ", (= " << conclusion
[1] << " "
957 << conclusion
[0] << ")\n";
958 visited
[d_node
] = conclusion
;
961 // Refl and laborious congruence steps for (= (f t1 ... tn) (f t1 ... tn)),
962 // which can be safely turned into reflexivity steps. These laborious
963 // congruence steps are currently generated in the equality engine because of
964 // the suboptimal handling of n-ary operators.
965 if (d_id
== MERGED_THROUGH_REFLEXIVITY
966 || (d_node
.getKind() == kind::EQUAL
&& d_node
[0] == d_node
[1]))
969 d_node
.getKind() == kind::EQUAL
? d_node
: d_node
.eqNode(d_node
);
970 p
->addStep(conclusion
, PfRule::REFL
, {}, {conclusion
[0]});
971 visited
[d_node
] = conclusion
;
974 // Equalities due to theory reasoning
975 if (d_id
== MERGED_THROUGH_CONSTANTS
)
977 Assert(!d_node
.isNull() && d_node
.getKind() == kind::EQUAL
978 && d_node
[1].isConst())
979 << ". Conclusion " << d_node
<< " from " << d_id
980 << " was expected to be (= (f t1 ... tn) c)\n";
981 Assert(!assumptions
.count(d_node
))
982 << "Conclusion " << d_node
<< " from " << d_id
<< " is an assumption\n";
983 // The step has the form
984 // [(= t1 c1)] ... [(= tn cn)]
985 // ------------------------
986 // (= (f t1 ... tn) c)
987 // where premises equating ti to constants are present when they are not
988 // already constants. Note that the premises may be in any order, e.g. with
989 // the equality for the second term being justified in the first premise.
990 // Moreover, they may be of the form (= ci ti).
992 // First recursively process premises, if any
993 std::vector
<Node
> premises
;
994 for (unsigned i
= 0; i
< d_children
.size(); ++i
)
996 Trace("eqproof-conv")
997 << "EqProof::addToProof: recurse on child " << i
<< "\n"
999 premises
.push_back(d_children
[i
]->addToProof(p
, visited
, assumptions
));
1000 Trace("eqproof-conv") << pop
;
1002 // After building the proper premises we could build a step like
1003 // [(= t1 c1)] ... [(= tn cn)]
1004 // ---------------------------- MACRO_SR_PRED_INTRO
1005 // (= (f t1 ... tn) c)
1006 // but note that since the substitution applied by MACRO_SR_PRED_INTRO is
1007 // *not* simultenous this could lead to issues if t_{i+1} occurred in some
1008 // t_{i}. So we build proofs as
1010 // [(= t1 c1)] ... [(= tn cn)]
1011 // ------------------------------- CONG -------------- MACRO_SR_PRED_INTRO
1012 // (= (f t1 ... tn) (f c1 ... cn)) (= (f c1 ... cn) c)
1013 // ---------------------------------------------------------- TRANS
1014 // (= (f t1 ... tn) c)
1015 std::vector
<Node
> subChildren
, constChildren
;
1016 for (unsigned i
= 0, size
= d_node
[0].getNumChildren(); i
< size
; ++i
)
1018 Node term
= d_node
[0][i
];
1019 // term already is a constant, add a REFL step
1022 subChildren
.push_back(term
.eqNode(term
));
1023 p
->addStep(subChildren
.back(), PfRule::REFL
, {}, {term
});
1024 constChildren
.push_back(term
);
1027 // Build the equality (= ti ci) as a premise, finding the respective ci is
1028 // the original premises
1030 for (const Node
& premise
: premises
)
1032 Assert(premise
.getKind() == kind::EQUAL
);
1033 if (premise
[0] == term
)
1035 Assert(premise
[1].isConst());
1036 constant
= premise
[1];
1039 if (premise
[1] == term
)
1041 Assert(premise
[0].isConst());
1042 constant
= premise
[0];
1046 Assert(!constant
.isNull());
1047 subChildren
.push_back(term
.eqNode(constant
));
1048 constChildren
.push_back(constant
);
1050 // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c)
1051 Kind k
= d_node
[0].getKind();
1052 Node constApp
= NodeManager::currentNM()->mkNode(k
, constChildren
);
1053 Node constEquality
= constApp
.eqNode(d_node
[1]);
1054 Trace("eqproof-conv") << "EqProof::addToProof: adding "
1055 << PfRule::MACRO_SR_PRED_INTRO
<< " step for "
1056 << constApp
<< " = " << d_node
[1] << "\n";
1057 p
->addStep(constEquality
, PfRule::MACRO_SR_PRED_INTRO
, {}, {constEquality
});
1058 // build congruence conclusion (= (f t1 ... tn) (f c1 ... cn))
1059 Node congConclusion
= d_node
[0].eqNode(constApp
);
1060 Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::CONG
1061 << " step for " << congConclusion
<< " from "
1062 << subChildren
<< "\n";
1063 p
->addStep(congConclusion
,
1066 {ProofRuleChecker::mkKindNode(k
)},
1068 Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::TRANS
1069 << " step for original conclusion " << d_node
<< "\n";
1070 std::vector
<Node
> transitivityChildren
{congConclusion
, constEquality
};
1071 p
->addStep(d_node
, PfRule::TRANS
, {transitivityChildren
}, {});
1072 visited
[d_node
] = d_node
;
1075 // Transtivity and disequality reasoning steps
1076 if (d_id
== MERGED_THROUGH_TRANS
)
1078 Assert(d_node
.getKind() == kind::EQUAL
1079 || (d_node
.getKind() == kind::NOT
1080 && d_node
[0].getKind() == kind::EQUAL
))
1081 << "EqProof::addToProof: transitivity step conclusion " << d_node
1082 << " is not equality or negated equality\n";
1083 // If conclusion is (not (= t1 t2)) change it to (= (= t1 t2) false), which
1084 // is the correct conclusion of the equality reasoning step. A FALSE_ELIM
1085 // step to revert this is only necessary when this is the root. That step is
1086 // done in the non-recursive caller of this function.
1088 d_node
.getKind() != kind::NOT
1090 : d_node
[0].eqNode(NodeManager::currentNM()->mkConst
<bool>(false));
1091 // If the conclusion is an assumption, its derivation was spurious, so it
1092 // can be discarded. Moreover, reconstructing the step may lead to cyclic
1093 // proofs, so we *must* cut here.
1094 if (assumptions
.count(conclusion
))
1096 visited
[d_node
] = conclusion
;
1099 // Process premises recursively
1100 std::vector
<Node
> children
;
1101 for (unsigned i
= 0, size
= d_children
.size(); i
< size
; ++i
)
1103 // If one of the steps is a "fake congruence" one, marked by a null
1104 // conclusion, it must deleted. Its premises are moved down to premises of
1105 // the transitivity step.
1106 EqProof
* childProof
= d_children
[i
].get();
1107 if (childProof
->d_id
== MERGED_THROUGH_CONGRUENCE
1108 && childProof
->d_node
.isNull())
1110 Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i
1111 << " is fake cong step. Fold it.\n";
1112 Assert(childProof
->d_children
.size() == 2);
1113 Trace("eqproof-conv") << push
;
1114 for (unsigned j
= 0, sizeJ
= childProof
->d_children
.size(); j
< sizeJ
;
1117 Trace("eqproof-conv")
1118 << "EqProof::addToProof: recurse on child " << j
<< "\n"
1121 childProof
->d_children
[j
]->addToProof(p
, visited
, assumptions
));
1122 Trace("eqproof-conv") << pop
;
1124 Trace("eqproof-conv") << pop
;
1127 Trace("eqproof-conv")
1128 << "EqProof::addToProof: recurse on child " << i
<< "\n"
1130 children
.push_back(childProof
->addToProof(p
, visited
, assumptions
));
1131 Trace("eqproof-conv") << pop
;
1133 // Eliminate spurious premises. Reasoning below assumes no refl steps.
1134 cleanReflPremises(children
);
1135 // If any premise is of the form (= (t1 t2) false), then the transitivity
1136 // step may be coarse-grained and needs to be expanded. If the expansion
1137 // happens it also finalizes the proof of conclusion.
1138 if (!expandTransitivityForDisequalities(
1139 conclusion
, children
, p
, assumptions
))
1141 Assert(!children
.empty());
1142 // similarly, if a disequality is concluded because of theory reasoning,
1143 // the step is coarse-grained and needs to be expanded, in which case the
1144 // proof is finalized in the call
1145 if (!expandTransitivityForTheoryDisequalities(conclusion
, children
, p
))
1147 Trace("eqproof-conv")
1148 << "EqProof::addToProof: build chain for transitivity premises"
1149 << children
<< " to conclude " << conclusion
<< "\n";
1150 // Build ordered transitivity chain from children to derive the
1152 buildTransitivityChain(conclusion
, children
);
1155 || (!children
.empty()
1156 && (children
[0] == conclusion
1157 || children
[0][1].eqNode(children
[0][0]) == conclusion
)));
1158 // Only add transitivity step if there is more than one premise in the
1159 // chain. Otherwise the premise will be the conclusion itself and it'll
1160 // already have had a step added to it when the premises were
1161 // recursively processed.
1162 if (children
.size() > 1)
1164 p
->addStep(conclusion
, PfRule::TRANS
, children
, {}, true);
1168 Assert(p
->hasStep(conclusion
));
1169 visited
[d_node
] = conclusion
;
1172 Assert(d_id
== MERGED_THROUGH_CONGRUENCE
);
1173 // The processing below is mainly dedicated to flattening congruence steps
1174 // (since EqProof assumes currying) and to prossibly reconstructing the
1175 // conclusion in case it involves n-ary steps.
1176 Assert(d_node
.getKind() == kind::EQUAL
)
1177 << "EqProof::addToProof: conclusion " << d_node
<< " is not equality\n";
1178 // The given conclusion is taken as ground truth. If the premises do not
1179 // align, for example with (= (f t1) (f t2)) but a premise being (= t2 t1), we
1180 // use (= t1 t2) as a premise and rely on a symmetry step to justify it.
1181 unsigned arity
= d_node
[0].getNumChildren();
1182 Kind k
= d_node
[0].getKind();
1183 bool isNary
= ExprManager::isNAryKind(k
);
1185 // N-ary operators are fun. The following proof is a valid EqProof
1187 // (= (f t1 t2 t3) (f t6 t5)) (= (f t6 t5) (f t5 t6))
1188 // -------------------------------------------------- TRANS
1189 // (= (f t1 t2 t3) (f t5 t6)) (= t4 t7)
1190 // ------------------------------------------------------------ CONG
1191 // (= (f t1 t2 t3 t4) (f t5 t6 t7))
1193 // We modify the above proof to conclude
1195 // (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7))
1197 // which is a valid congruence conclusion (applications of f with the same
1198 // arity). For the processing below to be// performed correctly we update
1199 // arity to be maximal one among the two applications (4 in the above
1201 if (d_node
[0].getNumChildren() != d_node
[1].getNumChildren())
1203 Assert(isNary
) << "We only handle congruences of apps with different "
1204 "number of children for theory n-ary operators";
1206 d_node
[1].getNumChildren() < arity
? arity
: d_node
[1].getNumChildren();
1207 Trace("eqproof-conv")
1208 << "EqProof::addToProof: Mismatching arities in cong conclusion "
1209 << d_node
<< ". Use tentative arity " << arity
<< "\n";
1211 // For a congruence proof of (= (f a0 ... an-1) (g b0 ... bn-1)), build a
1212 // transitivity matrix of n rows where the first row contains a transitivity
1213 // chain justifying (= f g) and the next rows (= ai bi)
1214 std::vector
<std::vector
<Node
>> transitivityChildren
;
1215 for (unsigned i
= 0; i
< arity
+ 1; ++i
)
1217 transitivityChildren
.push_back(std::vector
<Node
>());
1219 reduceNestedCongruence(
1220 arity
, d_node
, transitivityChildren
, p
, visited
, assumptions
, isNary
);
1221 // Congruences over n-ary operators may require changing the conclusion (as in
1222 // the above example). This is handled in a general manner below according to
1223 // whether the transitivity matrix computed by reduceNestedCongruence contains
1225 Node conclusion
= d_node
;
1226 NodeManager
* nm
= NodeManager::currentNM();
1229 unsigned emptyRows
= 0;
1230 for (unsigned i
= 1; i
<= arity
; ++i
)
1232 if (transitivityChildren
[i
].empty())
1237 // Given two n-ary applications f1:(f a0 ... an-1), f2:(f b0 ... bm-1), of
1238 // arities n and m, arity = max(n,m), the number emptyRows establishes the
1239 // sizes of the prefixes of f1 of f2 that have been equated via a
1240 // transitivity step. The prefixes necessarily have different sizes. The
1241 // suffixes have the same sizes. The new conclusion will be of the form
1242 // (= (f (f a0 ... ak1) ... an-1) (f (f b0 ... bk2) ... bm-1))
1244 // k1 = emptyRows + 1 - (arity - n)
1245 // k2 = emptyRows + 1 - (arity - m)
1248 // Note that by construction the equality between the first emptyRows + 1
1249 // arguments of each application is justified by the transitivity step in
1250 // the row emptyRows + 1 in the matrix.
1252 // All of the above is with the very first row in the matrix, reserved for
1253 // justifying the equality between the functions, which is not necessary in
1254 // the n-ary case, notwithstanding.
1257 Trace("eqproof-conv")
1258 << "EqProof::addToProof: Found " << emptyRows
1259 << " empty rows. Rebuild conclusion " << d_node
<< "\n";
1260 // New transitivity matrix is as before except that the empty rows in the
1261 // beginning are eliminated, as the new arity is the maximal arity among
1262 // the applications minus the number of empty rows.
1263 std::vector
<std::vector
<Node
>> newTransitivityChildren
{
1264 transitivityChildren
.begin() + 1 + emptyRows
,
1265 transitivityChildren
.end()};
1266 transitivityChildren
.clear();
1267 transitivityChildren
.push_back(std::vector
<Node
>());
1268 transitivityChildren
.insert(transitivityChildren
.end(),
1269 newTransitivityChildren
.begin(),
1270 newTransitivityChildren
.end());
1271 unsigned arityPrefix1
=
1272 emptyRows
+ 1 - (arity
- d_node
[0].getNumChildren());
1273 Assert(arityPrefix1
< d_node
[0].getNumChildren())
1274 << "arityPrefix1 " << arityPrefix1
<< " not smaller than "
1275 << d_node
[0] << "'s arity " << d_node
[0].getNumChildren() << "\n";
1276 unsigned arityPrefix2
=
1277 emptyRows
+ 1 - (arity
- d_node
[1].getNumChildren());
1278 Assert(arityPrefix2
< d_node
[1].getNumChildren())
1279 << "arityPrefix2 " << arityPrefix2
<< " not smaller than "
1280 << d_node
[1] << "'s arity " << d_node
[1].getNumChildren() << "\n";
1281 Trace("eqproof-conv") << "EqProof::addToProof: New internal "
1282 "applications with arities "
1283 << arityPrefix1
<< ", " << arityPrefix2
<< ":\n";
1284 std::vector
<Node
> childrenPrefix1
{d_node
[0].begin(),
1285 d_node
[0].begin() + arityPrefix1
};
1286 std::vector
<Node
> childrenPrefix2
{d_node
[1].begin(),
1287 d_node
[1].begin() + arityPrefix2
};
1288 Node newFirstChild1
= nm
->mkNode(k
, childrenPrefix1
);
1289 Node newFirstChild2
= nm
->mkNode(k
, childrenPrefix2
);
1290 Trace("eqproof-conv")
1291 << "EqProof::addToProof:\t " << newFirstChild1
<< "\n";
1292 Trace("eqproof-conv")
1293 << "EqProof::addToProof:\t " << newFirstChild2
<< "\n";
1294 std::vector
<Node
> newChildren1
{newFirstChild1
};
1295 newChildren1
.insert(newChildren1
.end(),
1296 d_node
[0].begin() + arityPrefix1
,
1298 std::vector
<Node
> newChildren2
{newFirstChild2
};
1299 newChildren2
.insert(newChildren2
.end(),
1300 d_node
[1].begin() + arityPrefix2
,
1302 conclusion
= nm
->mkNode(kind::EQUAL
,
1303 nm
->mkNode(k
, newChildren1
),
1304 nm
->mkNode(k
, newChildren2
));
1306 Assert((arity
- emptyRows
) == conclusion
[0].getNumChildren());
1307 arity
= arity
- emptyRows
;
1308 Trace("eqproof-conv")
1309 << "EqProof::addToProof: New conclusion " << conclusion
<< "\n";
1312 if (Trace
.isOn("eqproof-conv"))
1314 Trace("eqproof-conv")
1315 << "EqProof::addToProof: premises from reduced cong of " << conclusion
1317 for (unsigned i
= 0; i
<= arity
; ++i
)
1319 Trace("eqproof-conv") << "EqProof::addToProof:\t" << i
1320 << "-th arg: " << transitivityChildren
[i
] << "\n";
1323 std::vector
<Node
> children(arity
+ 1);
1324 // Check if there is a justification for equality between functions (HO case)
1325 if (!transitivityChildren
[0].empty())
1327 Assert(k
== kind::APPLY_UF
) << "Congruence with different functions only "
1328 "allowed for uninterpreted functions.\n";
1331 conclusion
[0].getOperator().eqNode(conclusion
[1].getOperator());
1332 Assert(transitivityChildren
[0].size() == 1
1333 && CDProof::isSame(children
[0], transitivityChildren
[0][0]))
1334 << "Justification of operators equality is wrong: "
1335 << transitivityChildren
[0] << "\n";
1337 // Proccess transitivity matrix to (possibly) generate transitivity steps for
1338 // congruence premises (= ai bi)
1339 for (unsigned i
= 1; i
<= arity
; ++i
)
1341 Node transConclusion
= conclusion
[0][i
- 1].eqNode(conclusion
[1][i
- 1]);
1342 children
[i
] = transConclusion
;
1343 Assert(!transitivityChildren
[i
].empty())
1344 << "EqProof::addToProof: did not add any justification for " << i
1345 << "-th arg of congruence " << conclusion
<< "\n";
1346 // If the transitivity conclusion is a reflexivity step, just add it. Note
1347 // that this can happen even with the respective transitivityChildren row
1348 // containing several equalities in the case of (= ai bi) being the same
1349 // n-ary application that was justified by a congruence step, which can
1350 // happen in the current equality engine.
1351 if (transConclusion
[0] == transConclusion
[1])
1353 p
->addStep(transConclusion
, PfRule::REFL
, {}, {transConclusion
[0]});
1356 // Remove spurious refl steps from the premises for (= ai bi)
1357 cleanReflPremises(transitivityChildren
[i
]);
1358 Assert(transitivityChildren
[i
].size() > 1 || transitivityChildren
[i
].empty()
1359 || CDProof::isSame(transitivityChildren
[i
][0], transConclusion
))
1360 << "EqProof::addToProof: premises " << transitivityChildren
[i
] << "for "
1361 << i
<< "-th cong premise " << transConclusion
<< " don't justify it\n";
1362 unsigned sizeTrans
= transitivityChildren
[i
].size();
1363 // If no transitivity premise left or if (= ai bi) is an assumption (which
1364 // might lead to a cycle with a transtivity step), nothing else to do.
1365 if (sizeTrans
== 0 || assumptions
.count(transConclusion
) > 0)
1369 // If the transitivity conclusion, or its symmetric, occurs in the
1370 // transitivity premises, nothing to do, as it is already justified and
1371 // doing so again would lead to a cycle.
1372 bool occurs
= false;
1373 for (unsigned j
= 0; j
< sizeTrans
&& !occurs
; ++j
)
1375 if (CDProof::isSame(transitivityChildren
[i
][j
], transConclusion
))
1382 // Build transitivity step
1383 buildTransitivityChain(transConclusion
, transitivityChildren
[i
]);
1384 Trace("eqproof-conv")
1385 << "EqProof::addToProof: adding trans step for cong premise "
1386 << transConclusion
<< " with children " << transitivityChildren
[i
]
1389 transConclusion
, PfRule::TRANS
, transitivityChildren
[i
], {}, true);
1393 if (children
[0].isNull())
1395 // remove placehold for function equality case
1396 children
.erase(children
.begin());
1397 // Get node of the function operator over which congruence is being
1399 std::vector
<Node
> args
;
1400 args
.push_back(ProofRuleChecker::mkKindNode(k
));
1401 if (kind::metaKindOf(k
) == kind::metakind::PARAMETERIZED
)
1403 args
.push_back(conclusion
[0].getOperator());
1405 // Add congruence step
1406 Trace("eqproof-conv") << "EqProof::addToProof: build cong step of "
1407 << conclusion
<< " with op " << args
[0]
1408 << " and children " << children
<< "\n";
1409 p
->addStep(conclusion
, PfRule::CONG
, children
, args
, true);
1411 // higher-order case
1414 // Add congruence step
1415 Trace("eqproof-conv") << "EqProof::addToProof: build HO-cong step of "
1416 << conclusion
<< " with children " << children
1418 p
->addStep(conclusion
, PfRule::HO_CONG
, children
, {}, true);
1420 // If the conclusion of the congruence step changed due to the n-ary handling,
1421 // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is
1422 // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via
1424 if (conclusion
!= d_node
)
1426 Trace("eqproof-conv") << "EqProof::addToProof: add "
1427 << PfRule::MACRO_SR_PRED_TRANSFORM
1428 << " step to flatten rebuilt conclusion "
1429 << conclusion
<< "into " << d_node
<< "\n";
1431 d_node
, PfRule::MACRO_SR_PRED_TRANSFORM
, {conclusion
}, {d_node
}, true);
1433 visited
[d_node
] = d_node
;
1438 } // Namespace theory