From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Jul 2022 13:54:47 +0000 (-0500)
Subject: Global negate requires quantifiers (#8957)
X-Git-Tag: cvc5-1.0.1~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=32892dea0b4e8fc82cce05c705192c3b3828b4cd;p=cvc5.git

Global negate requires quantifiers (#8957)

Fixes cvc5/cvc5-projects#521.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
---

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)