From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Sat, 24 Oct 2020 00:20:42 +0000 (-0300)
Subject: [proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)
X-Git-Tag: cvc5-1.0.0~2664
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6937d6afe65ae3e51f514ca463f95faa3feda7aa;p=cvc5.git

[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)

Adding missing cases of kinds that are n-ary but whose partial applications are
not true terms in the equality engine. This in the case not only for APPLY_UF
but also for the APPLY_* kinds for datatypes.
---

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index fdb80e878..f04ebbb60 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1011,13 +1011,19 @@ void EqualityEngine::buildEqConclusion(EqualityNodeId id1,
   Kind k2 = d_nodes[id2].getKind();
   // only try to build if ids do not correspond to internal nodes. If they do,
   // only try to build build if full applications corresponding to the given ids
-  // have the same congruence n-ary non-APPLY_UF kind, since the internal nodes
+  // have the same congruence n-ary non-APPLY_* kind, since the internal nodes
   // may be full nodes.
   if ((d_isInternal[id1] || d_isInternal[id2])
-      && (k1 != k2 || k1 == kind::APPLY_UF || !ExprManager::isNAryKind(k1)))
+      && (k1 != k2 || k1 == kind::APPLY_UF || k1 == kind::APPLY_CONSTRUCTOR
+          || k1 == kind::APPLY_SELECTOR || k1 == kind::APPLY_TESTER
+          || !ExprManager::isNAryKind(k1)))
   {
     return;
   }
+  Debug("equality") << "buildEqConclusion: {" << id1 << "} " << d_nodes[id1]
+                    << "\n";
+  Debug("equality") << "buildEqConclusion: {" << id2 << "} " << d_nodes[id2]
+                    << "\n";
   Node eq[2];
   NodeManager* nm = NodeManager::currentNM();
   for (unsigned i = 0; i < 2; ++i)