diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-06-30 04:50:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-30 08:50:40 -0300 |
commit | 724d8cf23ae74158b36b408643298c49c3b20833 (patch) | |
tree | 737db246271ec879aaae7e62e49b858faf473e35 /src/smt/command.cpp | |
parent | 6303c25fc375f33b27398f9b8c4b70901785a5f1 (diff) |
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.
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 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) |