From 6c8702ab5eb08466bf954e202241df39de680081 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 3 Jun 2020 08:47:46 -0500 Subject: [PATCH] Do not apply unconstrained simplification when quantifiers are present (#4532) Fixes #4437. This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered. It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic. --- src/options/smt_options.toml | 2 +- src/parser/smt2/Smt2.g | 8 +++++++- src/preprocessing/passes/unconstrained_simplifier.cpp | 9 +++++++++ src/preprocessing/passes/unconstrained_simplifier.h | 6 +++++- test/regress/CMakeLists.txt | 3 +-- .../regress0/quantifiers/issue4437-unc-quant.smt2 | 7 +++++++ test/regress/regress0/unconstrained/4481.smt2 | 3 ++- test/regress/regress0/unconstrained/4484.smt2 | 8 -------- test/regress/regress0/unconstrained/4486.smt2 | 8 -------- test/regress/regress1/strings/norn-ab.smt2 | 2 +- 10 files changed, 33 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 delete mode 100644 test/regress/regress0/unconstrained/4484.smt2 delete mode 100644 test/regress/regress0/unconstrained/4486.smt2 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 08e6f317c..449c0c31e 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -346,7 +346,7 @@ header = "options/smt_options.h" long = "unconstrained-simp" type = "bool" default = "false" - help = "turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)" + help = "turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logic QF_ABV." [[option]] name = "repeatSimp" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 081990a45..f29e03380 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1692,7 +1692,13 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] std::vector argTypes; } : LPAREN_TOK quantOp[kind] - { PARSER_STATE->pushScope(true); } + { + if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS)) + { + PARSER_STATE->parseError("Quantifier used in non-quantified logic."); + } + PARSER_STATE->pushScope(true); + } boundVarList[bvl] term[f, f2] RPAREN_TOK { diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 5d544ae57..b74909824 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -91,6 +91,15 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) d_unconstrained.insert(current); } } + else if (current.isClosure()) + { + // Throw an exception. This should never happen in practice unless the + // user specifically enabled unconstrained simplification in an illegal + // logic. + throw LogicException( + "Cannot use unconstrained simplification in this logic, due to " + "(possibly internally introduced) quantified formula."); + } else { for (TNode childNode : current) diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index ac4fd0a03..7fc13e17d 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -62,7 +62,11 @@ class UnconstrainedSimplifier : public PreprocessingPass theory::SubstitutionMap d_substitutions; const LogicInfo& d_logicInfo; - + /** + * Visit all subterms in assertion. This method throws a LogicException if + * there is a subterm that is unhandled by this preprocessing pass (e.g. a + * quantified formula). + */ void visitAll(TNode assertion); Node newUnconstrainedVar(TypeNode t, TNode var); void processUnconstrained(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b66d4e973..801f38b29 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -740,6 +740,7 @@ set(regress_0_tests regress0/quantifiers/issue3655.smt2 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/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 @@ -1127,8 +1128,6 @@ set(regress_0_tests regress0/uflra/simple.03.cvc regress0/uflra/simple.04.cvc regress0/unconstrained/4481.smt2 - regress0/unconstrained/4484.smt2 - regress0/unconstrained/4486.smt2 regress0/unconstrained/arith.smt2 regress0/unconstrained/arith3.smt2 regress0/unconstrained/arith4.smt2 diff --git a/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 new file mode 100644 index 000000000..61f792999 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 @@ -0,0 +1,7 @@ +; EXPECT: (error "Parse Error: issue4437-unc-quant.smt2:6.15: Quantifier used in non-quantified logic.") +; EXIT: 1 +(set-logic QF_AUFBVLIA) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(assert (forall ((c (_ BitVec 8))) (= (bvashr c a) b))) +(check-sat) diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2 index 028607093..19179f4d7 100644 --- a/test/regress/regress0/unconstrained/4481.smt2 +++ b/test/regress/regress0/unconstrained/4481.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp -; EXPECT: unsat +; EXPECT: (error "Cannot use unconstrained simplification in this logic, due to (possibly internally introduced) quantified formula.") +; EXIT: 1 (set-logic ALL) (set-info :status unsat) (declare-fun a () Int) diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2 deleted file mode 100644 index f2f11295b..000000000 --- a/test/regress/regress0/unconstrained/4484.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; COMMAND-LINE: --unconstrained-simp -; EXPECT: unsat -(set-logic QF_NIRA) -(set-info :status unsat) -(declare-fun a () Real) -(assert (= (to_int a) 2)) -(assert (= (to_int (/ a 2.0)) 2)) -(check-sat) diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2 deleted file mode 100644 index 01771ce66..000000000 --- a/test/regress/regress0/unconstrained/4486.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; COMMAND-LINE: --unconstrained-simp -; EXPECT: sat -(set-logic ALL) -(set-info :status sat) -(declare-fun x () Real) -(assert (is_int x)) -(assert (is_int (+ x 1))) -(check-sat) diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2 index 63a95bb78..6109a01dd 100644 --- a/test/regress/regress1/strings/norn-ab.smt2 +++ b/test/regress/regress1/strings/norn-ab.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic QF_SLIA) +(set-logic SLIA) (set-info :status unsat) (set-option :strings-exp true) -- 2.30.2