From d7ef769395f75b7acae3dd36df587a4438db5673 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Oct 2020 12:18:26 -0500 Subject: [PATCH] Send external equalities from collapse selector as lemmas (#5346) In 20e58d4, a policy change was made for datatypes to keep more inferences as internal facts. This leads to a crash (issue #5344) where the equality status of two BV terms is asked by TheoryDatatypes, where the TheoryBV was not informed of the term, as datatypes kept it internal. This refines the policy further such that the collapse selector rule is processed as a lemma for terms of external type. The reason is that this rule may generate new terms of external type. Other rules like unification retain the internal fact policy, as they do not generate new terms. Fixes #5344. FYI @barrettcw --- src/theory/datatypes/theory_datatypes.cpp | 9 +++++++-- src/theory/theory.cpp | 1 + 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1b557b3cb..d60d8af32 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1088,10 +1088,14 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { { Node eq = s.eqNode(rrs); Node peq = c.eqNode(s[0]); + // Since collapsing selectors may generate new terms, we must send + // this out as a lemma if it is of an external type, or otherwise we + // may ask for the equality status of terms that only datatypes knows + // about, see issue #5344. + bool forceLemma = !s.getType().isDatatype(); Trace("datatypes-infer") << "DtInfer : collapse sel"; - //Trace("datatypes-infer") << ( wrong ? " wrong" : ""); Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl; - d_im.addPendingInference(eq, peq, false, InferId::COLLAPSE_SEL); + d_im.addPendingInference(eq, peq, forceLemma, InferId::COLLAPSE_SEL); } } } @@ -1845,6 +1849,7 @@ bool TheoryDatatypes::areDisequal( TNode a, TNode b ){ } bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) { + Trace("datatypes-cg") << "areCareDisequal: " << x << " " << y << std::endl; Assert(d_equalityEngine->hasTerm(x)); Assert(d_equalityEngine->hasTerm(y)); if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES) diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 681f3bca1..78fe6927f 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -437,6 +437,7 @@ EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } + Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl; Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); // Check for equality (simplest) -- 2.30.2