Properly guard commands in the SyGuS API (#8390)

This commit ensures we don't segfault in the SyGuS API (for non-text inputs) if the option sygus is not set to true. It also renames mkSygusVar to declareSygusVar for consistency with the sygus input format.

For SyGuS API inputs, we now use the option sygus to true instead of setting the language to sygus2.

This furthermore changes a few details in set-defaults regarding the relationship between the language, the sygus option, and when to apply default options for sygus.

It also adds a unit test for checkSynth.

diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp
index 37a69fbdb7639396f43f1b44338ac83f33e05151..978e55fe60c4c3a63506e4bad64bc0b6afe53594 100644 (file)
--- a/examples/api/cpp/sygus-fun.cpp
+++ b/examples/api/cpp/sygus-fun.cpp
@@ -61,7 +61,7 @@ int main()
   Solver slv;
 
   // required options
-  slv.setOption("lang", "sygus2");
+  slv.setOption("sygus", "true");
   slv.setOption("incremental", "false");
 
   // set the logic
@@ -103,8 +103,8 @@ int main()
   Term min = slv.synthFun("min", {x, y}, integer);
 
   // declare universal variables.
-  Term varX = slv.mkSygusVar(integer, "x");
-  Term varY = slv.mkSygusVar(integer, "y");
+  Term varX = slv.declareSygusVar(integer, "x");
+  Term varY = slv.declareSygusVar(integer, "y");
 
   Term max_x_y = slv.mkTerm(APPLY_UF, {max, varX, varY});
   Term min_x_y = slv.mkTerm(APPLY_UF, {min, varX, varY});

diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp
index fc31a6a3231d21fb5360c5052186b3bf0e3ddab5..7be3cb0626b3dcf0cb094064b4591962d1016a38 100644 (file)
--- a/examples/api/cpp/sygus-grammar.cpp
+++ b/examples/api/cpp/sygus-grammar.cpp
@@ -58,7 +58,7 @@ int main()
   Solver slv;
 
   // required options
-  slv.setOption("lang", "sygus2");
+  slv.setOption("sygus", "true");
   slv.setOption("incremental", "false");
 
   // set the logic
@@ -103,7 +103,7 @@ int main()
   Term id4 = slv.synthFun("id4", {x}, integer, g1);
 
   // declare universal variables.
-  Term varX = slv.mkSygusVar(integer, "x");
+  Term varX = slv.declareSygusVar(integer, "x");
 
   Term id1_x = slv.mkTerm(APPLY_UF, {id1, varX});
   Term id2_x = slv.mkTerm(APPLY_UF, {id2, varX});

diff --git a/examples/api/cpp/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp
index aaff3e695c81accb64370e75a0f82d4d7a28ca84..3b8edd53a2e5f41f5aca82afb2bf0d1e21ef9f35 100644 (file)
--- a/examples/api/cpp/sygus-inv.cpp
+++ b/examples/api/cpp/sygus-inv.cpp
@@ -49,7 +49,7 @@ int main()
   Solver slv;
 
   // required options
-  slv.setOption("lang", "sygus2");
+  slv.setOption("sygus", "true");
   slv.setOption("incremental", "false");
 
   // set the logic

diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java
index 31aecdc94e248fd54a1d153d18872e6278a2246e..07a0eebbc934271d6b5be12e2104d5cad07ad985 100644 (file)
--- a/examples/api/java/SygusFun.java
+++ b/examples/api/java/SygusFun.java
@@ -59,7 +59,7 @@ public class SygusFun
     try (Solver slv = new Solver())
     {
       // required options
-      slv.setOption("lang", "sygus2");
+      slv.setOption("sygus", "true");
       slv.setOption("incremental", "false");
 
       // set the logic
@@ -101,8 +101,8 @@ public class SygusFun
       Term min = slv.synthFun("min", new Term[] {x, y}, integer);
 
       // declare universal variables.
-      Term varX = slv.mkSygusVar(integer, "x");
-      Term varY = slv.mkSygusVar(integer, "y");
+      Term varX = slv.declareSygusVar(integer, "x");
+      Term varY = slv.declareSygusVar(integer, "y");
 
       Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY);
       Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY);

diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java
index af8816a4063aa31099e76595e46cd1ae435c98e0..25233617b2a79bdfaa6ae3a4abea911ac7941162 100644 (file)
--- a/examples/api/java/SygusGrammar.java
+++ b/examples/api/java/SygusGrammar.java
@@ -56,7 +56,7 @@ public class SygusGrammar
     try (Solver slv = new Solver())
     {
       // required options
-      slv.setOption("lang", "sygus2");
+      slv.setOption("sygus", "true");
       slv.setOption("incremental", "false");
 
       // set the logic
@@ -101,7 +101,7 @@ public class SygusGrammar
       Term id4 = slv.synthFun("id4", new Term[] {x}, integer, g1);
 
       // declare universal variables.
-      Term varX = slv.mkSygusVar(integer, "x");
+      Term varX = slv.declareSygusVar(integer, "x");
 
       Term id1_x = slv.mkTerm(APPLY_UF, id1, varX);
       Term id2_x = slv.mkTerm(APPLY_UF, id2, varX);

diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java
index 226e8e61ea4260c2f2876f8dd09fb043b3443660..f07a4816eeb778ec0450daf1d7fada7b138911c1 100644 (file)
--- a/examples/api/java/SygusInv.java
+++ b/examples/api/java/SygusInv.java
@@ -47,7 +47,7 @@ public class SygusInv
     try (Solver slv = new Solver())
     {
       // required options
-      slv.setOption("lang", "sygus2");
+      slv.setOption("sygus", "true");
       slv.setOption("incremental", "false");
 
       // set the logic

diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 2f6417e35840904b01edf8fbd1a4ea86c95c8d19..82f3d08a73f2b629394512887005dab9cba4b8b7 100644 (file)
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -24,7 +24,7 @@ if __name__ == "__main__":
   slv = cvc5.Solver()
 
   # required options
-  slv.setOption("lang", "sygus2")
+  slv.setOption("sygus", "true")
   slv.setOption("incremental", "false")
 
   # set the logic
@@ -66,8 +66,8 @@ if __name__ == "__main__":
   min = slv.synthFun("min", [x, y], integer)
 
   # declare universal variables.
-  varX = slv.mkSygusVar(integer, "x")
-  varY = slv.mkSygusVar(integer, "y")
+  varX = slv.declareSygusVar(integer, "x")
+  varY = slv.declareSygusVar(integer, "y")
 
   max_x_y = slv.mkTerm(Kind.ApplyUf, max, varX, varY)
   min_x_y = slv.mkTerm(Kind.ApplyUf, min, varX, varY)

diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 41adad822f704148b494cc9f7ef76874aaa9d652..c6c158f793b60365b609ed01cbd05fecdf56f295 100644 (file)
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -25,7 +25,7 @@ if __name__ == "__main__":
   slv = cvc5.Solver()
 
   # required options
-  slv.setOption("lang", "sygus2")
+  slv.setOption("sygus", "true")
   slv.setOption("incremental", "false")
 
   # set the logic
@@ -70,7 +70,7 @@ if __name__ == "__main__":
   id4 = slv.synthFun("id4", {x}, integer, g1)
 
   # declare universal variables.
-  varX = slv.mkSygusVar(integer, "x")
+  varX = slv.declareSygusVar(integer, "x")
 
   id1_x = slv.mkTerm(Kind.ApplyUf, id1, varX)
   id2_x = slv.mkTerm(Kind.ApplyUf, id2, varX)

diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 249952a9e7b91494bc90ed3ef13d01716c5089fb..90a3deca7327073a22613ed787ae69376f628d33 100644 (file)
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -24,7 +24,7 @@ if __name__ == "__main__":
   slv = cvc5.Solver()
 
   # required options
-  slv.setOption("lang", "sygus2")
+  slv.setOption("sygus", "true")
   slv.setOption("incremental", "false")
 
   # set the logic

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0eba91ee291c2a52b2fc88694c4ac148ca7d923c..b229ef65f42bc69d01a37bcc3eb768d1a8376a0d 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -63,6 +63,7 @@
 #include "options/options.h"
 #include "options/options_public.h"
 #include "options/smt_options.h"
+#include "options/quantifiers_options.h"
 #include "proof/unsat_core.h"
 #include "smt/env.h"
 #include "smt/model.h"
@@ -7450,10 +7451,12 @@ void Solver::setOption(const std::string& option,
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkSygusVar(const Sort& sort, const std::string& symbol) const
+Term Solver::declareSygusVar(const Sort& sort, const std::string& symbol) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot call declareSygusVar unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
@@ -7486,6 +7489,8 @@ Term Solver::synthFun(const std::string& symbol,
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars);
   CVC5_API_SOLVER_CHECK_SORT(sort);
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot call synthFun unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   return synthFunHelper(symbol, boundVars, sort);
   ////////
@@ -7500,6 +7505,8 @@ Term Solver::synthFun(const std::string& symbol,
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars);
   CVC5_API_SOLVER_CHECK_SORT(sort);
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot call synthFun unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   return synthFunHelper(symbol, boundVars, sort, false, &grammar);
   ////////
@@ -7511,6 +7518,8 @@ Term Solver::synthInv(const std::string& symbol,
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars);
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot call synthInv unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   return synthFunHelper(
       symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true);
@@ -7524,6 +7533,8 @@ Term Solver::synthInv(const std::string& symbol,
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars);
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot call synthInv unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   return synthFunHelper(symbol,
                         boundVars,
@@ -7541,6 +7552,8 @@ void Solver::addSygusConstraint(const Term& term) const
   CVC5_API_ARG_CHECK_EXPECTED(
       term.d_node->getType() == getNodeManager()->booleanType(), term)
       << "boolean term";
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot addSygusConstraint unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   d_slv->assertSygusConstraint(*term.d_node, false);
   ////////
@@ -7554,6 +7567,8 @@ void Solver::addSygusAssume(const Term& term) const
   CVC5_API_ARG_CHECK_EXPECTED(
       term.d_node->getType() == getNodeManager()->booleanType(), term)
       << "boolean term";
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot addSygusAssume unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   d_slv->assertSygusConstraint(*term.d_node, true);
   ////////
@@ -7584,6 +7599,8 @@ void Solver::addSygusInvConstraint(Term inv,
 
   CVC5_API_CHECK(post.d_node->getType() == invType)
       << "Expected inv and post to have the same sort";
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot addSygusInvConstraint unless sygus is enabled (use --sygus)";
   //////// all checks before this line
 
   const std::vector<TypeNode>& invArgTypes = invType.getArgTypes();
@@ -7612,6 +7629,8 @@ void Solver::addSygusInvConstraint(Term inv,
 Result Solver::checkSynth() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot checkSynth unless sygus is enabled (use --sygus)";
   //////// all checks before this line
   return d_slv->checkSynth();
   ////////
@@ -7621,6 +7640,8 @@ Result Solver::checkSynth() const
 Result Solver::checkSynthNext() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
+      << "Cannot checkSynthNext unless sygus is enabled (use --sygus)";
   CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
       << "Cannot checkSynthNext when not solving incrementally (use "
          "--incremental)";

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 6d7f0417c288c7a3c726663e14e2e3c88f7a3b51..6d9b39df1219c4828117121ed9e66039df03a279 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4594,8 +4594,8 @@ class CVC5_EXPORT Solver
    * @param symbol the name of the universal variable
    * @return the universal variable
    */
-  Term mkSygusVar(const Sort& sort,
-                  const std::string& symbol = std::string()) const;
+  Term declareSygusVar(const Sort& sort,
+                       const std::string& symbol = std::string()) const;
 
   /**
    * Create a Sygus grammar. The first non-terminal is treated as the starting

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index f1f2b91f6653a5db5e0456fb62762d9132c6dc4a..183d2de95fc7cccdec8b1ec8db9a6232f8dee66f 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2420,9 +2420,9 @@ public class Solver implements IPointer, AutoCloseable
    * @param sort the sort of the universal variable
    * @return the universal variable
    */
-  public Term mkSygusVar(Sort sort)
+  public Term declareSygusVar(Sort sort)
   {
-    return mkSygusVar(sort, "");
+    return declareSygusVar(sort, "");
   }
   /**
    * Append \p symbol to the current list of universal variables.
@@ -2434,13 +2434,13 @@ public class Solver implements IPointer, AutoCloseable
    * @param symbol the name of the universal variable
    * @return the universal variable
    */
-  public Term mkSygusVar(Sort sort, String symbol)
+  public Term declareSygusVar(Sort sort, String symbol)
   {
-    long termPointer = mkSygusVar(pointer, sort.getPointer(), symbol);
+    long termPointer = declareSygusVar(pointer, sort.getPointer(), symbol);
     return new Term(this, termPointer);
   }
 
-  private native long mkSygusVar(long pointer, long sortPointer, String symbol);
+  private native long declareSygusVar(long pointer, long sortPointer, String symbol);
 
   /**
    * Create a Sygus grammar. The first non-terminal is treated as the starting

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index f440c164632bdb4c3879d4bda41ab6e8d2fb39c9..87caff1b0f7fa53a2fcf244aa255c4cfb3593c23 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2403,10 +2403,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_ensureTermSort(
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkSygusVar
+ * Method:    declareSygusVar
  * Signature: (JJLjava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSygusVar(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareSygusVar(
     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
@@ -2414,7 +2414,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSygusVar(
   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
   std::string cSymbol(s);
-  Term* retPointer = new Term(solver->mkSygusVar(*sort, cSymbol));
+  Term* retPointer = new Term(solver->declareSygusVar(*sort, cSymbol));
   env->ReleaseStringUTFChars(jSymbol, s);
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index c057e20f11ea5c1aada7f699d52a8ebdaf11f251..f133f324dc4992b79041edd1048fbeac8a92734a 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -246,8 +246,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Op mkOp(Kind kind, const vector[uint32_t]& args) except +
         # Sygus related functions
         Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
-        Term mkSygusVar(Sort sort, const string& symbol) except +
-        Term mkSygusVar(Sort sort) except +
+        Term declareSygusVar(Sort sort, const string& symbol) except +
+        Term declareSygusVar(Sort sort) except +
         void addSygusConstraint(Term term) except +
         void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except +
         Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 3305352d35cc81e3cabe05ecb28979cce717e657..354adaed193a653e9258132c73189597ddceb3ef 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1591,7 +1591,7 @@ cdef class Solver:
         grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
         return grammar
 
-    def mkSygusVar(self, Sort sort, str symbol=""):
+    def declareSygusVar(self, Sort sort, str symbol=""):
         """Append symbol to the current list of universal variables.
 
         SyGuS v2:
@@ -1605,7 +1605,7 @@ cdef class Solver:
         :return: the universal variable
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
+        term.cterm = self.csolver.declareSygusVar(sort.csort, symbol.encode())
         return term
 
     def addSygusConstraint(self, Term t):

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f104f3fa7b8b1e558c3dd30457b8a4fc3b3cc8f3..5c3933e5aca3263a0dcb812ef9d89db99ecb10e3 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -137,6 +137,14 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
       }
     }
   }
+  if (solver->getOption("input-language") == "LANG_SYGUS_V2")
+  {
+    // Enable the sygus API. We set this here instead of in set defaults 
+    // to simplify checking at the API level. In particular, the sygus
+    // option is the authority on whether sygus commands are currently
+    // allowed in the API.
+    solver->setOption("sygus", "true");
+  }
 
   if (solver->getOption("output-language") == "LANG_AUTO")
   {

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ac7392b86fde6dfbc1739585e354fb53e5545b20..f1476b94d70aad394bad89bdc751c5eb12709b9b 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -518,7 +518,7 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
     {
-      api::Term var = SOLVER->mkSygusVar(t, name);
+      api::Term var = SOLVER->declareSygusVar(t, name);
       PARSER_STATE->defineVar(name, var);
       cmd.reset(new DeclareSygusVarCommand(name, var, t));
     }

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 2416b9effd11fb244d04732b52ed5a2a806d6b1e..5e987b862163165b474d12c7d4c1b0d3ffa8c998 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -850,7 +850,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
 
 bool SetDefaults::isSygus(const Options& opts) const
 {
-  if (language::isLangSygus(opts.base.inputLanguage))
+  if (opts.quantifiers.sygus)
   {
     return true;
   }
@@ -913,13 +913,6 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
     reason << "global-negate";
     return true;
   }
-  if (isSygus(opts))
-  {
-    // When sygus answers "unsat", it is not due to showing a set of
-    // formulas is unsat in the standard way. Thus, proofs do not apply.
-    reason << "sygus";
-    return true;
-  }
   // options that are automatically set to support proofs
   if (opts.bv.bvAssertInput)
   {
@@ -1413,7 +1406,7 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
 
   // apply sygus options
   // if we are attempting to rewrite everything to SyGuS, use sygus()
-  if (usesSygus(opts))
+  if (isSygus(opts))
   {
     std::stringstream reasonNoSygus;
     if (incompatibleWithSygus(opts, reasonNoSygus))

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index cae7190a24e2dbe83d88c19485c563bd9c89802a..f3e135cdc46ea20df7616ced9306ec34ae5fc047 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -669,6 +669,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     // try a new core
     std::unique_ptr<SolverEngine> checkSol;
     initializeSubsolver(checkSol, d_env);
+    checkSol->setOption("sygus", "false");
     checkSol->setOption("produce-unsat-cores", "true");
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fc870b6ec0e108f56d7f3ea1ff849e80b3a1f7fd..7a07ae99607626d7dee05ad3405be9114c9a54a4 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1055,47 +1055,6 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
 /********************** Helper functions ***************************/
 /********************** Helper functions ***************************/
 
-Node mkAnd(const std::vector<TNode>& conjunctions)
-{
-  Assert(conjunctions.size() > 0);
-
-  std::set<TNode> all;
-  for (unsigned i = 0; i < conjunctions.size(); ++i)
-  {
-    TNode t = conjunctions[i];
-    if (t.getKind() == kind::AND)
-    {
-      for (TNode::iterator child_it = t.begin(); child_it != t.end();
-           ++child_it)
-      {
-        Assert((*child_it).getKind() != kind::AND);
-        all.insert(*child_it);
-      }
-    }
-    else
-    {
-      all.insert(t);
-    }
-  }
-
-  Assert(all.size() > 0);
-  if (all.size() == 1)
-  {
-    // All the same, or just one
-    return conjunctions[0];
-  }
-
-  NodeBuilder conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = all.begin();
-  std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end)
-  {
-    conjunction << *it;
-    ++it;
-  }
-  return conjunction;
-} /* mkAnd() */
-
 Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
 
 bool TheorySetsPrivate::isEntailed(Node n, bool pol)
@@ -1148,8 +1107,7 @@ Node TheorySetsPrivate::explain(TNode literal)
                   << polarity << "); kind" << atom.getKind() << std::endl;
     Unhandled();
   }
-
-  return mkAnd(assumptions);
+  return NodeManager::currentNM()->mkAnd(assumptions);
 }
 
 void TheorySetsPrivate::preRegisterTerm(TNode node)

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index c428eda3ac6e51d9a2ad6b41f3c77f74cd96b30e..ee249bea42e38956fb211ce85a4f2c07eedac96d 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2165,7 +2165,6 @@ set(regress_1_tests
   regress1/quantifiers/issue3765.smt2
   regress1/quantifiers/issue3765-quant-dd.smt2
   regress1/quantifiers/issue4021-ind-opts.smt2
-  regress1/quantifiers/issue4062-cegqi-aux.smt2
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue4328-nqe.smt2
@@ -3098,6 +3097,8 @@ set(regression_disabled_tests
   regress1/quantifiers/subtype-param.smt2
   # timeout after changes to theory preprocessing, note is non-linear and does not involve sygus-inst
   regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
+  # timeout on some builds after not applying default sygus options when using sygus-inst
+  regress1/quantifiers/issue4062-cegqi-aux.smt2
   ###
   regress1/rels/garbage_collect.cvc.smt2
   regress1/sets/setofsets-disequal.smt2

diff --git a/test/regress/cli/regress1/abduction/abduction_1255.corecstrs.readable.smt2 b/test/regress/cli/regress1/abduction/abduction_1255.corecstrs.readable.smt2
index 44bccd26431efae995ba3cb0638c095b3d2a6444..b4702415bbba6ae7673eefd81777a63cc13c2a29 100644 (file)
--- a/test/regress/cli/regress1/abduction/abduction_1255.corecstrs.readable.smt2
+++ b/test/regress/cli/regress1/abduction/abduction_1255.corecstrs.readable.smt2
@@ -2,7 +2,6 @@
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 
-
 (set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :source |

diff --git a/test/unit/api/cpp/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp
index 7b7556539e5dbc9bed14568aa90cfc028d68aba5..1aa35db8dd7cd5d94831627b4927c4d449b2d158 100644 (file)
--- a/test/unit/api/cpp/grammar_black.cpp
+++ b/test/unit/api/cpp/grammar_black.cpp
@@ -27,6 +27,7 @@ class TestApiBlackGrammar : public TestApi
 
 TEST_F(TestApiBlackGrammar, addRule)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
 
@@ -52,6 +53,7 @@ TEST_F(TestApiBlackGrammar, addRule)
 
 TEST_F(TestApiBlackGrammar, addRules)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
 
@@ -78,6 +80,7 @@ TEST_F(TestApiBlackGrammar, addRules)
 
 TEST_F(TestApiBlackGrammar, addAnyConstant)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolean = d_solver.getBooleanSort();
 
   Term nullTerm;
@@ -99,6 +102,7 @@ TEST_F(TestApiBlackGrammar, addAnyConstant)
 
 TEST_F(TestApiBlackGrammar, addAnyVariable)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolean = d_solver.getBooleanSort();
 
   Term nullTerm;

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7e6c113eb8344e4f5be54179a2bdc13aee8884f7..7e9fd58809e467a5f44c89311c18becfe24d1007 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2455,21 +2455,22 @@ TEST_F(TestApiBlackSolver, resetAssertions)
   d_solver.checkSatAssuming({slt, ule});
 }
 
-TEST_F(TestApiBlackSolver, mkSygusVar)
+TEST_F(TestApiBlackSolver, declareSygusVar)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
   Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
 
-  ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort));
-  ASSERT_NO_THROW(d_solver.mkSygusVar(funSort));
-  ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort, std::string("b")));
-  ASSERT_NO_THROW(d_solver.mkSygusVar(funSort, ""));
-  ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkSygusVar(d_solver.getNullSort(), "a"),
+  ASSERT_NO_THROW(d_solver.declareSygusVar(boolSort));
+  ASSERT_NO_THROW(d_solver.declareSygusVar(funSort));
+  ASSERT_NO_THROW(d_solver.declareSygusVar(boolSort, std::string("b")));
+  ASSERT_NO_THROW(d_solver.declareSygusVar(funSort, ""));
+  ASSERT_THROW(d_solver.declareSygusVar(Sort()), CVC5ApiException);
+  ASSERT_THROW(d_solver.declareSygusVar(d_solver.getNullSort(), "a"),
                CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.mkSygusVar(boolSort), CVC5ApiException);
+  ASSERT_THROW(slv.declareSygusVar(boolSort), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkSygusGrammar)
@@ -2495,6 +2496,7 @@ TEST_F(TestApiBlackSolver, mkSygusGrammar)
 
 TEST_F(TestApiBlackSolver, synthFun)
 {
+  d_solver.setOption("sygus", "true");
   Sort null = d_solver.getNullSort();
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
@@ -2519,6 +2521,7 @@ TEST_F(TestApiBlackSolver, synthFun)
   ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC5ApiException);
   ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC5ApiException);
   Solver slv;
