From: Andrew Reynolds Date: Wed, 22 Dec 2021 16:56:51 +0000 (-0600) Subject: Add support for incremental + interpolants (#7853) X-Git-Tag: cvc5-1.0.0~622 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c3cc154d0896568099c18ee6929439d49954e8f;p=cvc5.git Add support for incremental + interpolants (#7853) Adds support for incrementality + get-interpol, including the get-interpol-next command. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4c43dbd5b..be5f1017d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7579,9 +7579,14 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + << "Cannot get interpolant unless interpolants are enabled (try " + "--produce-interpols=mode)"; //////// all checks before this line Node result; - bool success = d_slv->getInterpol(*conj.d_node, result); + TypeNode nullType; + bool success = d_slv->getInterpolant(*conj.d_node, nullType, result); if (success) { output = Term(this, result); @@ -7597,10 +7602,36 @@ bool Solver::getInterpolant(const Term& conj, { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + << "Cannot get interpolant unless interpolants are enabled (try " + "--produce-interpols=mode)"; //////// all checks before this line Node result; bool success = - d_slv->getInterpol(*conj.d_node, *grammar.resolve().d_type, result); + d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type, result); + if (success) + { + output = Term(this, result); + } + return success; + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Solver::getInterpolantNext(Term& output) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + << "Cannot get interpolant unless interpolants are enabled (try " + "--produce-interpols=mode)"; + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) + << "Cannot get next interpolant when not solving incrementally (try " + "--incremental)"; + //////// all checks before this line + Node result; + bool success = d_slv->getInterpolantNext(result); if (success) { output = Term(this, result); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 7e4dc3cc8..21f51a9c8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4427,8 +4427,9 @@ class CVC5_EXPORT Solver * * (get-interpol ) * - * Requires to enable option - * :ref:`produce-interpols `. + * Requires option + * :ref:`produce-interpols ` to be set to a + * mode different from `none`. * \endverbatim * * @param conj the conjecture term @@ -4448,8 +4449,9 @@ class CVC5_EXPORT Solver * * (get-interpol ) * - * Requires to enable option - * :ref:`produce-interpols `. + * Requires option + * :ref:`produce-interpols ` to be set to a + * mode different from `none`. * \endverbatim * * @param conj the conjecture term @@ -4460,6 +4462,31 @@ class CVC5_EXPORT Solver */ bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const; + /** + * Get the next interpolant. Can only be called immediately after a successful + * call to get-interpol or get-interpol-next. Is guaranteed to produce a + * syntactically different interpolant wrt the last returned interpolant if + * successful. + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol-next) + * + * Requires to enable incremental mode, and option + * :ref:`produce-interpols ` to be set to a + * mode different from `none`. + * \endverbatim + * + * @param output a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj + * on the last call to getInterpolant. + * @return true if it gets interpolant @f$C@f$ successfully, false otherwise + */ + bool getInterpolantNext(Term& output) const; + /** * Get an abduct. * diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 32ddf0691..5e2ac0972 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2183,7 +2183,7 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( get-interpol ) * } - * Requires to enable option 'produce-interpols'. + * Requires 'produce-interpols' to be set to a mode different from 'none'. * @param conj the conjecture term * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the * current set of assertions and B is given in the input by conj. @@ -2202,7 +2202,7 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( get-interpol ) * } - * Requires to enable option 'produce-interpols'. + * Requires 'produce-interpols' to be set to a mode different from 'none'. * @param conj the conjecture term * @param grammar the grammar for the interpolant I * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the @@ -2217,6 +2217,35 @@ public class Solver implements IPointer, AutoCloseable private native boolean getInterpolant( long pointer, long conjPointer, long grammarPointer, long outputPointer); + /** + * Get the next interpolant. Can only be called immediately after a successful + * call to get-interpol or get-interpol-next. Is guaranteed to produce a + * syntactically different interpolant wrt the last returned interpolant if + * successful. + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol-next) + * + * Requires to enable incremental mode, and option 'produce-interpols' to be + * set to a mode different from 'none'. + * \endverbatim + * + * @param output a Term I such that {@code A->I} and {@code I->B} are valid, + * where A is the current set of assertions and B is given in the input + * by conj on the last call to getInterpolant. + * @return true if it gets interpolant @f$C@f$ successfully, false otherwise + */ + public boolean getInterpolantNext(Term output) + { + return getInterpolantNext(pointer, output.getPointer()); + } + + private native boolean getInterpolantNext(long pointer, long outputPointer); + /** * Get an abduct. * SMT-LIB: diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 524c52796..705803c12 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2243,6 +2243,21 @@ Java_io_github_cvc5_api_Solver_getInterpolant__JJJJ(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_api_Solver + * Method: getInterpolantNext + * Signature: (JJ)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext( + JNIEnv* env, jobject, jlong pointer, jlong outputPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast(pointer); + Term* output = reinterpret_cast(outputPointer); + return (jboolean)solver->getInterpolantNext(*output); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: getAbduct diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 31171b278..fafda041a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1022,6 +1022,10 @@ extendedCommand[std::unique_ptr* cmd] { cmd->reset(new GetInterpolCommand(name, e, g)); } + | GET_INTERPOL_NEXT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + cmd->reset(new GetInterpolNextCommand); + } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] sortSymbol[s, CHECK_DECLARED] @@ -2244,6 +2248,7 @@ GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; GET_ABDUCT_NEXT_TOK : 'get-abduct-next'; GET_INTERPOL_TOK : 'get-interpol'; +GET_INTERPOL_NEXT_TOK : 'get-interpol-next'; DECLARE_HEAP : 'declare-heap'; DECLARE_POOL : 'declare-pool'; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index a4ff10014..12b52e284 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -405,6 +405,11 @@ void Printer::toStreamCmdGetInterpol(std::ostream& out, printUnknownCommand(out, "get-interpol"); } +void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const +{ + printUnknownCommand(out, "get-interpol-next"); +} + void Printer::toStreamCmdGetAbduct(std::ostream& out, const std::string& name, Node conj, diff --git a/src/printer/printer.h b/src/printer/printer.h index 74eb8970b..2a9283001 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -200,6 +200,9 @@ class Printer Node conj, TypeNode sygusType) const; + /** Print get-interpol-next command */ + virtual void toStreamCmdGetInterpolNext(std::ostream& out) const; + /** Print get-abduct command */ virtual void toStreamCmdGetAbduct(std::ostream& out, const std::string& name, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e6c99c707..69da5d03d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1917,6 +1917,11 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out, out << ')' << std::endl; } +void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const +{ + out << "(get-interpol-next)" << std::endl; +} + void Smt2Printer::toStreamCmdGetAbduct(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 aad3948fe..bf6c20d40 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -174,6 +174,9 @@ class Smt2Printer : public cvc5::Printer Node conj, TypeNode sygusType) const override; + /** Print get-interpol-next command */ + void toStreamCmdGetInterpolNext(std::ostream& out) const override; + /** Print get-abduct command */ void toStreamCmdGetAbduct(std::ostream& out, const std::string& name, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 8161dfb49..e22c39d0e 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2007,6 +2007,9 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { + // we must remember the name of the interpolant, in case get-interpol-next + // is called later. + sm->setLastSynthName(d_name); if (d_sygus_grammar == nullptr) { d_resultStatus = solver->getInterpolant(d_conj, d_result); @@ -2069,6 +2072,72 @@ void GetInterpolCommand::toStream(std::ostream& out, out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar)); } +/* -------------------------------------------------------------------------- */ +/* class GetInterpolNextCommand */ +/* -------------------------------------------------------------------------- */ + +GetInterpolNextCommand::GetInterpolNextCommand() : d_resultStatus(false) {} + +api::Term GetInterpolNextCommand::getResult() const { return d_result; } + +void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm) +{ + try + { + // Get the name of the interpolant from the symbol manager + d_name = sm->getLastSynthName(); + d_resultStatus = solver->getInterpolantNext(d_result); + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetInterpolNextCommand::printResult(std::ostream& out) const +{ + if (!ok()) + { + this->Command::printResult(out); + } + else + { + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); + if (d_resultStatus) + { + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; + } + else + { + out << "none" << std::endl; + } + } +} + +Command* GetInterpolNextCommand::clone() const +{ + GetInterpolNextCommand* c = new GetInterpolNextCommand; + c->d_result = d_result; + c->d_resultStatus = d_resultStatus; + return c; +} + +std::string GetInterpolNextCommand::getCommandName() const +{ + return "get-interpol-next"; +} + +void GetInterpolNextCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + Language language) const +{ + Printer::getPrinter(language)->toStreamCmdGetInterpolNext(out); +} + /* -------------------------------------------------------------------------- */ /* class GetAbductCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 68ff7ffab..9a4b04196 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1058,6 +1058,35 @@ class CVC5_EXPORT GetInterpolCommand : public Command api::Term d_result; }; /* class GetInterpolCommand */ +/** The command (get-interpol-next) */ +class CVC5_EXPORT GetInterpolNextCommand : public Command +{ + public: + GetInterpolNextCommand(); + /** + * Get the result of the query, which is the solution to the interpolation + * query. + */ + api::Term getResult() const; + + void invoke(api::Solver* solver, SymbolManager* sm) override; + void printResult(std::ostream& out) const override; + Command* clone() const override; + std::string getCommandName() const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; + + protected: + /** The name of the interpolation predicate */ + std::string d_name; + /** the return status of the command */ + bool d_resultStatus; + /** the return expression of the command */ + api::Term d_result; +}; + /** The command (get-abduct s B (G)?) * * This command asks for an abduct from the current set of assertions and @@ -1134,7 +1163,7 @@ class CVC5_EXPORT GetAbductNextCommand : public Command bool d_resultStatus; /** the return expression of the command */ api::Term d_result; -}; /* class GetAbductCommand */ +}; class CVC5_EXPORT GetQuantifierEliminationCommand : public Command { diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 20be53e85..97d3a4224 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -36,10 +36,10 @@ InterpolationSolver::InterpolationSolver(Env& env) : EnvObj(env) {} InterpolationSolver::~InterpolationSolver() {} -bool InterpolationSolver::getInterpol(const std::vector& axioms, - const Node& conj, - const TypeNode& grammarType, - Node& interpol) +bool InterpolationSolver::getInterpolant(const std::vector& axioms, + const Node& conj, + const TypeNode& grammarType, + Node& interpol) { if (options().smt.produceInterpols == options::ProduceInterpols::NONE) { @@ -54,8 +54,8 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, conjn = rewrite(conjn); std::string name("__internal_interpol"); - quantifiers::SygusInterpol interpolSolver(d_env); - if (interpolSolver.solveInterpolation( + d_subsolver = std::make_unique(d_env); + if (d_subsolver->solveInterpolation( name, axioms, conjn, grammarType, interpol)) { if (options().smt.checkInterpols) @@ -67,12 +67,12 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, return false; } -bool InterpolationSolver::getInterpol(const std::vector& axioms, - const Node& conj, - Node& interpol) +bool InterpolationSolver::getInterpolantNext(Node& interpol) { - TypeNode grammarType; - return getInterpol(axioms, conj, grammarType, interpol); + // should already have initialized a subsolver, since we are immediately + // preceeded by a successful call to get-interpol(-next). + Assert(d_subsolver != nullptr); + return d_subsolver->solveInterpolationNext(interpol); } void InterpolationSolver::checkInterpol(Node interpol, diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 39a241816..d1f1c7fd8 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -23,6 +23,13 @@ #include "smt/env_obj.h" namespace cvc5 { + +namespace theory { +namespace quantifiers { +class SygusInterpol; +} +} // namespace theory + namespace smt { /** @@ -55,19 +62,24 @@ class InterpolationSolver : protected EnvObj * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getInterpol(const std::vector& axioms, - const Node& conj, - const TypeNode& grammarType, - Node& interpol); + bool getInterpolant(const std::vector& axioms, + const Node& conj, + const TypeNode& grammarType, + Node& interpol); /** - * Same as above, but without user-provided grammar restrictions. A default - * grammar is chosen internally using the sygus grammar constructor utility. + * Get next interpolant. This can only be called immediately after a + * successful call to getInterpolant or getInterpolantNext. + * + * Returns true if an interpolant was found, and sets interpol to the + * interpolant. + * + * This method reuses the subsolver initialized by the last call to + * getInterpolant. */ - bool getInterpol(const std::vector& axioms, - const Node& conj, - Node& interpol); + bool getInterpolantNext(Node& interpol); + private: /** * Check that a solution to an interpolation problem is indeed a solution. * @@ -78,6 +90,9 @@ class InterpolationSolver : protected EnvObj void checkInterpol(Node interpol, const std::vector& easserts, const Node& conj); + + /** The subsolver */ + std::unique_ptr d_subsolver; }; } // namespace smt diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 2df3eafa1..e7f2e2069 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1632,25 +1632,35 @@ Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict) *d_asserts, q, doFull, d_isInternalSubsolver); } -bool SolverEngine::getInterpol(const Node& conj, - const TypeNode& grammarType, - Node& interpol) +bool SolverEngine::getInterpolant(const Node& conj, + const TypeNode& grammarType, + Node& interpol) { SolverEngineScope smts(this); finishInit(); std::vector axioms = getExpandedAssertions(); bool success = - d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol); + d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol); // notify the state of whether the get-interpol call was successfuly, which // impacts the SMT mode. d_state->notifyGetInterpol(success); return success; } -bool SolverEngine::getInterpol(const Node& conj, Node& interpol) +bool SolverEngine::getInterpolantNext(Node& interpol) { - TypeNode grammarType; - return getInterpol(conj, grammarType, interpol); + SolverEngineScope smts(this); + finishInit(); + if (d_state->getMode() != SmtMode::INTERPOL) + { + throw RecoverableModalException( + "Cannot get-interpol-next unless immediately preceded by a successful " + "call to get-interpol(-next)."); + } + bool success = d_interpolSolver->getInterpolantNext(interpol); + // notify the state of whether the get-interpolant-next call was successful + d_state->notifyGetInterpol(success); + return success; } bool SolverEngine::getAbduct(const Node& conj, diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 165424594..99d2502b9 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -637,12 +637,18 @@ class CVC5_EXPORT SolverEngine * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getInterpol(const Node& conj, - const TypeNode& grammarType, - Node& interpol); + bool getInterpolant(const Node& conj, + const TypeNode& grammarType, + Node& interpol); - /** Same as above, but without user-provided grammar restrictions */ - bool getInterpol(const Node& conj, Node& interpol); + /** + * Get next interpolant. This can only be called immediately after a + * successful call to getInterpolant or getInterpolantNext. + * + * Returns true if an interpolant was found, and sets interpol to the + * interpolant. + */ + bool getInterpolantNext(Node& interpol); /** * This method asks this SMT engine to find an abduct with respect to the diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 3e1a5b34c..eb9bed3dc 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -323,36 +323,50 @@ bool SygusInterpol::solveInterpolation(const std::string& name, createVariables(itpGType.isNull()); TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); - Node itp = mkPredicate(name); - mkSygusConjecture(itp, axioms, conj); + d_itp = mkPredicate(name); + mkSygusConjecture(d_itp, axioms, conj); - std::unique_ptr subSolver; - initializeSubsolver(subSolver, d_env); + initializeSubsolver(d_subSolver, d_env); // get the logic - LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy(); + LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus l.enableSygus(); - subSolver->setLogic(l); + d_subSolver->setLogic(l); for (const Node& var : d_vars) { - subSolver->declareSygusVar(var); + d_subSolver->declareSygusVar(var); } std::vector vars_empty; - subSolver->declareSynthFun(itp, grammarType, false, vars_empty); - Trace("sygus-interpol") << "SolverEngine::getInterpol: made conjecture : " - << d_sygusConj << ", solving for " - << d_sygusConj[0][0] << std::endl; - subSolver->assertSygusConstraint(d_sygusConj); + d_subSolver->declareSynthFun(d_itp, grammarType, false, vars_empty); + Trace("sygus-interpol") + << "SygusInterpol::solveInterpolation: made conjecture : " << d_sygusConj + << ", solving for " << d_sygusConj[0][0] << std::endl; + d_subSolver->assertSygusConstraint(d_sygusConj); - Trace("sygus-interpol") << " SolverEngine::getInterpol check sat..." - << std::endl; - Result r = subSolver->checkSynth(); - Trace("sygus-interpol") << " SolverEngine::getInterpol result: " << r + Trace("sygus-interpol") + << " SygusInterpol::solveInterpolation check synth..." << std::endl; + Result r = d_subSolver->checkSynth(); + Trace("sygus-interpol") << " SygusInterpol::solveInterpolation result: " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - return findInterpol(subSolver.get(), interpol, itp); + return findInterpol(d_subSolver.get(), interpol, d_itp); + } + return false; +} + +bool SygusInterpol::solveInterpolationNext(Node& interpol) +{ + Trace("sygus-interpol") + << " SygusInterpol::solveInterpolationNext check synth..." << std::endl; + // invoke the check-synth with isNext = true. + Result r = d_subSolver->checkSynth(true); + Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext result: " + << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + return findInterpol(d_subSolver.get(), interpol, d_itp); } return false; } diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 4d3ae0219..604e7435f 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -84,6 +84,21 @@ class SygusInterpol : protected EnvObj const TypeNode& itpGType, Node& interpol); + /** + * Returns the sygus conjecture in interpol corresponding to the interpolation + * problem for input problem (F above) given by axioms (Fa above), and conj + * (Fc above). And solve the interpolation by sygus. Note that axioms is + * expected to be a subset of assertions in SMT-LIB. + * + * @param name the name for the interpol-to-synthesize. + * @param axioms the assertions (Fa above) + * @param conj the conjecture (Fc above) + * @param itpGType (if non-null) a sygus datatype type that encodes the + * grammar that should be used for solutions of the interpolation conjecture. + * @interpol the solution to the sygus conjecture. + */ + bool solveInterpolationNext(Node& interpol); + private: /** * Collects symbols from axioms (axioms) and conjecture (conj), which are @@ -212,6 +227,13 @@ class SygusInterpol : protected EnvObj * the sygus conjecture to synthesis for interpolation problem */ Node d_sygusConj; + /** + * The predicate for interpolation in the subsolver, which we pass to + * findInterpol above when the solving is successful. + */ + Node d_itp; + /** The subsolver to initialize */ + std::unique_ptr d_subSolver; }; } // namespace quantifiers diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5c4cdcd4a..e19ef2f7e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2476,7 +2476,9 @@ set(regress_1_tests regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy regress1/sygus/interpol1.smt2 + regress1/sygus/interpol1-push-pop.smt2 regress1/sygus/interpol3.smt2 + regress1/sygus/interpol3-next.smt2 regress1/sygus/interpol_arr1.smt2 regress1/sygus/interpol_arr2.smt2 regress1/sygus/interpol_cosa_1.smt2 diff --git a/test/regress/regress1/sygus/interpol1-push-pop.smt2 b/test/regress/regress1/sygus/interpol1-push-pop.smt2 new file mode 100644 index 000000000..5ea6d8568 --- /dev/null +++ b/test/regress/regress1/sygus/interpol1-push-pop.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols -i +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic NIA) +(declare-fun x ( ) Int) +(declare-fun y ( ) Int) +(declare-fun z ( ) Int) +(push) +(assert (= (* 2 x) y)) +(get-interpol A (distinct (+ (* 2 z) 1) y) + +; the grammar for the interpol-to-synthesize +((Start Bool) (StartInt Int)) +( +(Start Bool ((< StartInt StartInt))) +(StartInt Int +(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2)) +) +) +(pop) + +(assert (= (* 2 y) x)) +(get-interpol A (distinct (+ (* 2 z) 1) x) +; the grammar for the interpol-to-synthesize +((Start Bool) (StartInt Int)) +( +(Start Bool ((< StartInt StartInt))) +(StartInt Int +(x (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2)) +) +) diff --git a/test/regress/regress1/sygus/interpol3-next.smt2 b/test/regress/regress1/sygus/interpol3-next.smt2 new file mode 100644 index 000000000..b92a4254e --- /dev/null +++ b/test/regress/regress1/sygus/interpol3-next.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --produce-interpols=default --check-interpols -i +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(assert (> a 1)) +(get-interpol A (> a 0)) +(get-interpol-next) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 934e0da0d..bdd8201bc 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1448,6 +1448,35 @@ TEST_F(TestApiBlackSolver, getInterpolant) ASSERT_TRUE(output.getSort().isBoolean()); } +TEST_F(TestApiBlackSolver, getInterpolantNext) +{ + d_solver.setLogic("QF_LIA"); + d_solver.setOption("produce-interpols", "default"); + d_solver.setOption("incremental", "true"); + + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + Term z = d_solver.mkConst(intSort, "z"); + // Assumptions for interpolation: x + y > 0 /\ x < 0 + d_solver.assertFormula( + d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); + // Conjecture for interpolation: y + z > 0 \/ z < 0 + Term conj = + d_solver.mkTerm(OR, + d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), + d_solver.mkTerm(LT, z, zero)); + Term output; + d_solver.getInterpolant(conj, output); + Term output2; + d_solver.getInterpolantNext(output2); + + // We expect the next output to be distinct + ASSERT_TRUE(output != output2); +} + TEST_F(TestApiBlackSolver, declarePool) { Sort intSort = d_solver.getIntegerSort(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 3fb9ca50e..7313405be 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1439,6 +1439,31 @@ class SolverTest assertTrue(output.getSort().isBoolean()); } + @Test void getInterpolantNext() throws CVC5ApiException + { + d_solver.setLogic("QF_LIA"); + d_solver.setOption("produce-interpols", "default"); + d_solver.setOption("incremental", "true"); + + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + Term z = d_solver.mkConst(intSort, "z"); + + d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); + Term conj = d_solver.mkTerm( + OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero)); + Term output = d_solver.getNullTerm(); + d_solver.getInterpolant(conj, output); + Term output2 = d_solver.getNullTerm(); + d_solver.getInterpolantNext(output2); + + // We expect the next output to be distinct + assertNotEquals(output, output2); + } + @Test void getOp() throws CVC5ApiException { Sort bv32 = d_solver.mkBitVectorSort(32);