smt/model.h
smt/model_core_builder.cpp
smt/model_core_builder.h
+ smt/model_blocker.cpp
+ smt/model_blocker.h
smt/smt_engine.cpp
smt/smt_engine.h
smt/smt_engine_scope.cpp
${CMAKE_CURRENT_BINARY_DIR}/BitVectorSize.java
${CMAKE_CURRENT_BINARY_DIR}/BitVectorType.java
${CMAKE_CURRENT_BINARY_DIR}/BitVectorZeroExtend.java
+ ${CMAKE_CURRENT_BINARY_DIR}/BlockModelCommand.java
+ ${CMAKE_CURRENT_BINARY_DIR}/BlockModelValuesCommand.java
${CMAKE_CURRENT_BINARY_DIR}/BoolHashFunction.java
${CMAKE_CURRENT_BINARY_DIR}/BooleanType.java
${CMAKE_CURRENT_BINARY_DIR}/CVC4.java
}
}
+const std::string OptionsHandler::s_blockModelsHelp =
+ "\
+Blocking models modes are currently supported by the --block-models option:\n\
+\n\
+none (default) \n\
++ do not block models\n\
+\n\
+literals\n\
++ block models based on the SAT skeleton\n\
+\n\
+values\n\
++ block models based on the concrete model values for the free variables.\n\
+\n\
+";
+
+BlockModelsMode OptionsHandler::stringToBlockModelsMode(std::string option,
+ std::string optarg)
+{
+ if (optarg == "none")
+ {
+ return BLOCK_MODELS_NONE;
+ }
+ else if (optarg == "literals")
+ {
+ return BLOCK_MODELS_LITERALS;
+ }
+ else if (optarg == "values")
+ {
+ return BLOCK_MODELS_VALUES;
+ ;
+ }
+ else if (optarg == "help")
+ {
+ puts(s_blockModelsHelp.c_str());
+ exit(1);
+ }
+ else
+ {
+ throw OptionException(std::string("unknown option for --block-models: `")
+ + optarg + "'. Try --block-models help.");
+ }
+}
+
const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
"\
Modes for sygus solution output, supported by --sygus-out:\n\
SimplificationMode stringToSimplificationMode(std::string option,
std::string optarg);
ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg);
+ BlockModelsMode stringToBlockModelsMode(std::string option,
+ std::string optarg);
SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option,
std::string optarg);
void setProduceAssertions(std::string option, bool value);
static const std::string s_qcfWhenModeHelp;
static const std::string s_simplificationHelp;
static const std::string s_modelCoresHelp;
+ static const std::string s_blockModelsHelp;
static const std::string s_sygusSolutionOutModeHelp;
static const std::string s_cbqiBvIneqModeHelp;
static const std::string s_cegqiSingleInvHelp;
MODEL_CORES_NON_IMPLIED
};
+/** Block models modes. */
+enum BlockModelsMode
+{
+ /** Do not block models */
+ BLOCK_MODELS_NONE,
+ /**
+ * block models based on literals truth values.
+ */
+ BLOCK_MODELS_LITERALS,
+ /**
+ * block models based on concrete variable values in the model.
+ */
+ BLOCK_MODELS_VALUES,
+};
+
} // namespace CVC4
#endif /* CVC4__SMT__MODES_H */
includes = ["options/smt_modes.h"]
help = "mode for producing model cores"
+
+[[option]]
+ name = "blockModelsMode"
+ category = "regular"
+ long = "block-models=MODE"
+ type = "BlockModelsMode"
+ default = "BLOCK_MODELS_NONE"
+ handler = "stringToBlockModelsMode"
+ includes = ["options/smt_modes.h"]
+ help = "mode for producing several models"
+
[[option]]
name = "proof"
smt_name = "produce-proofs"
// We currently do nothing with the type information declared for the heap.
{ cmd->reset(new EmptyCommand()); }
RPAREN_TOK
+ | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ { cmd->reset(new BlockModelCommand()); }
+
+ | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ ( LPAREN_TOK termList[terms,e] RPAREN_TOK
+ { cmd->reset(new BlockModelValuesCommand(terms)); }
+ | ~LPAREN_TOK
+ { PARSER_STATE->parseError("The block-model-value command expects a list "
+ "of terms. Perhaps you forgot a pair of "
+ "parentheses?");
+ }
+ )
;
TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
GET_MODEL_TOK : 'get-model';
+BLOCK_MODEL_TOK : 'block-model';
+BLOCK_MODEL_VALUES_TOK : 'block-model-values';
ECHO_TOK : 'echo';
REWRITE_RULE_TOK : 'assert-rewrite';
REDUCTION_RULE_TOK : 'assert-reduction';
{
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
// 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();
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 */
/* -------------------------------------------------------------------------- */
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:
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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"));
}
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)
{
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();
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
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))
"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; }
* 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
*/
std::pair<Expr, Expr> getSepHeapAndNilExpr();
+ /** get expanded assertions
+ *
+ * Returns the set of assertions, after expanding definitions.
+ */
+ std::vector<Expr> getExpandedAssertions();
+
public:
/**
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.
*/
/* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */
;
+ /**
+ * 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
regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt
regress1/lemmas/pursuit-safety-8.smt
regress1/lemmas/simple_startup_9nodes.abstract.base.smt
+ regress1/model-blocker-simple.smt2
+ regress1/model-blocker-values.smt2
regress1/nl/approx-sqrt-unsat.smt2
regress1/nl/approx-sqrt.smt2
regress1/nl/arctan2-expdef.smt2
--- /dev/null
+; COMMAND-LINE: --incremental --produce-models --block-models=literals
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () Int)
+(assert (or (= x 4) (= x 5) (= x 6) (= x 7)))
+(check-sat)
+(block-model-values (x))
+(check-sat)
+(block-model)
+(check-sat)
+(block-model-values ((+ x 1)))
+(check-sat)
+(block-model)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental --produce-models --block-models=values
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_UFLIA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun f (Int) Int)
+(assert (distinct (f a) (f b)))
+(assert (= c (f a)))
+(assert (distinct a b))
+(assert (and (>= a 0) (>= b 0) (< a 2) (< b 2)))
+(check-sat)
+(block-model)
+(check-sat)
+(block-model)
+(check-sat)
projects / cvc5.git / commitdiff