From 724d8cf23ae74158b36b408643298c49c3b20833 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 30 Jun 2020 04:50:40 -0700 Subject: [PATCH] Interpolation step 1 (#4638) This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack. The first step creates the API framework, while omits the implementation for getting interpolation. --- src/api/cvc4cpp.cpp | 25 +++++++ src/api/cvc4cpp.h | 23 +++++++ src/options/smt_options.toml | 37 +++++++++++ src/parser/smt2/Smt2.g | 12 ++++ src/smt/command.cpp | 84 ++++++++++++++++++++++++ src/smt/command.h | 53 +++++++++++++++ src/smt/set_defaults.cpp | 7 +- src/smt/smt_engine.cpp | 19 ++++++ src/smt/smt_engine.h | 34 +++++++++- src/theory/datatypes/sygus_extension.cpp | 1 - test/unit/api/solver_black.h | 6 ++ 11 files changed, 297 insertions(+), 4 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 0c8de5291..1e14e9b3a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4744,6 +4744,31 @@ void Solver::pop(uint32_t nscopes) const CVC4_API_SOLVER_TRY_CATCH_END; } +bool Solver::getInterpolant(Term conj, Term& output) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Expr result; + bool success = d_smtEngine->getInterpol(*conj.d_expr, result); + if (success) { + output = Term(output.d_solver, result); + } + return success; + CVC4_API_SOLVER_TRY_CATCH_END; +} + +bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Expr result; + bool success = d_smtEngine->getInterpol(*conj.d_expr, gtype, result); + if (success) + { + output = Term(output.d_solver, result); + } + return success; + CVC4_API_SOLVER_TRY_CATCH_END; +} + void Solver::printModel(std::ostream& out) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 828dc6f65..76306d443 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3022,6 +3022,29 @@ class CVC4_PUBLIC Solver */ void pop(uint32_t nscopes = 1) const; + /** + * Get an interpolant + * SMT-LIB: ( get-interpol ) + * Requires to enable option 'produce-interpols'. + * @param conj the conjecture term + * @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. + * @return true if it gets I successfully, false otherwise. + */ + bool getInterpolant(Term conj, Term& output) const; + + /** + * Get an interpolant + * SMT-LIB: ( get-interpol ) + * Requires to enable option 'produce-interpols'. + * @param conj the conjecture term + * @param gtype the grammar for the interpolant I + * @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. + * @return true if it gets I successfully, false otherwise. + */ + bool getInterpolant(Term conj, const Type& gtype, Term& output) const; + /** * Print the model of a satisfiable query to the given output stream. * Requires to enable option 'produce-models'. diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 303448d1b..c104cb3e7 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -668,6 +668,34 @@ header = "options/smt_options.h" read_only = true help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" +[[option]] + name = "produceInterpols" + category = "undocumented" + long = "produce-interpols=MODE" + type = "ProduceInterpols" + default = "NONE" + read_only = true + help = "support the get-interpol command" + help_mode = "Interpolants grammar mode" +[[option.mode.NONE]] + name = "none" + help = "don't compute interpolants" +[[option.mode.DEFAULT]] + name = "default" + help = "use the default grammar for the theory or the user-defined grammar if given" +[[option.mode.ASSUMPTIONS]] + name = "assumptions" + help = "use only operators that occur in the assumptions" +[[option.mode.CONJECTURE]] + name = "conjecture" + help = "use only operators that occur in the conjecture" +[[option.mode.SHARED]] + name = "shared" + help = "use only operators that occur both in the assumptions and the conjecture" +[[option.mode.ALL]] + name = "all" + help = "use only operators that occur either in the assumptions or the conjecture" + [[option]] name = "produceAbducts" category = "undocumented" @@ -677,6 +705,15 @@ header = "options/smt_options.h" read_only = true help = "support the get-abduct command" +[[option]] + name = "checkInterpols" + category = "regular" + long = "check-interpols" + type = "bool" + default = "false" + read_only = true + help = "checks whether produced solutions to get-interpol are correct" + [[option]] name = "checkAbducts" category = "regular" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3e8234a86..703696cf5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1136,6 +1136,17 @@ extendedCommand[std::unique_ptr* cmd] { cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType())); } + | GET_INTERPOL_TOK { + PARSER_STATE->checkThatLogicIsSet(); + } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + term[e,e2] + ( + sygusGrammar[t, terms, name] + )? + { + cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType())); + } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] @@ -2315,6 +2326,7 @@ INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; +GET_INTERPOL_TOK : 'get-interpol'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands diff --git a/src/smt/command.cpp b/src/smt/command.cpp index cbb2076dd..095c59374 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2091,6 +2091,90 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } +GetInterpolCommand::GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj) + : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) +{ +} +GetInterpolCommand::GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj, + const Type& gtype) + : Command(solver), + d_name(name), + d_conj(conj), + d_sygus_grammar_type(gtype), + d_resultStatus(false) +{ +} + +api::Term GetInterpolCommand::getConjecture() const { return d_conj; } +Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; } +api::Term GetInterpolCommand::getResult() const { return d_result; } + +void GetInterpolCommand::invoke(SmtEngine* smtEngine) +{ + try + { + if (d_sygus_grammar_type.isNull()) + { + d_resultStatus = d_solver->getInterpolant(d_conj, d_result); + } + else + { + d_resultStatus = + d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result); + } + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetInterpolCommand::printResult(std::ostream& out, + uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + expr::ExprDag::Scope scope(out, false); + if (d_resultStatus) + { + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; + } + else + { + out << "none" << std::endl; + } + } +} + +Command* GetInterpolCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) +{ + Unimplemented(); +} + +Command* GetInterpolCommand::clone() const +{ + GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj); + c->d_result = d_result; + c->d_resultStatus = d_resultStatus; + return c; +} + +std::string GetInterpolCommand::getCommandName() const +{ + return "get-interpol"; +} + GetAbductCommand::GetAbductCommand() {} GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj) : d_name(name), d_conj(conj), d_resultStatus(false) diff --git a/src/smt/command.h b/src/smt/command.h index efb4f2f4a..a6a0faaae 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -28,6 +28,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/datatype.h" #include "expr/expr.h" #include "expr/type.h" @@ -1038,6 +1039,58 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command SmtEngine* d_smtEngine; }; /* class GetSynthSolutionCommand */ +/** The command (get-interpol s B) + * + * This command asks for an interpolant from the current set of assertions and + * conjecture (goal) B. + * + * The symbol s is the name for the interpolation predicate. If we successfully + * find a predicate P, then the output response of this command is: (define-fun + * s () Bool P) + */ +class CVC4_PUBLIC GetInterpolCommand : public Command +{ + public: + GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj); + /** The argument gtype is the grammar of the interpolation query */ + GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj, + const Type& gtype); + + /** Get the conjecture of the interpolation query */ + api::Term getConjecture() const; + /** Get the grammar sygus datatype type given for the interpolation query */ + Type getGrammarType() const; + /** Get the result of the query, which is the solution to the interpolation + * query. */ + api::Term getResult() const; + + void invoke(SmtEngine* smtEngine) override; + void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; + + protected: + /** The name of the interpolation predicate */ + std::string d_name; + /** The conjecture of the interpolation query */ + api::Term d_conj; + /** + * The (optional) grammar of the interpolation query, expressed as a sygus + * datatype type. + */ + Type d_sygus_grammar_type; + /** the return status of the command */ + bool d_resultStatus; + /** the return expression of the command */ + api::Term d_result; +}; /* class GetInterpolCommand */ + /** The command (get-abduct s B (G)?) * * This command asks for an abduct from the current set of assertions and diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d663352f7..a7e8e6212 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -291,8 +291,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) // sygus inference may require datatypes if (!smte.isInternalSubsolver()) { - if (options::produceAbducts() || options::sygusInference() - || options::sygusRewSynthInput() || options::sygusInst()) + if (options::produceAbducts() + || options::produceInterpols() != options::ProduceInterpols::NONE + || options::sygusInference() || options::sygusRewSynthInput() + || options::sygusInst()) { // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; @@ -316,6 +318,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) if ((options::checkModels() || options::checkSynthSol() || options::produceAbducts() + || options::produceInterpols() != options::ProduceInterpols::NONE || options::modelCoresMode() != options::ModelCoresMode::NONE || options::blockModelsMode() != options::BlockModelsMode::NONE) && !options::produceAssertions()) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a6d89aaf5..bb4d82fe0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2934,6 +2934,12 @@ void SmtEngine::checkSynthSolution() } } +void SmtEngine::checkInterpol(Expr interpol, + const std::vector& easserts, + const Node& conj) +{ +} + void SmtEngine::checkAbduct(Expr a) { Assert(a.getType().isBoolean()); @@ -3152,6 +3158,19 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +bool SmtEngine::getInterpol(const Expr& conj, + const Type& grammarType, + Expr& interpol) +{ + return false; +} + +bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol) +{ + Type grammarType; + return getInterpol(conj, grammarType, interpol); +} + bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) { SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8a9a60251..afb39b41b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -166,7 +166,9 @@ class CVC4_PUBLIC SmtEngine // immediately after a check-sat returning "unsat" SMT_MODE_UNSAT, // immediately after a successful call to get-abduct - SMT_MODE_ABDUCT + SMT_MODE_ABDUCT, + // immediately after a successful call to get-interpol + SMT_MODE_INTERPOL }; /** Construct an SmtEngine with the given expression manager. */ @@ -618,6 +620,23 @@ class CVC4_PUBLIC SmtEngine */ Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true); + /** + * This method asks this SMT engine to find an interpolant with respect to + * the current assertion stack (call it A) and the conjecture (call it B). If + * this method returns true, then interpolant is set to a formula I such that + * A ^ ~I and I ^ ~B are both unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shapes of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getInterpol(const Expr& conj, const Type& grammarType, Expr& interpol); + + /** Same as above, but without user-provided grammar restrictions */ + bool getInterpol(const Expr& conj, Expr& interpol); + /** * This method asks this SMT engine to find an abduct with respect to the * current assertion stack (call it A) and the conjecture (call it B). @@ -935,6 +954,18 @@ class CVC4_PUBLIC SmtEngine * unsatisfiable. If not, then the found solutions are wrong. */ void checkSynthSolution(); + + /** + * Check that a solution to an interpolation problem is indeed a solution. + * + * The check is made by determining that the assertions imply the solution of + * the interpolation problem (interpol), and the solution implies the goal + * (conj). If these criteria are not met, an internal error is thrown. + */ + void checkInterpol(Expr interpol, + const std::vector& easserts, + const Node& conj); + /** * Check that a solution to an abduction conjecture is indeed a solution. * @@ -1058,6 +1089,7 @@ class CVC4_PUBLIC SmtEngine void debugCheckFunctionBody(Expr formula, const std::vector& formals, Expr func); + /** * Get abduct internal. * diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 49c7461e6..fda08bb0e 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1673,7 +1673,6 @@ bool SygusExtension::checkValue(Node n, } TypeNode tn = n.getType(); const DType& dt = tn.getDType(); - Assert(dt.isSygus()); // ensure that the expected size bound is met int cindex = utils::indexOf(vn.getOperator()); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index f080f5348..ddff63352 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -95,6 +95,7 @@ class SolverBlack : public CxxTest::TestSuite void testUFIteration(); void testGetInfo(); + void testGetInterpolant(); void testGetOp(); void testGetOption(); void testGetUnsatAssumptions1(); @@ -1309,6 +1310,11 @@ void SolverBlack::testGetInfo() TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&); } +void SolverBlack::testGetInterpolant() +{ + // TODO +} + void SolverBlack::testGetOp() { Sort bv32 = d_solver->mkBitVectorSort(32); -- 2.30.2