diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 140 |
1 files changed, 79 insertions, 61 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 2e36190b4..97a51277b 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -90,7 +90,6 @@ ostream& operator<<(ostream& out, const CommandStatus* s) return out; } - /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) { @@ -137,7 +136,7 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} -Command::Command(api::Solver* solver) +Command::Command(const api::Solver* solver) : d_solver(solver), d_commandStatus(nullptr), d_muted(false) { } @@ -652,40 +651,49 @@ std::string DeclareSygusFunctionCommand::getCommandName() const } /* -------------------------------------------------------------------------- */ -/* class SynthFunCommand */ +/* class SynthFunCommand */ /* -------------------------------------------------------------------------- */ -SynthFunCommand::SynthFunCommand(const std::string& id, - Expr func, - Type sygusType, +SynthFunCommand::SynthFunCommand(const api::Solver* solver, + const std::string& id, + api::Term fun, + const std::vector<api::Term>& vars, + api::Sort sort, bool isInv, - const std::vector<Expr>& vars) + api::Grammar* g) : DeclarationDefinitionCommand(id), - d_func(func), - d_sygusType(sygusType), + d_fun(fun), + d_vars(vars), + d_sort(sort), d_isInv(isInv), - d_vars(vars) + d_grammar(g) { + d_solver = solver; } -SynthFunCommand::SynthFunCommand(const std::string& id, - Expr func, - Type sygusType, - bool isInv) - : SynthFunCommand(id, func, sygusType, isInv, {}) +api::Term SynthFunCommand::getFunction() const { return d_fun; } + +const std::vector<api::Term>& SynthFunCommand::getVars() const { + return d_vars; } -Expr SynthFunCommand::getFunction() const { return d_func; } -const std::vector<Expr>& SynthFunCommand::getVars() const { return d_vars; } -Type SynthFunCommand::getSygusType() const { return d_sygusType; } +api::Sort SynthFunCommand::getSort() const { return d_sort; } bool SynthFunCommand::isInv() const { return d_isInv; } +const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } + void SynthFunCommand::invoke(SmtEngine* smtEngine) { try { - smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars); + smtEngine->declareSynthFun(d_symbol, + d_fun.getExpr(), + d_grammar == nullptr + ? d_sort.getType() + : d_grammar->resolve().getType(), + d_isInv, + api::termVectorToExprs(d_vars)); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -697,15 +705,13 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine) Command* SynthFunCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SynthFunCommand(d_symbol, - d_func.exportTo(exprManager, variableMap), - d_sygusType.exportTo(exprManager, variableMap), - d_isInv); + Unimplemented(); } Command* SynthFunCommand::clone() const { - return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars); + return new SynthFunCommand( + d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar); } std::string SynthFunCommand::getCommandName() const @@ -1352,7 +1358,7 @@ Command* DefineNamedFunctionCommand::clone() const /* -------------------------------------------------------------------------- */ DefineFunctionRecCommand::DefineFunctionRecCommand( - api::Solver* solver, + const api::Solver* solver, api::Term func, const std::vector<api::Term>& formals, api::Term formula, @@ -1365,7 +1371,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( } DefineFunctionRecCommand::DefineFunctionRecCommand( - api::Solver* solver, + const api::Solver* solver, const std::vector<api::Term>& funcs, const std::vector<std::vector<api::Term>>& formals, const std::vector<api::Term>& formulas, @@ -2094,40 +2100,49 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } -GetInterpolCommand::GetInterpolCommand(api::Solver* solver, +/* -------------------------------------------------------------------------- */ +/* class GetInterpolCommand */ +/* -------------------------------------------------------------------------- */ + +GetInterpolCommand::GetInterpolCommand(const 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, +GetInterpolCommand::GetInterpolCommand(const api::Solver* solver, const std::string& name, api::Term conj, - const Type& gtype) + api::Grammar* g) : Command(solver), d_name(name), d_conj(conj), - d_sygus_grammar_type(gtype), + d_sygus_grammar(g), d_resultStatus(false) { } api::Term GetInterpolCommand::getConjecture() const { return d_conj; } -Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; } + +const api::Grammar* GetInterpolCommand::getGrammar() const +{ + return d_sygus_grammar; +} + api::Term GetInterpolCommand::getResult() const { return d_result; } void GetInterpolCommand::invoke(SmtEngine* smtEngine) { try { - if (d_sygus_grammar_type.isNull()) + if (!d_sygus_grammar) { d_resultStatus = d_solver->getInterpolant(d_conj, d_result); } else { d_resultStatus = - d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result); + d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result); } d_commandStatus = CommandSuccess::instance(); } @@ -2167,7 +2182,8 @@ Command* GetInterpolCommand::exportTo(ExprManager* exprManager, Command* GetInterpolCommand::clone() const { - GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj); + GetInterpolCommand* c = + new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar); c->d_result = d_result; c->d_resultStatus = d_resultStatus; return c; @@ -2178,42 +2194,50 @@ 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) +/* -------------------------------------------------------------------------- */ +/* class GetAbductCommand */ +/* -------------------------------------------------------------------------- */ + +GetAbductCommand::GetAbductCommand(const api::Solver* solver, + const std::string& name, + api::Term conj) + : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) { } -GetAbductCommand::GetAbductCommand(const std::string& name, - Expr conj, - const Type& gtype) - : d_name(name), +GetAbductCommand::GetAbductCommand(const api::Solver* solver, + const std::string& name, + api::Term conj, + api::Grammar* g) + : Command(solver), + d_name(name), d_conj(conj), - d_sygus_grammar_type(gtype), + d_sygus_grammar(g), d_resultStatus(false) { } -Expr GetAbductCommand::getConjecture() const { return d_conj; } -Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; } +api::Term GetAbductCommand::getConjecture() const { return d_conj; } + +const api::Grammar* GetAbductCommand::getGrammar() const +{ + return d_sygus_grammar; +} + std::string GetAbductCommand::getAbductName() const { return d_name; } -Expr GetAbductCommand::getResult() const { return d_result; } +api::Term GetAbductCommand::getResult() const { return d_result; } void GetAbductCommand::invoke(SmtEngine* smtEngine) { try { - Node conjNode = Node::fromExpr(d_conj); - Node resn; - if (d_sygus_grammar_type.isNull()) + if (!d_sygus_grammar) { - d_resultStatus = smtEngine->getAbduct(conjNode, resn); + d_resultStatus = d_solver->getAbduct(d_conj, d_result); } else { - TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type); - d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn); + d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result); } - d_result = resn.toExpr(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2246,19 +2270,13 @@ void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const Command* GetAbductCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAbductCommand* c = - new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap)); - c->d_sygus_grammar_type = - d_sygus_grammar_type.exportTo(exprManager, variableMap); - c->d_result = d_result.exportTo(exprManager, variableMap); - c->d_resultStatus = d_resultStatus; - return c; + Unimplemented(); } Command* GetAbductCommand::clone() const { - GetAbductCommand* c = new GetAbductCommand(d_name, d_conj); - c->d_sygus_grammar_type = d_sygus_grammar_type; + GetAbductCommand* c = + new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar); c->d_result = d_result; c->d_resultStatus = d_resultStatus; return c; |