From 6937d6afe65ae3e51f514ca463f95faa3feda7aa Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 23 Oct 2020 21:20:42 -0300 Subject: [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. --- src/theory/uf/equality_engine.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src/theory/uf') 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) -- cgit v1.2.3