From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Jul 2021 21:35:21 +0000 (-0300)
Subject: Generalize congruence handling for HO in eq proofs (#6883)
X-Git-Tag: cvc5-1.0.0~1488
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35397d766e6cb991c0106aca56dcff865f525270;p=cvc5.git

Generalize congruence handling for HO in eq proofs (#6883)

Previously we were not considering proofs for HO equalities (i.e., between operators) that were transitivity chains. This commit generalizes the elaboration procedure in eq_proof to do so.
---

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index fbed7ffb5..6b2fae389 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -1321,24 +1321,30 @@ Node EqProof::addToProof(CDProof* p,
     }
   }
   std::vector<Node> children(arity + 1);
-  // Check if there is a justification for equality between functions (HO case)
-  if (!transitivityChildren[0].empty())
-  {
-    Assert(k == kind::APPLY_UF) << "Congruence with different functions only "
-                                   "allowed for uninterpreted functions.\n";
-
-    children[0] =
-        conclusion[0].getOperator().eqNode(conclusion[1].getOperator());
-    Assert(transitivityChildren[0].size() == 1
-           && CDProof::isSame(children[0], transitivityChildren[0][0]))
-        << "Justification of operators equality is wrong: "
-        << transitivityChildren[0] << "\n";
-  }
   // Proccess transitivity matrix to (possibly) generate transitivity steps for
   // congruence premises (= ai bi)
-  for (unsigned i = 1; i <= arity; ++i)
+  for (unsigned i = 0; i <= arity; ++i)
   {
-    Node transConclusion = conclusion[0][i - 1].eqNode(conclusion[1][i - 1]);
+    Node transConclusion;
+    // We special case the operator case because there is only ever the need to
+    // do something when in some HO case
+    if (i == 0)
+    {
+      // no justification for equality between functions, skip
+      if (transitivityChildren[0].empty())
+      {
+        continue;
+      }
+      // HO case
+      Assert(k == kind::APPLY_UF) << "Congruence with different functions only "
+                                     "allowed for uninterpreted functions.\n";
+      transConclusion =
+          conclusion[0].getOperator().eqNode(conclusion[1].getOperator());
+    }
+    else
+    {
+      transConclusion = conclusion[0][i - 1].eqNode(conclusion[1][i - 1]);
+    }
     children[i] = transConclusion;
     Assert(!transitivityChildren[i].empty())
         << "EqProof::addToProof: did not add any justification for " << i