diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 115 | ||||
-rw-r--r-- | src/smt/command.h | 31 | ||||
-rw-r--r-- | src/smt/model_blocker.cpp | 288 | ||||
-rw-r--r-- | src/smt/model_blocker.h | 70 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 147 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 50 |
6 files changed, 660 insertions, 41 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 */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index eb3199944..d82399135 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -958,6 +958,37 @@ class CVC4_PUBLIC GetModelCommand : public Command SmtEngine* d_smtEngine; }; /* class GetModelCommand */ +/** The command to block models. */ +class CVC4_PUBLIC BlockModelCommand : public Command +{ + public: + BlockModelCommand(); + + void invoke(SmtEngine* smtEngine) override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; +}; /* class BlockModelCommand */ + +/** The command to block model values. */ +class CVC4_PUBLIC BlockModelValuesCommand : public Command +{ + public: + BlockModelValuesCommand(const std::vector<Expr>& terms); + + const std::vector<Expr>& getTerms() const; + void invoke(SmtEngine* smtEngine) override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; + + protected: + /** The terms we are blocking */ + std::vector<Expr> d_terms; +}; /* class BlockModelValuesCommand */ + class CVC4_PUBLIC GetProofCommand : public Command { public: diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp new file mode 100644 index 000000000..cb962ee45 --- /dev/null +++ b/src/smt/model_blocker.cpp @@ -0,0 +1,288 @@ +/********************* */ +/*! \file model_blocker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of utility for blocking models. + ** + **/ + +#include "smt/model_blocker.h" + +#include "expr/node.h" +#include "expr/node_algorithm.h" +#include "theory/quantifiers/term_util.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, + theory::TheoryModel* m, + BlockModelsMode mode, + const std::vector<Expr>& exprToBlock) +{ + NodeManager* nm = NodeManager::currentNM(); + // convert to nodes + std::vector<Node> tlAsserts; + for (const Expr& a : assertions) + { + Node an = Node::fromExpr(a); + tlAsserts.push_back(an); + } + std::vector<Node> nodesToBlock; + for (const Expr& eb : exprToBlock) + { + nodesToBlock.push_back(Node::fromExpr(eb)); + } + Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl; + Node blocker; + if (mode == BLOCK_MODELS_LITERALS) + { + Assert(nodesToBlock.empty()); + // optimization: filter out top-level unit assertions, as they cannot + // contribute to model blocking. + unsigned counter = 0; + std::vector<Node> asserts; + while (counter < tlAsserts.size()) + { + Node cur = tlAsserts[counter]; + counter++; + Node catom = cur.getKind() == NOT ? cur[0] : cur; + bool cpol = cur.getKind() != NOT; + if (catom.getKind() == NOT) + { + tlAsserts.push_back(catom[0]); + } + else if (catom.getKind() == AND && cpol) + { + tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end()); + } + else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom)) + { + asserts.push_back(cur); + Trace("model-blocker") << " " << cur << std::endl; + } + } + if (asserts.empty()) + { + Node blockTriv = nm->mkConst(false); + Trace("model-blocker") + << "...model blocker is (trivially) " << blockTriv << std::endl; + return blockTriv.toExpr(); + } + + Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0]; + std::unordered_map<TNode, Node, TNodeHashFunction> visited; + std::unordered_map<TNode, Node, TNodeHashFunction> implicant; + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode cur; + visit.push_back(formula); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + Trace("model-blocker-debug") << "Visit : " << cur << std::endl; + + if (it == visited.end()) + { + visited[cur] = Node::null(); + Node catom = cur.getKind() == NOT ? cur[0] : cur; + bool cpol = cur.getKind() != NOT; + // compute the implicant + // impl is a formula that implies cur that is also satisfied by m + Node impl; + if (catom.getKind() == NOT) + { + // double negation + impl = catom[0]; + } + else if (catom.getKind() == OR || catom.getKind() == AND) + { + // if disjunctive + if ((catom.getKind() == OR) == cpol) + { + // take the first literal that is satisfied + for (Node n : catom) + { + // rewrite, this ensures that e.g. the propositional value of + // quantified formulas can be queried + n = theory::Rewriter::rewrite(n); + Node vn = Node::fromExpr(m->getValue(n.toExpr())); + Assert(vn.isConst()); + if (vn.getConst<bool>() == cpol) + { + impl = cpol ? n : n.negate(); + break; + } + } + } + else if (catom.getKind() == OR) + { + // one step NNF + std::vector<Node> children; + for (const Node& cn : catom) + { + children.push_back(cn.negate()); + } + impl = nm->mkNode(AND, children); + } + } + else if (catom.getKind() == ITE) + { + Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr())); + Assert(vcond.isConst()); + Node cond = cur[0]; + Node branch; + if (vcond.getConst<bool>()) + { + branch = cur[1]; + } + else + { + cond = cond.negate(); + branch = cur[2]; + } + impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate()); + } + else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean()) + || catom.getKind() == XOR) + { + // based on how the children evaluate in the model + std::vector<Node> children; + for (const Node& cn : catom) + { + Node vn = Node::fromExpr(m->getValue(cn.toExpr())); + Assert(vn.isConst()); + children.push_back(vn.getConst<bool>() ? cn : cn.negate()); + } + impl = nm->mkNode(AND, children); + } + else + { + // literals justified by themselves + visited[cur] = cur; + Trace("model-blocker-debug") << "...self justified" << std::endl; + } + if (visited[cur].isNull()) + { + visit.push_back(cur); + if (impl.isNull()) + { + Assert(cur.getKind() == AND); + Trace("model-blocker-debug") << "...recurse" << std::endl; + visit.insert(visit.end(), cur.begin(), cur.end()); + } + else + { + Trace("model-blocker-debug") + << "...implicant : " << impl << std::endl; + implicant[cur] = impl; + visit.push_back(impl); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + it = implicant.find(cur); + if (it != implicant.end()) + { + Node impl = it->second; + it = visited.find(impl); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + ret = it->second; + Trace("model-blocker-debug") + << "...implicant res: " << ret << std::endl; + } + else + { + bool childChanged = false; + std::vector<Node> children; + // we never recurse to parameterized nodes + Assert(cur.getMetaKind() != metakind::PARAMETERIZED); + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + Trace("model-blocker-debug") << "...recons res: " << ret << std::endl; + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(formula) != visited.end()); + Assert(!visited.find(formula)->second.isNull()); + blocker = visited[formula].negate(); + } + else + { + Assert(mode == BLOCK_MODELS_VALUES); + std::vector<Node> blockers; + // if specific terms were not specified, block all variables of + // the model + if (nodesToBlock.empty()) + { + Trace("model-blocker") + << "no specific terms to block recognized" << std::endl; + std::unordered_set<Node, NodeHashFunction> symbols; + for (Node n : tlAsserts) + { + expr::getSymbols(n, symbols); + } + for (Node s : symbols) + { + if (s.getType().getKind() != kind::FUNCTION_TYPE) + { + Node v = m->getValue(s); + Node a = nm->mkNode(DISTINCT, s, v); + blockers.push_back(a); + } + } + } + // otherwise, block all terms that were specified in get-value + else + { + std::unordered_set<Node, NodeHashFunction> terms; + for (Node n : nodesToBlock) + { + Node v = m->getValue(n); + Node a = nm->mkNode(DISTINCT, n, v); + blockers.push_back(a); + } + } + if (blockers.size() == 0) + { + blocker = nm->mkConst<bool>(true); + } + else if (blockers.size() == 1) + { + blocker = blockers[0]; + } + else + { + blocker = nm->mkNode(OR, blockers); + } + } + Trace("model-blocker") << "...model blocker is " << blocker << std::endl; + return blocker.toExpr(); +} + +} /* namespace CVC4 */ diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h new file mode 100644 index 000000000..ca201ec66 --- /dev/null +++ b/src/smt/model_blocker.h @@ -0,0 +1,70 @@ +/********************* */ +/*! \file model_blocker.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for blocking the current model + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__MODEL_BLOCKER_H +#define __CVC4__THEORY__MODEL_BLOCKER_H + +#include <vector> + +#include "expr/expr.h" +#include "options/smt_options.h" +#include "theory/theory_model.h" + +namespace CVC4 { + +/** + * A utility for blocking the current model. + */ +class ModelBlocker +{ + public: + /** get model blocker + * + * This returns a disjunction of literals ~L1 V ... V ~Ln with the following + * properties: + * (1) L1 ... Ln hold in the current model (given by argument m), + * (2) if mode is set to "literals", L1 ... Ln are literals that occur in + * assertions and propositionally entail all non-unit top-level assertions. + * (3) if mode is set to "values", L1 ... Ln are literals of the form x=c, + * where c is the value of x in the current model. + * (4) if exprToBlock is not empty, L1 ... Ln are literals of the form t=c, + * where c is the value of t in the current model. If exprToBlock is + * non-empty, then L1 ... Ln are t1=c1 ... tn=cn where exprToBlock is + * { t1 ... tn }; if exprToBlock is empty, then t1 ... tn are the free + * variables of assertions. + * + * We expect exprToBlock to be non-empty only if mode is BLOCK_MODELS_VALUES. + * + * For example, if our input is: + * x > 0 ^ ( y < 0 V z < 0 V w < 0 ) + * and m is { x -> 1, y -> 2, z -> -1, w -> -1 }, then this method may + * return ~(z < 0) or ~(w < 0) when set to mode "literals". + * + * Notice that we do not require that L1...Ln entail unit top-level assertions + * since these literals are trivially entailed to be true in all models of + * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the + * left disjunct is always false. + */ + static Expr getModelBlocker( + const std::vector<Expr>& assertions, + theory::TheoryModel* m, + BlockModelsMode mode, + const std::vector<Expr>& exprToBlock = std::vector<Expr>()); +}; /* class TheoryModelCoreBuilder */ + +} // namespace CVC4 + +#endif /* __CVC4__THEORY__MODEL_BLOCKER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5db3fc43d..560cb0599 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -85,6 +85,7 @@ #include "smt/command_list.h" #include "smt/logic_request.h" #include "smt/managed_ostreams.h" +#include "smt/model_blocker.h" #include "smt/model_core_builder.h" #include "smt/smt_engine_scope.h" #include "smt/term_formula_removal.h" @@ -1278,11 +1279,12 @@ void SmtEngine::setDefaults() { if ((options::checkModels() || options::checkSynthSol() || options::produceAbducts() - || options::modelCoresMode() != MODEL_CORES_NONE) + || options::modelCoresMode() != MODEL_CORES_NONE + || options::blockModelsMode() != BLOCK_MODELS_NONE) && !options::produceAssertions()) { Notice() << "SmtEngine: turning on produce-assertions to support " - << "check-models, check-synth-sol or produce-model-cores." << endl; + << "option requiring assertions." << endl; setOption("produce-assertions", SExpr("true")); } @@ -3055,6 +3057,34 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); } +theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const +{ + if (!options::assignFunctionValues()) + { + std::stringstream ss; + ss << "Cannot " << c << " when --assign-function-values is false."; + throw RecoverableModalException(ss.str().c_str()); + } + + if (d_status.isNull() || d_status.asSatisfiabilityResult() == Result::UNSAT + || d_problemExtended) + { + std::stringstream ss; + ss << "Cannot " << c + << " unless immediately preceded by SAT/INVALID or UNKNOWN response."; + throw RecoverableModalException(ss.str().c_str()); + } + if (!options::produceModels()) + { + std::stringstream ss; + ss << "Cannot " << c << " when produce-models options is off."; + throw ModalException(ss.str().c_str()); + } + + TheoryModel* m = d_theoryEngine->getBuiltModel(); + + return m; +} void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache) { @@ -4200,6 +4230,16 @@ Expr SmtEngine::getValue(const Expr& ex) const return resultNode.toExpr(); } +vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs) +{ + vector<Expr> result; + for (const Expr& e : exprs) + { + result.push_back(getValue(e)); + } + return result; +} + bool SmtEngine::addToAssignment(const Expr& ex) { SmtScope smts(this); finalOptionsAreSet(); @@ -4337,27 +4377,7 @@ Model* SmtEngine::getModel() { Dump("benchmark") << GetModelCommand(); } - if (!options::assignFunctionValues()) - { - const char* msg = - "Cannot get the model when --assign-function-values is false."; - throw RecoverableModalException(msg); - } - - if(d_status.isNull() || - d_status.asSatisfiabilityResult() == Result::UNSAT || - d_problemExtended) { - const char* msg = - "Cannot get the current model unless immediately " - "preceded by SAT/INVALID or UNKNOWN response."; - throw RecoverableModalException(msg); - } - if(!options::produceModels()) { - const char* msg = - "Cannot get model when produce-models options is off."; - throw ModalException(msg); - } - TheoryModel* m = d_theoryEngine->getBuiltModel(); + TheoryModel* m = getAvailableModel("get model"); // Since model m is being returned to the user, we must ensure that this // model object remains valid with future check-sat calls. Hence, we set @@ -4367,23 +4387,67 @@ Model* SmtEngine::getModel() { if (options::modelCoresMode() != MODEL_CORES_NONE) { // If we enabled model cores, we compute a model core for m based on our - // assertions using the model core builder utility - std::vector<Expr> easserts = getAssertions(); - // must expand definitions - std::vector<Expr> eassertsProc; - std::unordered_map<Node, Node, NodeHashFunction> cache; - for (unsigned i = 0, nasserts = easserts.size(); i < nasserts; i++) - { - Node ea = Node::fromExpr(easserts[i]); - Node eae = d_private->expandDefinitions(ea, cache); - eassertsProc.push_back(eae.toExpr()); - } + // (expanded) assertions using the model core builder utility + std::vector<Expr> eassertsProc = getExpandedAssertions(); ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode()); } m->d_inputName = d_filename; return m; } +Result SmtEngine::blockModel() +{ + Trace("smt") << "SMT blockModel()" << endl; + SmtScope smts(this); + + finalOptionsAreSet(); + + if (Dump.isOn("benchmark")) + { + Dump("benchmark") << BlockModelCommand(); + } + + TheoryModel* m = getAvailableModel("block model"); + + if (options::blockModelsMode() == BLOCK_MODELS_NONE) + { + std::stringstream ss; + ss << "Cannot block model when block-models is set to none."; + throw ModalException(ss.str().c_str()); + } + + // get expanded assertions + std::vector<Expr> eassertsProc = getExpandedAssertions(); + Expr eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m, options::blockModelsMode()); + return assertFormula(eblocker); +} + +Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs) +{ + Trace("smt") << "SMT blockModelValues()" << endl; + SmtScope smts(this); + + finalOptionsAreSet(); + + PrettyCheckArgument( + !exprs.empty(), + "block model values must be called on non-empty set of terms"); + if (Dump.isOn("benchmark")) + { + Dump("benchmark") << BlockModelValuesCommand(exprs); + } + + TheoryModel* m = getAvailableModel("block model values"); + + // get expanded assertions + std::vector<Expr> eassertsProc = getExpandedAssertions(); + // we always do block model values mode here + Expr eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m, BLOCK_MODELS_VALUES, exprs); + return assertFormula(eblocker); +} + std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) { if (!d_logic.isTheoryEnabled(THEORY_SEP)) @@ -4406,6 +4470,21 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) "expressions from theory model."); } +std::vector<Expr> SmtEngine::getExpandedAssertions() +{ + std::vector<Expr> easserts = getAssertions(); + // must expand definitions + std::vector<Expr> eassertsProc; + std::unordered_map<Node, Node, NodeHashFunction> cache; + for (const Expr& e : easserts) + { + Node ea = Node::fromExpr(e); + Node eae = d_private->expandDefinitions(ea, cache); + eassertsProc.push_back(eae.toExpr()); + } + return eassertsProc; +} + Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 566777a89..316ca16d1 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -402,6 +402,16 @@ class CVC4_PUBLIC SmtEngine { * that). */ Result quickCheck(); + /** get the model, if it is available and return a pointer to it + * + * This ensures that the model is currently available, which means that + * CVC4 is producing models, and is in "SAT mode", otherwise an exception + * is thrown. + * + * The flag c is used for giving an error message to indicate the context + * this method was called. + */ + theory::TheoryModel* getAvailableModel(const char* c) const; /** * Fully type-check the argument, and also type-check that it's @@ -480,6 +490,12 @@ class CVC4_PUBLIC SmtEngine { */ std::pair<Expr, Expr> getSepHeapAndNilExpr(); + /** get expanded assertions + * + * Returns the set of assertions, after expanding definitions. + */ + std::vector<Expr> getExpandedAssertions(); + public: /** @@ -553,12 +569,37 @@ class CVC4_PUBLIC SmtEngine { std::string getFilename() const; /** * Get the model (only if immediately preceded by a SAT - * or INVALID query). Only permitted if CVC4 was built with model - * support and produce-models is on. + * or INVALID query). Only permitted if produce-models is on. */ Model* getModel(); /** + * Block the current model. Can be called only if immediately preceded by + * a SAT or INVALID query. Only permitted if produce-models is on, and the + * block-models option is set to a mode other than "none". + * + * This adds an assertion to the assertion stack that blocks the current + * model based on the current options configured by CVC4. + * + * The return value has the same meaning as that of assertFormula. + */ + Result blockModel(); + + /** + * Block the current model values of (at least) the values in exprs. + * Can be called only if immediately preceded by a SAT or INVALID query. Only + * permitted if produce-models is on, and the block-models option is set to a + * mode other than "none". + * + * This adds an assertion to the assertion stack of the form: + * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn))) + * where M0 ... Mn are the current model values of exprs[0] ... exprs[n]. + * + * The return value has the same meaning as that of assertFormula. + */ + Result blockModelValues(const std::vector<Expr>& exprs); + + /** * When using separation logic, obtain the expression for the heap. */ Expr getSepHeapExpr(); @@ -775,6 +816,11 @@ class CVC4_PUBLIC SmtEngine { ; /** + * Same as getValue but for a vector of expressions + */ + std::vector<Expr> getValues(const std::vector<Expr>& exprs); + + /** * Add a function to the set of expressions whose value is to be * later returned by a call to getAssignment(). The expression * should be a Boolean zero-ary defined function or a Boolean |