+  slv.setOption("sygus", "true");
   Term x2 = slv.mkVar(slv.getBooleanSort());
   ASSERT_NO_THROW(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
   ASSERT_THROW(slv.synthFun("", {}, d_solver.getBooleanSort()),
@@ -2529,6 +2532,7 @@ TEST_F(TestApiBlackSolver, synthFun)
 
 TEST_F(TestApiBlackSolver, synthInv)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
 
@@ -2554,6 +2558,7 @@ TEST_F(TestApiBlackSolver, synthInv)
 
 TEST_F(TestApiBlackSolver, addSygusConstraint)
 {
+  d_solver.setOption("sygus", "true");
   Term nullTerm;
   Term boolTerm = d_solver.mkBoolean(true);
   Term intTerm = d_solver.mkInteger(1);
@@ -2563,11 +2568,13 @@ TEST_F(TestApiBlackSolver, addSygusConstraint)
   ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC5ApiException);
 
   Solver slv;
+  slv.setOption("sygus", "true");
   ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, addSygusAssume)
 {
+  d_solver.setOption("sygus", "true");
   Term nullTerm;
   Term boolTerm = d_solver.mkBoolean(false);
   Term intTerm = d_solver.mkInteger(1);
@@ -2577,11 +2584,13 @@ TEST_F(TestApiBlackSolver, addSygusAssume)
   ASSERT_THROW(d_solver.addSygusAssume(intTerm), CVC5ApiException);
 
   Solver slv;
+  slv.setOption("sygus", "true");
   ASSERT_THROW(slv.addSygusAssume(boolTerm), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, addSygusInvConstraint)
 {
+  d_solver.setOption("sygus", "true");
   Sort boolean = d_solver.getBooleanSort();
   Sort real = d_solver.getRealSort();
 
@@ -2633,6 +2642,7 @@ TEST_F(TestApiBlackSolver, addSygusInvConstraint)
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, trans),
                CVC5ApiException);
   Solver slv;
+  slv.setOption("sygus", "true");
   Sort boolean2 = slv.getBooleanSort();
   Sort real2 = slv.getRealSort();
   Term inv22 = slv.declareFun("inv", {real2}, boolean2);
@@ -2650,9 +2660,17 @@ TEST_F(TestApiBlackSolver, addSygusInvConstraint)
                CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, checkSynth)
