diff options
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 211 |
1 files changed, 196 insertions, 15 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ecd3c6f16..8baaeb1e9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1358,8 +1358,7 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) this->DefineFunctionCommand::invoke(smtEngine); if (!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment( - d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + smtEngine->addToAssignment(d_func); } d_commandStatus = CommandSuccess::instance(); } @@ -1663,16 +1662,18 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) { try { - vector<Expr> result; ExprManager* em = smtEngine->getExprManager(); NodeManager* nm = NodeManager::fromExprManager(em); - for (const Expr& e : d_terms) + smt::SmtScope scope(smtEngine); + vector<Expr> result = smtEngine->getValues(d_terms); + Assert(result.size() == d_terms.size()); + for (int i = 0, size = d_terms.size(); i < size; i++) { + Expr e = d_terms[i]; Assert(nm == NodeManager::fromExprManager(e.getExprManager())); - smt::SmtScope scope(smtEngine); Node request = Node::fromExpr( options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e); - Node value = Node::fromExpr(smtEngine->getValue(e)); + Node value = Node::fromExpr(result[i]); if (value.getType().isInteger() && request.getType() == nm->realType()) { // Need to wrap in division-by-one so that output printers know this @@ -1680,7 +1681,7 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) // a rational. Necessary for SMT-LIB standards compliance. value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1))); } - result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); + result[i] = nm->mkNode(kind::SEXPR, request, value).toExpr(); } d_result = em->mkExpr(kind::SEXPR, result); d_commandStatus = CommandSuccess::instance(); @@ -1751,14 +1752,7 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) for (const auto& p : assignments) { vector<SExpr> v; - if (p.first.getKind() == kind::APPLY) - { - v.emplace_back(SExpr::Keyword(p.first.getOperator().toString())); - } - else - { - v.emplace_back(SExpr::Keyword(p.first.toString())); - } + v.emplace_back(SExpr::Keyword(p.first.toString())); v.emplace_back(SExpr::Keyword(p.second.toString())); sexprs.emplace_back(v); } @@ -1878,6 +1872,109 @@ Command* GetModelCommand::clone() const std::string GetModelCommand::getCommandName() const { return "get-model"; } /* -------------------------------------------------------------------------- */ +/* class BlockModelCommand */ +/* -------------------------------------------------------------------------- */ + +BlockModelCommand::BlockModelCommand() {} +void BlockModelCommand::invoke(SmtEngine* smtEngine) +{ + try + { + smtEngine->blockModel(); + d_commandStatus = CommandSuccess::instance(); + } + catch (RecoverableModalException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.what()); + } + catch (UnsafeInterruptException& e) + { + d_commandStatus = new CommandInterrupted(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* BlockModelCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) +{ + BlockModelCommand* c = new BlockModelCommand(); + return c; +} + +Command* BlockModelCommand::clone() const +{ + BlockModelCommand* c = new BlockModelCommand(); + return c; +} + +std::string BlockModelCommand::getCommandName() const { return "block-model"; } + +/* -------------------------------------------------------------------------- */ +/* class BlockModelValuesCommand */ +/* -------------------------------------------------------------------------- */ + +BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms) + : d_terms(terms) +{ + PrettyCheckArgument(terms.size() >= 1, + terms, + "cannot block-model-values of an empty set of terms"); +} + +const std::vector<Expr>& BlockModelValuesCommand::getTerms() const +{ + return d_terms; +} +void BlockModelValuesCommand::invoke(SmtEngine* smtEngine) +{ + try + { + smtEngine->blockModelValues(d_terms); + d_commandStatus = CommandSuccess::instance(); + } + catch (RecoverableModalException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.what()); + } + catch (UnsafeInterruptException& e) + { + d_commandStatus = new CommandInterrupted(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* BlockModelValuesCommand::exportTo( + ExprManager* exprManager, ExprManagerMapCollection& variableMap) +{ + vector<Expr> exportedTerms; + for (std::vector<Expr>::const_iterator i = d_terms.begin(); + i != d_terms.end(); + ++i) + { + exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); + } + BlockModelValuesCommand* c = new BlockModelValuesCommand(exportedTerms); + return c; +} + +Command* BlockModelValuesCommand::clone() const +{ + BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms); + return c; +} + +std::string BlockModelValuesCommand::getCommandName() const +{ + return "block-model-values"; +} + +/* -------------------------------------------------------------------------- */ /* class GetProofCommand */ /* -------------------------------------------------------------------------- */ @@ -2041,6 +2138,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 */ /* -------------------------------------------------------------------------- */ |