diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 15:00:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 15:00:07 -0500 |
commit | f71a719b8000e901af141a326ac12bce59a6153d (patch) | |
tree | b11379ca5139cfa9c87121c05cb883bcb453da07 /src/smt/command.cpp | |
parent | 90eddb069c3c9abf96719ac20aff45b44af86207 (diff) |
Model blocker feature (#3112)
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 115 |
1 files changed, 110 insertions, 5 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 044062f77..8baaeb1e9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1662,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 @@ -1679,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(); @@ -1870,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 */ /* -------------------------------------------------------------------------- */ |