From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 01:21:20 +0000 (-0500)
Subject: Fix eq proof conversion for constant merged parameterized ops (#6926)
X-Git-Tag: cvc5-1.0.0~1450
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8bfa89721ce12e815abbbbe2caf87f2384bc8eb5;p=cvc5.git

Fix eq proof conversion for constant merged parameterized ops (#6926)

This issue arises when using the central equality engine on several regressions.
---

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};