From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 25 Feb 2021 20:36:05 +0000 (-0800)
Subject: Datatypes lemmas: share only external types (#5997)
X-Git-Tag: cvc5-1.0.0~2210
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a4b16c643d71c9318042ba7b9d42af71c58ac2f;p=cvc5.git

Datatypes lemmas: share only external types (#5997)

Forcing lemmas in datatypes used to be done only for external types.
This was changed to consider all types, which is not needed.
This PR brings back the restriction to external types.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9d3b5a143..45787ee04 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1562,11 +1562,15 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   // may contribute to conflicts due to cardinality (good examples of this are
   // regress0/datatypes/dt-param-card4-bool-sat.smt2 and
   // regress0/datatypes/list-bool.smt2).
-  bool forceLemma = true;
+  bool forceLemma;
   if (options::dtPoliteOptimize())
   {
     forceLemma = dt[index].hasFiniteExternalArgType(ttn);
   }
+  else
+  {
+    forceLemma = dt.involvesExternalType();
+  }
   Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
                                  << " forceLemma = " << forceLemma << std::endl;
   d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma);