This allows SyGuS subsolvers to be called multiple times to produce solutions for a given set of SyGuS constraints using a new command check-synth-next.
By default, the SyGuS subsolver will generate a new solution for each successive check-synth.
This simplifies the internal SyGuS solver in several ways for this purpose. It also ensures that solutions are cached; current master may recompute solutions in the same state more than once if asked, which is no longer the case.
This completes our support for incremental SyGuS.
CVC5_API_TRY_CATCH_END;
}
+Result Solver::checkSynthNext() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
+ << "Cannot checkSynthNext when not solving incrementally (use "
+ "--incremental)";
+ //////// all checks before this line
+ return d_slv->checkSynth(true);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
Term Solver::getSynthSolution(Term term) const
{
CVC5_API_TRY_CATCH_BEGIN;
* (check-synth)
* \endverbatim
*
- * @return the result of the synthesis conjecture.
+ * @return the result of the check, which is unsat if the check succeeded,
+ * in which case solutions are available via getSynthSolutions.
*/
Result checkSynth() const;
+ /**
+ * Try to find a next solution for the synthesis conjecture corresponding to
+ * the current list of functions-to-synthesize, universal variables and
+ * constraints. Must be called immediately after a successful call to
+ * check-synth or check-synth-next. Requires incremental mode.
+ *
+ * SyGuS v2:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-synth-next)
+ * \endverbatim
+ *
+ * @return the result of the check, which is unsat if the check succeeded,
+ * in which case solutions are available via getSynthSolutions.
+ */
+ Result checkSynthNext() const;
+
/**
* Get the synthesis solution of the given term. This method should be called
* immediately after the solver answers unsat for sygus input.
* {@code
* ( check-synth )
* }
- * @return the result of the synthesis conjecture.
+ * @return the result of the check, which is unsat if the check succeeded,
+ * in which case solutions are available via getSynthSolutions.
*/
public Result checkSynth()
{
private native long checkSynth(long pointer);
+ /**
+ * Try to find a next solution for the synthesis conjecture corresponding to
+ * the current list of functions-to-synthesize, universal variables and
+ * constraints. Must be called immediately after a successful call to
+ * check-synth or check-synth-next. Requires incremental mode.
+ * SyGuS v2:
+ * {@code
+ * ( check-synth-next )
+ * }
+ * @return the result of the check, which is UNSAT if the check succeeded,
+ * in which case solutions are available via getSynthSolutions.
+ */
+ public Result checkSynthNext()
+ {
+ long resultPointer = checkSynthNext(pointer);
+ return new Result(this, resultPointer);
+ }
+
+ private native long checkSynthNext(long pointer);
+
/**
* Get the synthesis solution of the given term. This method should be called
* immediately after the solver answers unsat for sygus input.
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
+/*
+ * Class: io_github_cvc5_api_Solver
+ * Method: checkSynthNext
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynthNext(
+ JNIEnv* env, jobject, jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ Result* retPointer = new Result(solver->checkSynthNext());
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
/*
* Class: io_github_cvc5_api_Solver
* Method: getSynthSolution
Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except +
Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except +
Result checkSynth() except +
+ Result checkSynthNext() except +
Term getSynthSolution(Term t) except +
vector[Term] getSynthSolutions(const vector[Term]& terms) except +
Term synthInv(const string& symbol, const vector[Term]& bound_vars) except +
r.cr = self.csolver.checkSynth()
return r
+ def checkSynthNext(self):
+ """
+ Try to find a next solution for the synthesis conjecture corresponding
+ to the current list of functions-to-synthesize, universal variables and
+ constraints. Must be called immediately after a successful call to
+ check-synth or check-synth-next. Requires incremental mode.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( check-synth )
+
+ :return: the result of the check, which is unsat if the check succeeded,
+ in which case solutions are available via getSynthSolutions.
+ """
+ cdef Result r = Result()
+ r.cr = self.csolver.checkSynthNext()
+ return r
+
def getSynthSolution(self, Term term):
"""
Get the synthesis solution of the given term. This method should be
PARSER_STATE->checkThatLogicIsSet();
cmd.reset(new CheckSynthCommand());
}
+ | /* check-synth-next */
+ CHECK_SYNTH_NEXT_TOK
+ {
+ PARSER_STATE->checkThatLogicIsSet();
+ cmd.reset(new CheckSynthCommand(true));
+ }
| /* set-feature */
SET_FEATURE_TOK keyword[name] symbolicExpr[expr]
{
SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun';
SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
+CHECK_SYNTH_NEXT_TOK : { PARSER_STATE->sygus()}?'check-synth-next';
DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
{
printUnknownCommand(out, "check-synth");
}
+void Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
+{
+ printUnknownCommand(out, "check-synth-next");
+}
void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
{
/** Print check-synth command */
virtual void toStreamCmdCheckSynth(std::ostream& out) const;
+ /** Print check-synth-next command */
+ virtual void toStreamCmdCheckSynthNext(std::ostream& out) const;
+
/** Print simplify command */
virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
out << "(check-synth)" << std::endl;
}
+void Smt2Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
+{
+ out << "(check-synth-next)" << std::endl;
+}
+
void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
const std::string& name,
Node conj,
/** Print check-synth command */
void toStreamCmdCheckSynth(std::ostream& out) const override;
+ /** Print check-synth-next command */
+ void toStreamCmdCheckSynthNext(std::ostream& out) const override;
+
/** Print simplify command */
void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
{
try
{
- d_result = solver->checkSynth();
+ d_result = d_isNext ? solver->checkSynthNext() : solver->checkSynth();
d_commandStatus = CommandSuccess::instance();
d_solution.clear();
// check whether we should print the status
Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
-std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
+std::string CheckSynthCommand::getCommandName() const
+{
+ return d_isNext ? "check-synth-next" : "check-synth";
+}
void CheckSynthCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
Language language) const
{
- Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+ if (d_isNext)
+ {
+ Printer::getPrinter(language)->toStreamCmdCheckSynthNext(out);
+ }
+ else
+ {
+ Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+ }
}
/* -------------------------------------------------------------------------- */
class CVC5_EXPORT CheckSynthCommand : public Command
{
public:
- CheckSynthCommand(){};
+ CheckSynthCommand(bool isNext = false) : d_isNext(isNext){};
/** returns the result of the check-synth call */
api::Result getResult() const;
/** prints the result of the check-synth-call */
Language language = Language::LANG_AUTO) const override;
protected:
+ /** Whether this is a check-synth-next call */
+ bool d_isNext;
/** result of the check-synth call */
api::Result d_result;
/** string stream that stores the output of the solution */
case SmtMode::UNSAT: out << "UNSAT"; break;
case SmtMode::ABDUCT: out << "ABDUCT"; break;
case SmtMode::INTERPOL: out << "INTERPOL"; break;
+ case SmtMode::SYNTH: out << "SYNTH"; break;
default: out << "SmtMode!Unknown"; break;
}
return out;
// immediately after a successful call to get-abduct
ABDUCT,
// immediately after a successful call to get-interpol
- INTERPOL
+ INTERPOL,
+ // immediately after a successful call to check-synth or check-synth-next
+ SYNTH
};
/**
* Writes a SmtMode to a stream.
d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
}
-Result SolverEngine::checkSynth()
+Result SolverEngine::checkSynth(bool isNext)
{
SolverEngineScope smts(this);
finishInit();
- return d_sygusSolver->checkSynth(*d_asserts);
+ if (isNext && d_state->getMode() != SmtMode::SYNTH)
+ {
+ throw RecoverableModalException(
+ "Cannot check-synth-next unless immediately preceded by a successful "
+ "call to check-synth.");
+ }
+ Result r = d_sygusSolver->checkSynth(*d_asserts, isNext);
+ d_state->notifyCheckSynthResult(r);
+ return r;
}
/*
* in which f1...fn are the functions-to-synthesize, v1...vm are the declared
* universal variables and F is the set of declared constraints.
*
+ * @param isNext Whether we are asking for the next synthesis solution (if
+ * using incremental).
+ *
* @throw Exception
*/
- Result checkSynth();
+ Result checkSynth(bool isNext = false);
/*------------------------- end of sygus commands ------------------------*/
}
}
+void SolverEngineState::notifyCheckSynthResult(Result r)
+{
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ // successfully generated a synthesis solution, update to abduct state
+ d_smtMode = SmtMode::SYNTH;
+ }
+ else
+ {
+ // failed, we revert to the assert state
+ d_smtMode = SmtMode::ASSERT;
+ }
+}
+
void SolverEngineState::notifyGetAbduct(bool success)
{
if (success)
* @param r The result of the check-sat call.
*/
void notifyCheckSatResult(bool hasAssumptions, Result r);
+ /**
+ * Notify that the result of the last check-synth or check-synth-next was r.
+ * @param r The result of the check-synth or check-synth-next call.
+ */
+ void notifyCheckSynthResult(Result r);
/**
* Notify that we finished an abduction query, where success is whether the
* command was successful. This is managed independently of the above
d_sygusConjectureStale = true;
}
-Result SygusSolver::checkSynth(Assertions& as)
+Result SygusSolver::checkSynth(Assertions& as, bool isNext)
{
Trace("smt") << "SygusSolver::checkSynth" << std::endl;
// if applicable, check if the subsolver is the correct one
+ if (!isNext)
+ {
+ // if we are not using check-synth-next, we always reconstruct the solver.
+ d_sygusConjectureStale = true;
+ }
if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get())
{
// this can occur if we backtrack to a place where we were using a different
// the subsolver.
d_sygusConjectureStale = true;
}
- // TODO (project #7): we currently must always rebuild the synthesis
- // conjecture + subsolver, since it answers unsat. When the subsolver is
- // updated to treat "sat" as solution for synthesis conjecture, this line
- // will be deleted.
- d_sygusConjectureStale = true;
if (d_sygusConjectureStale)
{
NodeManager* nm = NodeManager::currentNM();
* in which f1...fn are the functions-to-synthesize, v1...vm are the declared
* universal variables and F is the set of declared constraints.
*/
- Result checkSynth(Assertions& as);
+ Result checkSynth(Assertions& as, bool isNext);
/**
* Get synth solution.
*
d_tds(tr.getTermDatabaseSygus()),
d_verify(env, d_tds),
d_hasSolution(false),
+ d_computedSolution(false),
d_ceg_si(new CegSingleInv(env, tr, s)),
d_templInfer(new SygusTemplateInfer(env)),
d_ceg_proc(new SynthConjectureProcess(env)),
void SynthConjecture::presolve()
{
- // we don't have a solution yet
- d_hasSolution = false;
+ // If we previously had a solution, block it. Notice that
+ // excludeCurrentSolution in the block below ensures we implement a
+ // policy where a *new* solution is generated for check-synth if the set of
+ // SyGuS constraints has not changed. This call will block solutions for
+ // *smart* enumerators only. This behavior makes smart enumeration have
+ // a consistent policy with *fast* enumerators, which will generate
+ // a new, next solution in their enumeration.
+ if (d_hasSolution)
+ {
+ excludeCurrentSolution(d_solutionValues.back());
+ // we don't have a solution yet
+ d_hasSolution = false;
+ d_computedSolution = false;
+ d_sol.clear();
+ d_solStatus.clear();
+ }
}
void SynthConjecture::assign(Node q)
{
// have we tried to repair the previous solution?
// if not, call the repair constant utility
- unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
+ size_t ninst = d_solutionValues.size();
if (d_repair_index < ninst)
{
- std::vector<Node> fail_cvs;
- for (const Node& cprog : d_candidates)
- {
- Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
- fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
- }
+ std::vector<Node> fail_cvs = d_solutionValues[d_repair_index];
if (Trace.isOn("sygus-engine"))
{
Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
{
if (!checkSideCondition(candidate_values))
{
- excludeCurrentSolution(terms, candidate_values);
+ excludeCurrentSolution(candidate_values);
Trace("sygus-engine") << "...failed side condition" << std::endl;
return false;
}
// In the rare case that the subcall is unknown, we simply exclude the
// solution, without adding a counterexample point. This should only
// happen if the quantifier free logic is undecidable.
- excludeCurrentSolution(terms, candidate_values);
+ excludeCurrentSolution(candidate_values);
// We should set incomplete, since a "sat" answer should not be
// interpreted as "infeasible", which would make a difference in the rare
// case where e.g. we had a finite grammar and exhausted the grammar.
if (options().quantifiers.sygusStream)
{
// immediately print the current solution
- printAndContinueStream(terms, candidate_values);
+ printAndContinueStream(candidate_values);
// streaming means now we immediately are looking for a new solution
d_hasSolution = false;
+ d_computedSolution = false;
+ d_sol.clear();
+ d_solStatus.clear();
return false;
}
// We set incomplete and terminate with unknown.
Trace("sygus-engine-debug") << " ...(warning) failed to refine candidate, "
"manually exclude candidate."
<< std::endl;
- std::vector<Node> cvals;
- for (const Node& c : d_candidates)
- {
- cvals.push_back(d_cinfo[c].d_inst.back());
- }
+ std::vector<Node> cvals = d_solutionValues.back();
// something went wrong, exclude the current candidate
- excludeCurrentSolution(d_candidates, cvals);
+ excludeCurrentSolution(cvals);
// Note this happens when evaluation is incapable of disproving a candidate
// for counterexample point c, but satisfiability checking happened to find
// the the same point c is indeed a true counterexample. It is sound
Trace(c) << " * Counterexample skolems : " << d_innerSks << std::endl;
}
-void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
- const std::vector<Node>& values)
+void SynthConjecture::printAndContinueStream(const std::vector<Node>& values)
{
Assert(d_master != nullptr);
// we have generated a solution, print it
// get the current output stream
printSynthSolutionInternal(*options().base.out);
- excludeCurrentSolution(enums, values);
+ excludeCurrentSolution(values);
}
-void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
- const std::vector<Node>& values)
+void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& values)
{
- Trace("cegqi-debug") << "Exclude current solution: " << enums << " / "
- << values << std::endl;
+ Assert(values.size() == d_candidates.size());
+ Trace("cegqi-debug") << "Exclude current solution: " << values << std::endl;
// However, we need to exclude the current solution using an explicit
// blocking clause, so that we proceed to the next solution. We do this only
// for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
std::vector<Node> exp;
- for (unsigned i = 0, tsize = enums.size(); i < tsize; i++)
+ for (size_t i = 0, tsize = d_candidates.size(); i < tsize; i++)
{
- Node cprog = enums[i];
+ Node cprog = d_candidates[i];
Assert(d_tds->isEnumerator(cprog));
if (d_tds->isPassiveEnumerator(cprog))
{
return true;
}
-void SynthConjecture::recordSolution(std::vector<Node>& vs)
+void SynthConjecture::recordSolution(const std::vector<Node>& vs)
{
Assert(vs.size() == d_candidates.size());
- d_cinfo.clear();
- for (unsigned i = 0; i < vs.size(); i++)
- {
- d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
- }
+ d_solutionValues.clear();
+ d_solutionValues.push_back(vs);
}
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
{
return false;
}
+ if (d_computedSolution)
+ {
+ sols.insert(sols.end(), d_sol.begin(), d_sol.end());
+ statuses.insert(statuses.end(), d_solStatus.begin(), d_solStatus.end());
+ return true;
+ }
+ d_computedSolution = true;
+ // get the (SyGuS datatype) values of the solutions, if they exist
+ std::vector<Node> svals;
+ if (!d_solutionValues.empty())
+ {
+ svals = d_solutionValues.back();
+ }
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
Node prog = d_embed_quant[0][i];
else
{
Node cprog = d_candidates[i];
- if (!d_cinfo[cprog].d_inst.empty())
+ if (!svals.empty())
{
- // the solution is just the last instantiated term
- sol = d_cinfo[cprog].d_inst.back();
+ // the solution is the value of the last term
+ sol = svals[i];
status = 1;
// check if there was a template
<< std::endl;
}
}
- sols.push_back(sol);
- statuses.push_back(status);
+ d_sol.push_back(sol);
+ d_solStatus.push_back(status);
}
+ sols.insert(sols.end(), d_sol.begin(), d_sol.end());
+ statuses.insert(statuses.end(), d_solStatus.begin(), d_solStatus.end());
return true;
}
TermRegistry& tr,
SygusStatistics& s);
~SynthConjecture();
- /** presolve */
+ /**
+ * Presolve, called once at the beginning of every check-sat.
+ */
void presolve();
/** get original version of conjecture */
Node getConjecture() const { return d_quant; }
* on every call to presolve.
*/
bool d_hasSolution;
+ /** Whether we have computed a solution */
+ bool d_computedSolution;
+ /**
+ * The final solution and status, caches getSynthSolutionsInternal, valid
+ * if d_computedSolution is true.
+ */
+ std::vector<Node> d_sol;
+ std::vector<int8_t> d_solStatus;
+ /**
+ * (SyGuS datatype) values for solutions, which is populated if we have a
+ * solution and only if we are not using the single invocation solver.
+ */
+ std::vector<std::vector<Node>> d_solutionValues;
/** the decision strategy for the feasible guard */
std::unique_ptr<DecisionStrategy> d_feasible_strategy;
/** single invocation utility */
Node d_simp_quant;
/** (negated) conjecture after simplification, conversion to deep embedding */
Node d_embed_quant;
- /** candidate information */
- class CandidateInfo
- {
- public:
- CandidateInfo() {}
- /** list of terms we have instantiated candidates with */
- std::vector<Node> d_inst;
- };
- std::map<Node, CandidateInfo> d_cinfo;
/**
* The first index of an instantiation in CandidateInfo::d_inst that we have
* not yet tried to repair.
*/
unsigned d_repair_index;
/** record solution (this is used to construct solutions later) */
- void recordSolution(std::vector<Node>& vs);
+ void recordSolution(const std::vector<Node>& vs);
/** get synth solutions internal
*
* This function constructs the body of solutions for all
* The argument enums is the set of enumerators that comprise the current
* solution, and values is their current values.
*/
- void printAndContinueStream(const std::vector<Node>& enums,
- const std::vector<Node>& values);
+ void printAndContinueStream(const std::vector<Node>& values);
/** exclude the current solution { enums -> values } */
- void excludeCurrentSolution(const std::vector<Node>& enums,
- const std::vector<Node>& values);
+ void excludeCurrentSolution(const std::vector<Node>& values);
/**
* Whether we have guarded a stream exclusion lemma when using sygusStream.
* This is an optimization that allows us to guard only the first stream
regress1/sygus/icfp_14_12_diff_types.sy
regress1/sygus/icfp_28_10.sy
regress1/sygus/icfp_easy-ite.sy
+ regress1/sygus/incremental-stream-ex.sy
regress1/sygus/int-any-const.sy
regress1/sygus/inv-example.sy
regress1/sygus/inv-missed-sol-true.sy
--- /dev/null
+; COMMAND-LINE: -i --sygus-out=status
+;EXPECT: unsat
+;EXPECT: unsat
+;EXPECT: unsat
+;EXPECT: unsat
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+ ((Start Int) (StartBool Bool))
+ ((Start Int (0 1 x y
+ (+ Start Start)
+ (- Start Start)
+ (ite StartBool Start Start)))
+ (StartBool Bool ((and StartBool StartBool)
+ (not StartBool)
+ (<= Start Start)))))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (f x y) 0))
+
+(check-synth)
+(check-synth-next)
+(check-synth-next)
+(check-synth-next)
ASSERT_THROW(slv.getSynthSolutions({x}), CVC5ApiException);
}
+TEST_F(TestApiBlackSolver, checkSynthNext)
+{
+ d_solver.setOption("lang", "sygus2");
+ d_solver.setOption("incremental", "true");
+ Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+ d_solver.checkSynth();
+ ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
+ d_solver.checkSynthNext();
+ ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
+}
+
+TEST_F(TestApiBlackSolver, checkSynthNext2)
+{
+ d_solver.setOption("lang", "sygus2");
+ d_solver.setOption("incremental", "false");
+ Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+ d_solver.checkSynth();
+ ASSERT_THROW(d_solver.checkSynthNext(), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, checkSynthNext3)
+{
+ d_solver.setOption("lang", "sygus2");
+ d_solver.setOption("incremental", "true");
+ Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+ ASSERT_THROW(d_solver.checkSynthNext(), CVC5ApiException);
+}
+
TEST_F(TestApiBlackSolver, tupleProject)
{
std::vector<Sort> sorts = {d_solver.getBooleanSort(),
assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
slv.close();
}
+ @Test void checkSynthNext() throws CVC5ApiException
+ {
+ d_solver.setOption("lang", "sygus2");
+ d_solver.setOption("incremental", "true");
+ Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+ d_solver.checkSynth();
+ assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
+ d_solver.checkSynthNext();
+ assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
+ }
+
+ @Test void checkSynthNext2() throws CVC5ApiException
+ {
+ d_solver.setOption("lang", "sygus2");
+ d_solver.setOption("incremental", "false");
+ Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+ d_solver.checkSynth();
+ assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
+ }
+
+ @Test void checkSynthNext3() throws CVC5ApiException
+ {
+ d_solver.setOption("lang", "sygus2");
+ d_solver.setOption("incremental", "true");
+ Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+ assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
+ }
@Test void tupleProject() throws CVC5ApiException
{
with pytest.raises(RuntimeError):
slv.getSynthSolution(f)
+def test_check_synth_next(solver):
+ solver.setOption("lang", "sygus2")
+ solver.setOption("incremental", "true")
+ f = solver.synthFun("f", [], solver.getBooleanSort())
+
+ solver.checkSynth()
+ solver.getSynthSolutions([f])
+
+ solver.checkSynthNext()
+ solver.getSynthSolutions([f])
+
+def test_check_synth_next2(solver):
+ solver.setOption("lang", "sygus2")
+ solver.setOption("incremental", "false")
+ f = solver.synthFun("f", [], solver.getBooleanSort())
+
+ solver.checkSynth()
+ with pytest.raises(RuntimeError):
+ solver.checkSynthNext()
+
+def test_check_synth_next3(solver):
+ solver.setOption("lang", "sygus2")
+ solver.setOption("incremental", "true")
+ f = solver.synthFun("f", [], solver.getBooleanSort())
+ with pytest.raises(RuntimeError):
+ solver.checkSynthNext()
def test_declare_pool(solver):
intSort = solver.getIntegerSort()
projects / cvc5.git / commitdiff