diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 13:58:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 13:58:09 -0500 |
commit | 90eddb069c3c9abf96719ac20aff45b44af86207 (patch) | |
tree | 5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c /src/smt/command.cpp | |
parent | 3aba99657b39ccc0ab400c7ed9778673a3acddd7 (diff) |
Support get-abduct smt2 command (#3122)
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index b1936d8cc..044062f77 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2033,6 +2033,90 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } +GetAbductCommand::GetAbductCommand() {} +GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj) + : d_name(name), d_conj(conj), d_resultStatus(false) +{ +} +GetAbductCommand::GetAbductCommand(const std::string& name, + Expr conj, + const Type& gtype) + : d_name(name), + d_conj(conj), + d_sygus_grammar_type(gtype), + d_resultStatus(false) +{ +} + +Expr GetAbductCommand::getConjecture() const { return d_conj; } +Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; } +Expr GetAbductCommand::getResult() const { return d_result; } + +void GetAbductCommand::invoke(SmtEngine* smtEngine) +{ + try + { + if (d_sygus_grammar_type.isNull()) + { + d_resultStatus = smtEngine->getAbduct(d_conj, d_result); + } + else + { + d_resultStatus = + smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result); + } + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetAbductCommand::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* 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; +} + +Command* GetAbductCommand::clone() const +{ + GetAbductCommand* c = new GetAbductCommand(d_name, d_conj); + c->d_sygus_grammar_type = d_sygus_grammar_type; + c->d_result = d_result; + c->d_resultStatus = d_resultStatus; + return c; +} + +std::string GetAbductCommand::getCommandName() const { return "get-abduct"; } + /* -------------------------------------------------------------------------- */ /* class GetQuantifierEliminationCommand */ /* -------------------------------------------------------------------------- */ |