+{
+  // requires option to be set
+  ASSERT_THROW(d_solver.checkSynth(), CVC5ApiException);
+  d_solver.setOption("sygus", "true");
+  ASSERT_NO_THROW(d_solver.checkSynth());
+}
+
 TEST_F(TestApiBlackSolver, getSynthSolution)
 {
-  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("sygus", "true");
   d_solver.setOption("incremental", "false");
 
   Term nullTerm;
@@ -2675,7 +2693,7 @@ TEST_F(TestApiBlackSolver, getSynthSolution)
 
 TEST_F(TestApiBlackSolver, getSynthSolutions)
 {
-  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("sygus", "true");
   d_solver.setOption("incremental", "false");
 
   Term nullTerm;
@@ -2700,7 +2718,7 @@ TEST_F(TestApiBlackSolver, getSynthSolutions)
 
 TEST_F(TestApiBlackSolver, checkSynthNext)
 {
-  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("sygus", "true");
   d_solver.setOption("incremental", "true");
   Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
 
@@ -2712,7 +2730,7 @@ TEST_F(TestApiBlackSolver, checkSynthNext)
 
 TEST_F(TestApiBlackSolver, checkSynthNext2)
 {
-  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("sygus", "true");
   d_solver.setOption("incremental", "false");
   Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
 
@@ -2722,7 +2740,7 @@ TEST_F(TestApiBlackSolver, checkSynthNext2)
 
 TEST_F(TestApiBlackSolver, checkSynthNext3)
 {
-  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("sygus", "true");
   d_solver.setOption("incremental", "true");
   Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
 

diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java
index 37e1b5206a62beb66a34819dac0bbd668244f707..15d9786922c5ded5abcc7277cea3f5db252137b1 100644 (file)
--- a/test/unit/api/java/GrammarTest.java
+++ b/test/unit/api/java/GrammarTest.java
@@ -39,6 +39,7 @@ class GrammarTest
 
   @Test void addRule()
   {
+    d_solver.setOption("sygus", "true");
     Sort bool = d_solver.getBooleanSort();
     Sort integer = d_solver.getIntegerSort();
 
@@ -63,6 +64,7 @@ class GrammarTest
 
   @Test void addRules()
   {
+    d_solver.setOption("sygus", "true");
     Sort bool = d_solver.getBooleanSort();
     Sort integer = d_solver.getIntegerSort();
 
@@ -91,6 +93,7 @@ class GrammarTest
 
   @Test void addAnyConstant()
   {
+    d_solver.setOption("sygus", "true");
     Sort bool = d_solver.getBooleanSort();
 
     Term nullTerm = d_solver.getNullTerm();
@@ -112,6 +115,7 @@ class GrammarTest
 
   @Test void addAnyVariable()
   {
+    d_solver.setOption("sygus", "true");
     Sort bool = d_solver.getBooleanSort();
 
     Term nullTerm = d_solver.getNullTerm();

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index cc94600f5c99f03f930a65457d4fa947b10081a1..fe5afeee61fb21c83f2740ae87ab360d0fb4b279 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -2403,22 +2403,24 @@ class SolverTest
     d_solver.checkSatAssuming(new Term[] {slt, ule});
   }
 
-  @Test void mkSygusVar() throws CVC5ApiException
+  @Test void declareSygusVar() throws CVC5ApiException
   {
+    d_solver.setOption("sygus", "true");
     Sort boolSort = d_solver.getBooleanSort();
     Sort intSort = d_solver.getIntegerSort();
     Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
 
-    assertDoesNotThrow(() -> d_solver.mkSygusVar(boolSort));
-    assertDoesNotThrow(() -> d_solver.mkSygusVar(funSort));
-    assertDoesNotThrow(() -> d_solver.mkSygusVar(boolSort, ("b")));
-    assertDoesNotThrow(() -> d_solver.mkSygusVar(funSort, ""));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar(boolSort));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar(funSort));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar(boolSort, ("b")));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar(funSort, ""));
 
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkSygusVar(d_solver.getNullSort()));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkSygusVar(d_solver.getNullSort(), "a"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort(), "a"));
 
     Solver slv = new Solver();
-    assertThrows(CVC5ApiException.class, () -> slv.mkSygusVar(boolSort));
+    slv.setOption("sygus", "true");
+    assertThrows(CVC5ApiException.class, () -> slv.declareSygusVar(boolSort));
     slv.close();
   }
 
@@ -2442,6 +2444,7 @@ class SolverTest
         () -> d_solver.mkSygusGrammar(new Term[] {boolTerm}, new Term[] {intVar}));
 
     Solver slv = new Solver();
+    slv.setOption("sygus", "true");
     Term boolVar2 = slv.mkVar(slv.getBooleanSort());
     Term intVar2 = slv.mkVar(slv.getIntegerSort());
     assertDoesNotThrow(() -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));
