From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Oct 2020 17:18:26 +0000 (-0500)
Subject: Send external equalities from collapse selector as lemmas (#5346)
X-Git-Tag: cvc5-1.0.0~2662
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7ef769395f75b7acae3dd36df587a4438db5673;p=cvc5.git

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

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)