From feb0643e8d02e6c26b2cf2a4325ac05542c47e73 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Mar 2022 14:34:31 -0500 Subject: [PATCH] Disable minisat variable elimination when a parametric theory is present (#8487) Fixes cvc5/cvc5-projects#506. It seems there are extremely few cases where it is safe to use this option. --- src/smt/set_defaults.cpp | 10 +++++++--- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/arrays/proj-issue506-ms-var-elim.smt2 | 6 ++++++ 3 files changed, 14 insertions(+), 3 deletions(-) create mode 100644 test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 32fafc75b..b3a8007a1 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -695,12 +695,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL) { // cannot use minisat variable elimination for logics where a theory solver - // introduces new literals into the search. This includes quantifiers + // introduces new literals into the search, or for parametric theories + // which may introduce Boolean term variables. This includes quantifiers // (quantifier instantiation), and the lemma schemas used in non-linear // and sets. We also can't use it if models are enabled. if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS) - || logic.isQuantified() || opts.smt.produceModels - || opts.smt.produceAssignments || opts.smt.checkModels + || logic.isTheoryEnabled(THEORY_ARRAYS) + || logic.isTheoryEnabled(THEORY_STRINGS) + || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isQuantified() + || opts.smt.produceModels || opts.smt.produceAssignments + || opts.smt.checkModels || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { opts.prop.minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index f20bc9edd..f4c318da4 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -132,6 +132,7 @@ set(regress_0_tests regress0/arrays/issue7596-define-array-uminus.smt2 regress0/arrays/issue8103-1-weak-equiv-models.smt2 regress0/arrays/issue8276-arith-getModelValue.smt2 + regress0/arrays/proj-issue506-ms-var-elim.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 regress0/arrays/x3.smtv1.smt2 diff --git a/test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2 b/test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2 new file mode 100644 index 000000000..40974915f --- /dev/null +++ b/test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_AX) +(set-info :status sat) +(declare-const x (Array Bool Bool)) +(declare-const _x Bool) +(assert (select (store x _x false) false)) +(check-sat) -- 2.30.2