Enable sygus-inst for FP, NIA and NRA. (#7098)

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index af34da6c7c73fd7bf3b29c4656610ffbc3434d2a..3c9a82a6176d9c7edf0f0f45f12112cc7276de5c 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -145,6 +145,22 @@ void SetDefaults::setDefaultsPre(Options& opts)
 
 void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 {
+  if (opts.quantifiers.sygusInstWasSetByUser)
+  {
+    if (isSygus(opts))
+    {
+      throw OptionException(std::string(
+          "SyGuS instantiation quantifiers module cannot be enabled "
+          "for SyGuS inputs."));
+    }
+  }
+  else if (!isSygus(opts) && logic.isQuantified()
+           && (logic.isPure(THEORY_FP)
+               || (logic.isPure(THEORY_ARITH) && !logic.isLinear())))
+  {
+    opts.quantifiers.sygusInst = true;
+  }
+
   if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
   {
     if (opts.smt.produceModels

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d1208ad0f2248dbfc289c9e6dd5f5be66430cf1d..8804563b4f78674f2268d7fba5298f6797c6d011 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2764,6 +2764,7 @@ set(regression_disabled_tests
   regress2/ho/SYO362^5.p
   # time out
   regress3/unifpi-solve-car_1.lus.sy
+  # unknown (is sat)
   regress3/issue4476-ext-rew.smt2
 )
 

diff --git a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
index 62853011bff11f4b61eb9d8f442cd28154c6745d..3aeb38c6e108e39fb938e19db1e16e046c72c2ad 100644 (file)
--- a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
+++ b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-rlv=always
+; COMMAND-LINE: --nl-rlv=always --no-sygus-inst
 ; EXPECT: unsat
 (set-logic NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/issue5662-nl-tc.smt2 b/test/regress/regress1/nl/issue5662-nl-tc.smt2
index d805b721d51c2882d4586e1d957ab9af9f526f57..9107d3f64f609b39fb9256da942c3f7ffdacda19 100644 (file)
--- a/test/regress/regress1/nl/issue5662-nl-tc.smt2
+++ b/test/regress/regress1/nl/issue5662-nl-tc.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-sygus-inst
 (set-logic NRA)
 (set-info :status sat)
 (declare-fun a () Real)

diff --git a/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
index ee7cafd63324bccb7e54337524d18a19ef1246b4..f3a3c99b75b81d04029f44900473167c119751cb 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
+++ b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rewrite-quant
+; COMMAND-LINE: --ext-rewrite-quant --no-check-models
 ; EXPECT: sat
 (set-logic NIA)
 (assert (exists ((x Int)) (= (div 1 x x) x)))

diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
index f414f46310c70072bffd3540292ec2f7e7b97f37..0cd319ffbb5397aad8847b32cef8215ecb912b39 100644 (file)
--- a/test/regress/regress1/quantifiers/issue5470-aext.smt2
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic NIA)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
index 82857c50ab165115b06bc819a4e30ca63b6591b5..a6dfc9f9260462c52492ac64860cef1933611856 100644 (file)
--- a/test/regress/regress1/quantifiers/nl-pow-trick.smt2
+++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-all --no-relational-triggers
+; COMMAND-LINE: --cegqi-all --no-relational-triggers --no-sygus-inst
 ; EXPECT: unsat
 (set-logic NIA)
 (declare-fun a () Int)