@@ -2455,6 +2458,7 @@ class SolverTest
 
   @Test void synthFun() throws CVC5ApiException
   {
+    d_solver.setOption("sygus", "true");
     Sort nullSort = d_solver.getNullSort();
     Sort bool = d_solver.getBooleanSort();
     Sort integer = d_solver.getIntegerSort();
@@ -2481,6 +2485,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.synthFun("f6", new Term[] {x}, bool, g2));
 
     Solver slv = new Solver();
+    slv.setOption("sygus", "true");
     Term x2 = slv.mkVar(slv.getBooleanSort());
     assertDoesNotThrow(() -> slv.synthFun("f1", new Term[] {x2}, slv.getBooleanSort()));
 
@@ -2493,6 +2498,7 @@ class SolverTest
 
   @Test void synthInv() throws CVC5ApiException
   {
+    d_solver.setOption("sygus", "true");
     Sort bool = d_solver.getBooleanSort();
     Sort integer = d_solver.getIntegerSort();
 
@@ -2518,6 +2524,7 @@ class SolverTest
 
   @Test void addSygusConstraint() throws CVC5ApiException
   {
+    d_solver.setOption("sygus", "true");
     Term nullTerm = d_solver.getNullTerm();
     Term boolTerm = d_solver.mkBoolean(true);
     Term intTerm = d_solver.mkInteger(1);
@@ -2527,12 +2534,14 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.addSygusConstraint(intTerm));
 
     Solver slv = new Solver();
+    slv.setOption("sygus", "true");
     assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
     slv.close();
   }
 
   @Test void addSygusAssume()
   {
+    d_solver.setOption("sygus", "true");
     Term nullTerm = d_solver.getNullTerm();
     Term boolTerm = d_solver.mkBoolean(false);
     Term intTerm = d_solver.mkInteger(1);
@@ -2542,12 +2551,14 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.addSygusAssume(intTerm));
 
     Solver slv = new Solver();
