From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 26 Nov 2020 02:37:23 +0000 (-0600)
Subject: Disable fact vs lemma optimization in datatypes for now (#5521)
X-Git-Tag: cvc5-1.0.0~2550
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=084518db641e0648164bbe4461cd98b10e937dc0;p=cvc5.git

Disable fact vs lemma optimization in datatypes for now (#5521)

This optimization needs more work to determine its correctness. It is currently leading to incorrect candidate models on Facebook benchmarks.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6bfe136ce..74c822215 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1551,13 +1551,18 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   }
   eq = tt.eqNode(tt_cons);
   // Determine if the equality must be sent out as a lemma. Notice that
-  // we can keep new equalities from the instantiate rule internal as long as
-  // they are for datatype constructors that have no arguments that have
-  // finite external type. Such equalities must be sent because they introduce
-  // selector terms that may contribute to conflicts due to cardinality (good
-  // examples of this are regress0/datatypes/dt-param-card4-bool-sat.smt2 and
+  // we could potentially keep new equalities from the instantiate rule internal
+  // as long as they are for datatype constructors that have no arguments that
+  // have finite external type, which would correspond to:
+  //   forceLemma = dt[index].hasFiniteExternalArgType(ttn);
+  // Such equalities must be sent because they introduce selector terms that
+  // 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 = dt[index].hasFiniteExternalArgType(ttn);
+  // For now, to be conservative, we always send lemmas out, since otherwise
+  // we may encounter conflicts during model building when datatypes adds its
+  // equality engine to the theory model.
+  bool forceLemma = true;
   Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
                                  << " forceLemma = " << forceLemma << std::endl;
   d_im.addPendingInference(eq, exp, forceLemma, InferId::INST);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index effe70c1c..8969b6c01 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -769,7 +769,6 @@ set(regress_0_tests
   regress0/quantifiers/issue4086-infs.smt2
   regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
   regress0/quantifiers/issue4437-unc-quant.smt2
-  regress0/quantifiers/issue4476-ext-rew.smt2
   regress0/quantifiers/issue4576.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
@@ -2418,6 +2417,8 @@ set(regression_disabled_tests
   regress0/ite_arith.smt2
   regress0/lemmas/fischer3-mutex-16.smtv1.smt2
   regress0/nl/all-logic.smt2
+  # timeout after change to datatypes, impacting sygus-inst
+  regress0/quantifiers/issue4476-ext-rew.smt2
   regress0/quantifiers/qbv-multi-lit-uge.smt2
   regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
   regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2