From: Andrew Reynolds Date: Fri, 25 Mar 2022 02:21:44 +0000 (-0500) Subject: Properly guard commands in the SyGuS API (#8390) X-Git-Tag: cvc5-1.0.0~179 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ae28c60383ca156cba69cfcc43062195ff59d3a;p=cvc5.git 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 37a69fbdb..978e55fe6 100644 --- 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 fc31a6a32..7be3cb062 100644 --- 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 aaff3e695..3b8edd53a 100644 --- 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 31aecdc94..07a0eebbc 100644 --- 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 af8816a40..25233617b 100644 --- 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 226e8e61e..f07a4816e 100644 --- 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 2f6417e35..82f3d08a7 100644 --- 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 41adad822..c6c158f79 100644 --- 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 249952a9e..90a3deca7 100644 --- 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 0eba91ee2..b229ef65f 100644 --- 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& 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 6d7f0417c..6d9b39df1 100644 --- 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 f1f2b91f6..183d2de95 100644 --- 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 f440c1646..87caff1b0 100644 --- 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(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(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 c057e20f1..f133f324d 100644 --- 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 3305352d3..354adaed1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1591,7 +1591,7 @@ cdef class Solver: grammar.cgrammar = self.csolver.mkSygusGrammar( bvc, 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 f104f3fa7..5c3933e5a 100644 --- 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& 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 ac7392b86..f1476b94d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -518,7 +518,7 @@ sygusCommand returns [std::unique_ptr 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 2416b9eff..5e987b862 100644 --- 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 cae7190a2..f3e135cdc 100644 --- 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 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 rasserts = asserts; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index fc870b6ec..7a07ae996 100644 --- 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& conjunctions) -{ - Assert(conjunctions.size() > 0); - - std::set 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::const_iterator it = all.begin(); - std::set::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 c428eda3a..ee249bea4 100644 --- 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 44bccd264..b4702415b 100644 --- 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 7b7556539..1aa35db8d 100644 --- 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 7e6c113eb..7e9fd5880 100644 --- 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 37e1b5206..15d978692 100644 --- 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 cc94600f5..fe5afeee6 100644 --- 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 dd50da4c4..6bdd504f2 100644 --- 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 e47ee8f6f..6329c1011 100644 --- 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):