From 32892dea0b4e8fc82cce05c705192c3b3828b4cd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Jul 2022 08:54:47 -0500 Subject: [PATCH] Global negate requires quantifiers (#8957) Fixes cvc5/cvc5-projects#521. Co-authored-by: Aina Niemetz --- src/smt/set_defaults.cpp | 7 +++++++ test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/quantifiers/global_negate.smt2 | 11 +++++++++++ 3 files changed, 19 insertions(+) create mode 100644 test/regress/cli/regress0/quantifiers/global_negate.smt2 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 942af84e8..63dd97ba2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1243,6 +1243,13 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const logic = log; logic.lock(); } + if (opts.quantifiers.globalNegate) + { + LogicInfo log(logic.getUnlockedCopy()); + log.enableQuantifiers(); + logic = log; + logic.lock(); + } if (opts.quantifiers.preSkolemQuantNested && opts.quantifiers.preSkolemQuantNestedWasSetByUser) { diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 0545664b3..51836ea02 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1074,6 +1074,7 @@ set(regress_0_tests regress0/quantifiers/ex3.smt2 regress0/quantifiers/ex6.smt2 regress0/quantifiers/floor.smt2 + regress0/quantifiers/global_negate.smt2 regress0/quantifiers/horn-ground-pre-post.smt2 regress0/quantifiers/is-even-pred.smt2 regress0/quantifiers/is-int.smt2 diff --git a/test/regress/cli/regress0/quantifiers/global_negate.smt2 b/test/regress/cli/regress0/quantifiers/global_negate.smt2 new file mode 100644 index 000000000..e03babc85 --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/global_negate.smt2 @@ -0,0 +1,11 @@ +; EXPECT: sat +(set-option :global-declarations true) +(set-logic QF_FP) +(set-option :global-negate true) +(set-option :fp-exp true) +(declare-const _x0 (_ BitVec 23)) +(declare-const _x1 (_ BitVec 5)) +(declare-const _x2 (_ BitVec 16)) +(declare-const _x3 (_ BitVec 5)) +(assert (let ((_let0 ((_ to_fp 5 11) _x2)))(fp.leq _let0 _let0 _let0))) +(check-sat) -- 2.30.2