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.
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;
*/
void pop(uint32_t nscopes = 1) const;
+ /**
+ * Get an interpolant
+ * SMT-LIB: ( get-interpol <term> )
+ * 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 <term> )
+ * 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'.
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"
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"
{
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]
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
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)
#include <string>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/datatype.h"
#include "expr/expr.h"
#include "expr/type.h"
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
// 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;
if ((options::checkModels() || options::checkSynthSol()
|| options::produceAbducts()
+ || options::produceInterpols() != options::ProduceInterpols::NONE
|| options::modelCoresMode() != options::ModelCoresMode::NONE
|| options::blockModelsMode() != options::BlockModelsMode::NONE)
&& !options::produceAssertions())
}
}
+void SmtEngine::checkInterpol(Expr interpol,
+ const std::vector<Expr>& easserts,
+ const Node& conj)
+{
+}
+
void SmtEngine::checkAbduct(Expr a)
{
Assert(a.getType().isBoolean());
}
}
+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);
// 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. */
*/
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).
* 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<Expr>& easserts,
+ const Node& conj);
+
/**
* Check that a solution to an abduction conjecture is indeed a solution.
*
void debugCheckFunctionBody(Expr formula,
const std::vector<Expr>& formals,
Expr func);
+
/**
* Get abduct internal.
*
}
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());
void testUFIteration();
void testGetInfo();
+ void testGetInterpolant();
void testGetOp();
void testGetOption();
void testGetUnsatAssumptions1();
TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&);
}
+void SolverBlack::testGetInterpolant()
+{
+ // TODO
+}
+
void SolverBlack::testGetOp()
{
Sort bv32 = d_solver->mkBitVectorSort(32);
projects / cvc5.git / commitdiff