+    slv.setOption("sygus", "true");
     assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm));
     slv.close();
   }
 
   @Test void addSygusInvConstraint() throws CVC5ApiException
   {
+    d_solver.setOption("sygus", "true");
     Sort bool = d_solver.getBooleanSort();
     Sort real = d_solver.getRealSort();
 
@@ -2592,6 +2603,7 @@ class SolverTest
         CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans, trans));
 
     Solver slv = new Solver();
+    slv.setOption("sygus", "true");
     Sort boolean2 = slv.getBooleanSort();
     Sort real2 = slv.getRealSort();
     Term inv22 = slv.declareFun("inv", new Sort[] {real2}, boolean2);
@@ -2611,9 +2623,16 @@ class SolverTest
     slv.close();
   }
 
+  @Test void checkSynth() throws CVC5ApiException
+  {
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSynth());
+    d_solver.setOption("sygus", "true");
+    assertDoesNotThrow(() -> d_solver.checkSynth());
+  }
+
   @Test void getSynthSolution() throws CVC5ApiException
   {
-    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("sygus", "true");
     d_solver.setOption("incremental", "false");
 
     Term nullTerm = d_solver.getNullTerm();
@@ -2637,7 +2656,7 @@ class SolverTest
 
   @Test void getSynthSolutions() throws CVC5ApiException
   {
-    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("sygus", "true");
     d_solver.setOption("incremental", "false");
 
     Term nullTerm = d_solver.getNullTerm();
@@ -2662,7 +2681,7 @@ class SolverTest
   }
   @Test void checkSynthNext() throws CVC5ApiException
   {
-    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("sygus", "true");
     d_solver.setOption("incremental", "true");
     Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
 
@@ -2674,7 +2693,7 @@ class SolverTest
 
   @Test void checkSynthNext2() throws CVC5ApiException
   {
-    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("sygus", "true");
     d_solver.setOption("incremental", "false");
     Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
 
@@ -2684,7 +2703,7 @@ class SolverTest
 
   @Test void checkSynthNext3() throws CVC5ApiException
   {
-    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("sygus", "true");
     d_solver.setOption("incremental", "true");
     Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
 

diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
index dd50da4c413dd4edf31652fb448ba38cd9476cab..6bdd504f237865c0732487579ec8d5d9193f9768 100644 (file)
--- a/test/unit/api/python/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
@@ -25,6 +25,7 @@ def solver():
 
 
 def test_add_rule(solver):
+    solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()
     integer = solver.getIntegerSort()
 
@@ -58,6 +59,7 @@ def test_add_rule(solver):
 
 
 def test_add_rules(solver):
+    solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()
     integer = solver.getIntegerSort()
 
@@ -89,6 +91,7 @@ def test_add_rules(solver):
 
 
 def test_add_any_constant(solver):
+    solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()
 
     null_term = Term(solver)
@@ -112,6 +115,7 @@ def test_add_any_constant(solver):
 
 
 def test_add_any_variable(solver):
+    solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()
 
     null_term = Term(solver)

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index e47ee8f6fe5de502ba8b140aebe81cc8f9f43a90..6329c10111969e0ce87ac1fb43c3fef96b232dc5 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1915,6 +1915,7 @@ def test_mk_sygus_grammar(solver):
 
 
 def test_synth_inv(solver):
+    solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()
     integer = solver.getIntegerSort()
 
@@ -1941,6 +1942,7 @@ def test_synth_inv(solver):
 
 
 def test_add_sygus_constraint(solver):
+    solver.setOption("sygus", "true")
     nullTerm = cvc5.Term(solver)
     boolTerm = solver.mkBoolean(True)
     intTerm = solver.mkInteger(1)
@@ -1957,6 +1959,7 @@ def test_add_sygus_constraint(solver):
 
 
 def test_add_sygus_inv_constraint(solver):
+    solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()
     real = solver.getRealSort()
 
@@ -2008,6 +2011,7 @@ def test_add_sygus_inv_constraint(solver):
     with pytest.raises(RuntimeError):
         solver.addSygusInvConstraint(inv, pre, trans, trans)
     slv = cvc5.Solver()
+    slv.setOption("sygus", "true")
     boolean2 = slv.getBooleanSort()
     real2 = slv.getRealSort()
     inv22 = slv.declareFun("inv", [real2], boolean2)
@@ -2025,8 +2029,14 @@ def test_add_sygus_inv_constraint(solver):
         slv.addSygusInvConstraint(inv22, pre22, trans22, post)
 
 
+def test_check_synth(solver):
+    with pytest.raises(RuntimeError):
+        solver.checkSynth()
+    solver.setOption("sygus", "true")
+    solver.checkSynth()
+
 def test_get_synth_solution(solver):
-    solver.setOption("lang", "sygus2")
+    solver.setOption("sygus", "true")
     solver.setOption("incremental", "false")
 
     nullTerm = cvc5.Term(solver)
@@ -2051,7 +2061,7 @@ def test_get_synth_solution(solver):
         slv.getSynthSolution(f)
 
 def test_check_synth_next(solver):
-    solver.setOption("lang", "sygus2")
+    solver.setOption("sygus", "true")
     solver.setOption("incremental", "true")
     f = solver.synthFun("f", [], solver.getBooleanSort())
 
@@ -2062,7 +2072,7 @@ def test_check_synth_next(solver):
     solver.getSynthSolutions([f])
 
 def test_check_synth_next2(solver):
-    solver.setOption("lang", "sygus2")
+    solver.setOption("sygus", "true")
     solver.setOption("incremental", "false")
     f = solver.synthFun("f", [], solver.getBooleanSort())
 
@@ -2071,7 +2081,7 @@ def test_check_synth_next2(solver):
         solver.checkSynthNext()
 
 def test_check_synth_next3(solver):
-    solver.setOption("lang", "sygus2")
+    solver.setOption("sygus", "true")
     solver.setOption("incremental", "true")
     f = solver.synthFun("f", [], solver.getBooleanSort())
     with pytest.raises(RuntimeError):
@@ -2245,7 +2255,7 @@ def test_get_model_domain_elements(solver):
 
 
 def test_get_synth_solutions(solver):
-    solver.setOption("lang", "sygus2")
+    solver.setOption("sygus", "true")
     solver.setOption("incremental", "false")
 
     nullTerm = cvc5.Term(solver)
@@ -2462,20 +2472,22 @@ def test_mk_sygus_var(solver):
     intSort = solver.getIntegerSort()
     funSort = solver.mkFunctionSort(intSort, boolSort)
 
-    solver.mkSygusVar(boolSort)
-    solver.mkSygusVar(funSort)
-    solver.mkSygusVar(boolSort, "b")
-    solver.mkSygusVar(funSort, "")
+    solver.declareSygusVar(boolSort)
+    solver.declareSygusVar(funSort)
+    solver.declareSygusVar(boolSort, "b")
+    solver.declareSygusVar(funSort, "")
     with pytest.raises(RuntimeError):
-        solver.mkSygusVar(cvc5.Sort(solver))
+        solver.declareSygusVar(cvc5.Sort(solver))
     with pytest.raises(RuntimeError):
-        solver.mkSygusVar(solver.getNullSort(), "a")
+        solver.declareSygusVar(solver.getNullSort(), "a")
     slv = cvc5.Solver()
+    solver.setOption("sygus", "true")
     with pytest.raises(RuntimeError):
-        slv.mkSygusVar(boolSort)
+        slv.declareSygusVar(boolSort)
 
 
 def test_synth_fun(solver):
+    solver.setOption("sygus", "true")
     null = solver.getNullSort()
     boolean = solver.getBooleanSort()
     integer = solver.getIntegerSort()
@@ -2503,6 +2515,7 @@ def test_synth_fun(solver):
     with pytest.raises(RuntimeError):
         solver.synthFun("f6", [x], boolean, g2)
     slv = cvc5.Solver()
+    solver.setOption("sygus", "true")
     x2 = slv.mkVar(slv.getBooleanSort())
     slv.synthFun("f1", [x2], slv.getBooleanSort())
     with pytest.raises(RuntimeError):