From 084518db641e0648164bbe4461cd98b10e937dc0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 20:37:23 -0600 Subject: [PATCH] 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. --- src/theory/datatypes/theory_datatypes.cpp | 17 +++++++++++------ 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 -- 2.30.2