From: Andrew Reynolds Date: Mon, 20 Dec 2021 15:23:16 +0000 (-0600) Subject: Allow SyGuS subsolver to be reused in incremental mode (#7785) X-Git-Tag: cvc5-1.0.0~630 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=20d040d79b5e0b3d42e605b1e951f837b66422c1;p=cvc5.git Allow SyGuS subsolver to be reused in incremental mode (#7785) 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. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 24b4500d5..bdaef769e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7944,6 +7944,18 @@ Result Solver::checkSynth() const 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; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index f2bfb48e2..3b22f0c6f 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4811,10 +4811,30 @@ class CVC5_EXPORT Solver * (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. diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index d04b766e0..64bef09c9 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2594,7 +2594,8 @@ public class Solver implements IPointer, AutoCloseable * {@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() { @@ -2604,6 +2605,26 @@ public class Solver implements IPointer, AutoCloseable 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. diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 8008ebada..73e481b49 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2629,6 +2629,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynth(JNIEnv* env, 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(pointer); + Result* retPointer = new Result(solver->checkSynthNext()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: getSynthSolution diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 5a33628a6..552fe6399 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -204,6 +204,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": 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 + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index d3f58ce62..63e21bf7e 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1694,6 +1694,26 @@ cdef class Solver: 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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 41cd4869a..7f95368b0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -576,6 +576,12 @@ sygusCommand returns [std::unique_ptr cmd] 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] { @@ -2240,6 +2246,7 @@ DECLARE_POOL : 'declare-pool'; 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'; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 16b626e30..d1c2c58a5 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -350,6 +350,10 @@ void Printer::toStreamCmdCheckSynth(std::ostream& out) const { 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 { diff --git a/src/printer/printer.h b/src/printer/printer.h index 485cd70e6..d55723443 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -165,6 +165,9 @@ class Printer /** 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; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 875ca7dc2..2a20bba36 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1899,6 +1899,11 @@ void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) 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, diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 4ee333f67..b97ad2ffb 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -142,6 +142,9 @@ class Smt2Printer : public cvc5::Printer /** 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; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 1321c558e..ac393d568 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -833,7 +833,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) { 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 @@ -901,14 +901,24 @@ void CheckSynthCommand::printResult(std::ostream& out) const 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); + } } /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 6ca5a7fc8..1a00c2ada 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -821,7 +821,7 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command 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 */ @@ -846,6 +846,8 @@ class CVC5_EXPORT CheckSynthCommand : public Command 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 */ diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp index 6a6e35dd9..37d1d5950 100644 --- a/src/smt/smt_mode.cpp +++ b/src/smt/smt_mode.cpp @@ -30,6 +30,7 @@ std::ostream& operator<<(std::ostream& out, SmtMode m) 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; diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index aff9b6366..098bf1cb7 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -42,7 +42,9 @@ enum class SmtMode // 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. diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 13d061f1f..09814c300 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -934,11 +934,19 @@ void SolverEngine::assertSygusInvConstraint(Node inv, 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; } /* diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 1299a493a..ecfb521a0 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -451,9 +451,12 @@ class CVC5_EXPORT SolverEngine * 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 ------------------------*/ diff --git a/src/smt/solver_engine_state.cpp b/src/smt/solver_engine_state.cpp index 8558e91cf..4ec577b68 100644 --- a/src/smt/solver_engine_state.cpp +++ b/src/smt/solver_engine_state.cpp @@ -113,6 +113,20 @@ void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) } } +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) diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h index 7a06b0510..5cc72fd08 100644 --- a/src/smt/solver_engine_state.h +++ b/src/smt/solver_engine_state.h @@ -87,6 +87,11 @@ class SolverEngineState : protected EnvObj * @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 diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 70ad65644..692a123db 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -183,10 +183,15 @@ void SygusSolver::assertSygusInvConstraint(Node inv, 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 @@ -194,11 +199,6 @@ Result SygusSolver::checkSynth(Assertions& as) // 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(); diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 4e7a04364..b37762ce1 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -131,7 +131,7 @@ class SygusSolver : protected EnvObj * 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. * diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e5dfe408b..2a1258082 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -59,6 +59,7 @@ SynthConjecture::SynthConjecture(Env& env, 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)), @@ -93,8 +94,22 @@ SynthConjecture::~SynthConjecture() {} 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) @@ -345,15 +360,10 @@ bool SynthConjecture::doCheck() { // 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 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 fail_cvs = d_solutionValues[d_repair_index]; if (Trace.isOn("sygus-engine")) { Trace("sygus-engine") << "CegConjuncture : repair previous solution "; @@ -468,7 +478,7 @@ bool SynthConjecture::doCheck() { if (!checkSideCondition(candidate_values)) { - excludeCurrentSolution(terms, candidate_values); + excludeCurrentSolution(candidate_values); Trace("sygus-engine") << "...failed side condition" << std::endl; return false; } @@ -555,7 +565,7 @@ bool SynthConjecture::doCheck() // 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. @@ -569,9 +579,12 @@ bool SynthConjecture::doCheck() 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. @@ -634,13 +647,9 @@ bool SynthConjecture::processCounterexample(const std::vector& skModel) Trace("sygus-engine-debug") << " ...(warning) failed to refine candidate, " "manually exclude candidate." << std::endl; - std::vector cvals; - for (const Node& c : d_candidates) - { - cvals.push_back(d_cinfo[c].d_inst.back()); - } + std::vector 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 @@ -728,28 +737,26 @@ void SynthConjecture::debugPrint(const char* c) Trace(c) << " * Counterexample skolems : " << d_innerSks << std::endl; } -void SynthConjecture::printAndContinueStream(const std::vector& enums, - const std::vector& values) +void SynthConjecture::printAndContinueStream(const std::vector& 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& enums, - const std::vector& values) +void SynthConjecture::excludeCurrentSolution(const std::vector& 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 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)) { @@ -935,14 +942,11 @@ bool SynthConjecture::getSynthSolutions( return true; } -void SynthConjecture::recordSolution(std::vector& vs) +void SynthConjecture::recordSolution(const std::vector& 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& sols, @@ -952,6 +956,19 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& 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 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]; @@ -974,10 +991,10 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, 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 @@ -1025,9 +1042,11 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, << 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; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 005ae4361..ce9788c50 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -62,7 +62,9 @@ class SynthConjecture : protected EnvObj 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; } @@ -197,6 +199,19 @@ class SynthConjecture : protected EnvObj * 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 d_sol; + std::vector 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> d_solutionValues; /** the decision strategy for the feasible guard */ std::unique_ptr d_feasible_strategy; /** single invocation utility */ @@ -283,22 +298,13 @@ class SynthConjecture : protected EnvObj 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 d_inst; - }; - std::map 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& vs); + void recordSolution(const std::vector& vs); /** get synth solutions internal * * This function constructs the body of solutions for all @@ -328,11 +334,9 @@ class SynthConjecture : protected EnvObj * The argument enums is the set of enumerators that comprise the current * solution, and values is their current values. */ - void printAndContinueStream(const std::vector& enums, - const std::vector& values); + void printAndContinueStream(const std::vector& values); /** exclude the current solution { enums -> values } */ - void excludeCurrentSolution(const std::vector& enums, - const std::vector& values); + void excludeCurrentSolution(const std::vector& 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 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 568fec3ce..4a54e2fcb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2468,6 +2468,7 @@ set(regress_1_tests 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 diff --git a/test/regress/regress1/sygus/incremental-stream-ex.sy b/test/regress/regress1/sygus/incremental-stream-ex.sy new file mode 100644 index 000000000..127a2e3bc --- /dev/null +++ b/test/regress/regress1/sygus/incremental-stream-ex.sy @@ -0,0 +1,28 @@ +; 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) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index f3bc91eaa..d96ff17a0 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2589,6 +2589,37 @@ TEST_F(TestApiBlackSolver, getSynthSolutions) 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 sorts = {d_solver.getBooleanSort(), diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index f6fa3d6f1..128141bfa 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -2584,6 +2584,36 @@ class SolverTest 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 { diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 1e9dbcf1f..0fe0d465e 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1960,6 +1960,32 @@ def test_get_synth_solution(solver): 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()