From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Oct 2021 16:24:31 +0000 (-0500)
Subject: Disable sygus-inst when incremental (#7485)
X-Git-Tag: cvc5-1.0.0~968
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa09c24adf024eee0a72ba5b5d9119c71e17d2a0;p=cvc5.git

Disable sygus-inst when incremental (#7485)

Fixes #7385.

Option --sygus-inst relies on the quantifier-free sygus extension of datatypes, which does not support incremental mode. Updating it to support incremental is a long term project.

Until this is complete, --sygus-inst should not be run in incremental mode.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 17f0cd2c9..c4935340f 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -197,7 +197,8 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
   }
   else if (!isSygus(opts) && logic.isQuantified()
            && (logic.isPure(THEORY_FP)
-               || (logic.isPure(THEORY_ARITH) && !logic.isLinear())))
+               || (logic.isPure(THEORY_ARITH) && !logic.isLinear()))
+           && !opts.base.incrementalSolving)
   {
     opts.quantifiers.sygusInst = true;
   }
@@ -989,6 +990,18 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
              << std::endl;
     opts.quantifiers.sygusInference = false;
   }
+  if (opts.quantifiers.sygusInst)
+  {
+    if (opts.quantifiers.sygusInstWasSetByUser)
+    {
+      reason << "sygus inst";
+      return true;
+    }
+    Notice() << "SolverEngine: turning off sygus inst to support "
+                "incremental solving"
+             << std::endl;
+    opts.quantifiers.sygusInst = false;
+  }
   if (opts.smt.solveIntAsBV > 0)
   {
     reason << "solveIntAsBV";
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2cf9554e2..8263152dd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1960,6 +1960,7 @@ set(regress_1_tests
   regress1/quantifiers/issue6699-nc-shadow.smt2
   regress1/quantifiers/issue6775-vts-int.smt2
   regress1/quantifiers/issue6845-nl-lemma-tc.smt2
+  regress1/quantifiers/issue7385-sygus-inst-i.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2
new file mode 100644
index 000000000..26fc1cf7e
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic NIRA)
+(push)
+(assert (exists ((q29 Int) (q30 Bool) (q35 Bool)) (= (= 0 q29) (= q35 q30))))
+(push)
+(pop)
+(pop)
+(check-sat)