diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-25 20:37:23 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-25 20:37:23 -0600 |
| commit | 084518db641e0648164bbe4461cd98b10e937dc0 (patch) | |
| tree | c229d107f9ccc0b6188b9114ddf834cb20e2f8d4 | |
| parent | 8e21ca2de274f82ded4429d21a34741fc1501b1b (diff) | |
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.
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 17 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 |
2 files changed, 13 insertions, 7 deletions
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 |