diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-26 20:21:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-27 01:21:20 +0000 |
commit | 8bfa89721ce12e815abbbbe2caf87f2384bc8eb5 (patch) | |
tree | c52f175894df096a82e03545e47a9fd9d6f66304 /src/theory/uf | |
parent | bedba8e500fabeb0ac8f4f6e93af245f750a1850 (diff) |
Fix eq proof conversion for constant merged parameterized ops (#6926)
This issue arises when using the central equality engine on several regressions.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/eq_proof.cpp | 13 |
1 files 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<Node> 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<Node> transitivityChildren{congConclusion, constEquality}; |