From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 2 Sep 2021 03:22:57 +0000 (-0700)
Subject: Enable sygus-inst for FP, NIA and NRA. (#7098)
X-Git-Tag: cvc5-1.0.0~1297
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c26524c9b5b5d9fd62ba68ac49759957a1e54d8e;p=cvc5.git

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

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index af34da6c7..3c9a82a61 100644
--- 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 d1208ad0f..8804563b4 100644
--- 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 62853011b..3aeb38c6e 100644
--- 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 d805b721d..9107d3f64 100644
--- 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 ee7cafd63..f3a3c99b7 100644
--- 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 f414f4631..0cd319ffb 100644
--- 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 82857c50a..a6dfc9f92 100644
--- 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)