diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/bindings/java/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 43 | ||||
| -rw-r--r-- | src/options/options_handler.h | 3 | ||||
| -rw-r--r-- | src/options/smt_modes.h | 15 | ||||
| -rw-r--r-- | src/options/smt_options.toml | 11 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 14 | ||||
| -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 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/model-blocker-simple.smt2 | 18 | ||||
| -rw-r--r-- | test/regress/regress1/model-blocker-values.smt2 | 18 |
16 files changed, 788 insertions, 41 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 861841633..028a5ab21 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -238,6 +238,8 @@ libcvc4_add_sources( 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 diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 555ab2d6f..3d1e0463b 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -37,6 +37,8 @@ set(gen_java_files ${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 diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b7684c556..43602c0a1 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1757,6 +1757,49 @@ ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option, } } +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\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 7ae461fd8..59503552c 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -183,6 +183,8 @@ public: 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); @@ -258,6 +260,7 @@ public: 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; diff --git a/src/options/smt_modes.h b/src/options/smt_modes.h index ed40a28a1..d719dc243 100644 --- a/src/options/smt_modes.h +++ b/src/options/smt_modes.h @@ -53,6 +53,21 @@ enum ModelCoresMode 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 */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index ef4e19654..733819780 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -98,6 +98,17 @@ header = "options/smt_options.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" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a95689f1c..663594ce8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1546,6 +1546,18 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] // 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?"); + } + ) ; @@ -3052,6 +3064,8 @@ PAR_TOK : { PARSER_STATE->v2_6() }?'par'; 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'; 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 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5ecacd4ab..9874100b3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1194,6 +1194,8 @@ set(regress_1_tests 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 diff --git a/test/regress/regress1/model-blocker-simple.smt2 b/test/regress/regress1/model-blocker-simple.smt2 new file mode 100644 index 000000000..526b51007 --- /dev/null +++ b/test/regress/regress1/model-blocker-simple.smt2 @@ -0,0 +1,18 @@ +; 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) diff --git a/test/regress/regress1/model-blocker-values.smt2 b/test/regress/regress1/model-blocker-values.smt2 new file mode 100644 index 000000000..65db79ca4 --- /dev/null +++ b/test/regress/regress1/model-blocker-values.smt2 @@ -0,0 +1,18 @@ +; 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) |