From 739f947fb53bc44fbae59952b3d9878b65ed0576 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Jun 2021 12:04:00 -0500 Subject: [PATCH] Always check legal eliminations in quantified logics (#6720) Fixes #6699. --- src/theory/theory.cpp | 12 +++++++++--- test/regress/CMakeLists.txt | 8 +++++--- .../regress1/quantifiers/issue6699-nc-shadow.smt2 | 9 +++++++++ 3 files changed, 23 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index d6ad4cd41..b9dc1ba42 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -330,12 +330,18 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!options::produceModels()) + if (!options::produceModels() && !d_logicInfo.isQuantified()) { - // don't care about the model, we are fine + // Don't care about the model and logic is not quantified, we can eliminate. return true; } - // if there is a model object + // If models are enabled, then it depends on whether the term contains any + // unevaluable operators like FORALL, SINE, etc. Having such operators makes + // model construction contain non-constant values for variables, which is + // not ideal from a user perspective. + // We also insist on this check since the term to eliminate should never + // contain quantifiers, or else variable shadowing issues may arise. + // there should be a model object TheoryModel* tm = d_valuation.getModel(); Assert(tm != nullptr); return tm->isLegalElimination(x, val); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ca281af7b..6706ed4f6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1614,13 +1614,10 @@ set(regress_1_tests regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 - regress1/ho/nested_lambdas-AGT034^2.smt2 - regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p regress1/ho/store-ax-min.p - regress1/ho/SYO056^1.p regress1/hole6.cvc regress1/ite5.smt2 regress1/issue3970-nl-ext-purify.smt2 @@ -1849,6 +1846,7 @@ set(regress_1_tests regress1/quantifiers/issue5658-qe.smt2 regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 regress1/quantifiers/issue5899-qe.smt2 + regress1/quantifiers/issue6699-nc-shadow.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -2632,6 +2630,10 @@ set(regression_disabled_tests regress1/fmf/ko-bound-set.cvc # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 + # after disallowing solving for terms with quantifiers + regress1/ho/nested_lambdas-AGT034^2.smt2 + regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 + regress1/ho/SYO056^1.p # slow on some builds after changes to tangent planes regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator diff --git a/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 b/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 new file mode 100644 index 000000000..e1e0cdbe8 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -i +; EXPECT: unsat +(set-logic ALL) +(declare-fun v1 () Bool) +(declare-fun v4 () Bool) +(declare-fun v7 () Bool) +(assert (distinct v7 v1 (and v4 (exists ((q1 Int)) (= (= 0 q1) (and v7 v1)))))) +(push) +(check-sat) -- 2.30.2