From 8bfa89721ce12e815abbbbe2caf87f2384bc8eb5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Jul 2021 20:21:20 -0500 Subject: [PATCH] Fix eq proof conversion for constant merged parameterized ops (#6926) This issue arises when using the central equality engine on several regressions. --- src/theory/uf/eq_proof.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 6b2fae389..27b61e87d 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -1049,6 +1049,13 @@ Node EqProof::addToProof(CDProof* p, } // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c) Kind k = d_node[0].getKind(); + std::vector cargs; + cargs.push_back(ProofRuleChecker::mkKindNode(k)); + if (d_node[0].getMetaKind() == kind::metakind::PARAMETERIZED) + { + constChildren.insert(constChildren.begin(), d_node[0].getOperator()); + cargs.push_back(d_node[0].getOperator()); + } Node constApp = NodeManager::currentNM()->mkNode(k, constChildren); Node constEquality = constApp.eqNode(d_node[1]); Trace("eqproof-conv") << "EqProof::addToProof: adding " @@ -1060,11 +1067,7 @@ Node EqProof::addToProof(CDProof* p, Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::CONG << " step for " << congConclusion << " from " << subChildren << "\n"; - p->addStep(congConclusion, - PfRule::CONG, - {subChildren}, - {ProofRuleChecker::mkKindNode(k)}, - true); + p->addStep(congConclusion, PfRule::CONG, {subChildren}, cargs, true); Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::TRANS << " step for original conclusion " << d_node << "\n"; std::vector transitivityChildren{congConclusion, constEquality}; -- 2.30.2