From: Andrew Reynolds Date: Tue, 11 Sep 2018 18:08:00 +0000 (-0500) Subject: Support model cores via option --produce-model-cores. (#2407) X-Git-Tag: cvc5-1.0.0~4660 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=64c48c4d3b4c26b0ba28ab1ab11ef2314ca0cbee;p=cvc5.git Support model cores via option --produce-model-cores. (#2407) This adds support for model cores, fixes #1233. It includes some minor cleanup and additions to utility functions. --- diff --git a/src/Makefile.am b/src/Makefile.am index e11a1374d..5f6d7e9ad 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -205,6 +205,8 @@ libcvc4_la_SOURCES = \ smt/managed_ostreams.h \ smt/model.cpp \ smt/model.h \ + smt/model_core_builder.cpp \ + smt/model_core_builder.h \ smt/smt_engine.cpp \ smt/smt_engine.h \ smt/smt_engine_check_proof.cpp \ @@ -239,6 +241,8 @@ libcvc4_la_SOURCES = \ theory/sort_inference.h \ theory/substitutions.cpp \ theory/substitutions.h \ + theory/subs_minimize.cpp \ + theory/subs_minimize.h \ theory/term_registration_visitor.cpp \ theory/term_registration_visitor.h \ theory/theory.cpp \ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 36ada5a95..93e892943 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -99,13 +99,13 @@ header = "options/smt_options.h" help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] - name = "omitDontCares" + name = "produceModelCores" category = "regular" - long = "omit-dont-cares" + long = "produce-model-cores" type = "bool" default = "false" read_only = true - help = "When producing a model, omit variables whose value does not matter" + help = "when printing models, compute a minimal core of relevant definitions" [[option]] name = "proof" diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 439649725..e834238a5 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -88,7 +88,8 @@ void Printer::toStream(std::ostream& out, const Model& m) const for(size_t i = 0; i < m.getNumCommands(); ++i) { const Command* cmd = m.getCommand(i); const DeclareFunctionCommand* dfc = dynamic_cast(cmd); - if (dfc != NULL && m.isDontCare(dfc->getFunction())) { + if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction())) + { continue; } toStream(out, m, cmd); diff --git a/src/smt/model.h b/src/smt/model.h index 927a055fd..3ad35fa5f 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -38,14 +38,14 @@ class Model { /** the input name (file name, etc.) this model is associated to */ std::string d_inputName; -protected: + protected: /** The SmtEngine we're associated with */ SmtEngine& d_smt; /** construct the base class; users cannot do this, only CVC4 internals */ Model(); -public: + public: /** virtual destructor */ virtual ~Model() { } /** get number of commands to report */ @@ -58,9 +58,28 @@ public: const SmtEngine* getSmtEngine() const { return &d_smt; } /** get the input name (file name, etc.) this model is associated to */ std::string getInputName() const { return d_inputName; } -public: - /** Check whether this expr is a don't-care in the model */ - virtual bool isDontCare(Expr expr) const { return false; } + //--------------------------- model cores + /** set using model core + * + * This sets that this model is minimized to be a "model core" for some + * formula (typically the input formula). + * + * For example, given formula ( a>5 OR b>5 ) AND f( c ) = 0, + * a model for this formula is: a -> 6, b -> 0, c -> 0, f -> lambda x. 0. + * A "model core" is a subset of this model that suffices to show the + * above formula is true, for example { a -> 6, f -> lambda x. 0 } is a + * model core for this formula. + */ + virtual void setUsingModelCore() = 0; + /** record model core symbol + * + * This marks that sym is a "model core symbol". In other words, its value is + * critical to the satisfiability of the formula this model is for. + */ + virtual void recordModelCoreSymbol(Expr sym) = 0; + /** Check whether this expr is in the model core */ + virtual bool isModelCoreSymbol(Expr expr) const = 0; + //--------------------------- end model cores /** get value for expression */ virtual Expr getValue(Expr expr) const = 0; /** get cardinality for sort */ diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp new file mode 100644 index 000000000..dbc6c5c9e --- /dev/null +++ b/src/smt/model_core_builder.cpp @@ -0,0 +1,97 @@ +/********************* */ +/*! \file model_core_builder.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 building model cores + **/ + +#include "smt/model_core_builder.h" + +#include "theory/subs_minimize.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +bool ModelCoreBuilder::setModelCore(const std::vector& assertions, + Model* m) +{ + if (Trace.isOn("model-core")) + { + Trace("model-core") << "Compute model core, assertions:" << std::endl; + for (const Node& a : assertions) + { + Trace("model-core") << " " << a << std::endl; + } + } + + // convert to nodes + std::vector asserts; + for (unsigned i = 0, size = assertions.size(); i < size; i++) + { + asserts.push_back(Node::fromExpr(assertions[i])); + } + NodeManager* nm = NodeManager::currentNM(); + + Node formula = nm->mkNode(AND, asserts); + std::vector vars; + std::vector subs; + Trace("model-core") << "Assignments: " << std::endl; + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(formula); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar()) + { + Node vcur = Node::fromExpr(m->getValue(cur.toExpr())); + Trace("model-core") << " " << cur << " -> " << vcur << std::endl; + vars.push_back(cur); + subs.push_back(vcur); + } + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + visit.push_back(cur.getOperator()); + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } while (!visit.empty()); + + Node truen = nm->mkConst(true); + + Trace("model-core") << "Minimizing substitution..." << std::endl; + std::vector coreVars; + bool minimized = + theory::SubstitutionMinimize::find(formula, truen, vars, subs, coreVars); + Assert(minimized, + "cannot compute model core, since model does not satisfy input!"); + if (minimized) + { + m->setUsingModelCore(); + Trace("model-core") << "...got core vars : " << coreVars << std::endl; + + for (const Node& cv : coreVars) + { + m->recordModelCoreSymbol(cv.toExpr()); + } + return true; + } + Trace("model-core") << "...failed, model does not satisfy input!" + << std::endl; + return false; +} + +} /* namespace CVC4 */ diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h new file mode 100644 index 000000000..29348a4f4 --- /dev/null +++ b/src/smt/model_core_builder.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file model_core_builder.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 building model cores + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__MODEL_CORE_BUILDER_H +#define __CVC4__THEORY__MODEL_CORE_BUILDER_H + +#include + +#include "expr/expr.h" +#include "smt/model.h" + +namespace CVC4 { + +/** + * A utility for building model cores. + */ +class ModelCoreBuilder +{ + public: + /** set model core + * + * This function updates the model m so that it is a minimal "core" of + * substitutions that satisfy the formulas in assertions, interpreted + * conjunctively. This is specified via calls to + * Model::setUsingModelCore, Model::recordModelCoreSymbol, + * for details see smt/model.h. + * + * It returns true if m is a model for assertions. In this case, we set: + * m->usingModelCore(); + * m->recordModelCoreSymbol(s1); ... m->recordModelCoreSymbol(sn); + * such that each formula in assertions under the substitution + * { s1 -> m(s1), ..., sn -> m(sn) } rewrites to true. + * + * If m is not a model for assertions, this method returns false and m is + * left unchanged. + */ + static bool setModelCore(const std::vector& assertions, Model* m); +}; /* class TheoryModelCoreBuilder */ + +} // namespace CVC4 + +#endif /* __CVC4__THEORY__MODEL_CORE_BUILDER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8cd236a89..73264daa5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -114,6 +114,7 @@ #include "smt/command_list.h" #include "smt/logic_request.h" #include "smt/managed_ostreams.h" +#include "smt/model_core_builder.h" #include "smt/smt_engine_scope.h" #include "smt/term_formula_removal.h" #include "smt/update_ostream.h" @@ -1255,12 +1256,13 @@ void SmtEngine::setDefaults() { is_sygus = true; } - if ((options::checkModels() || options::checkSynthSol()) + if ((options::checkModels() || options::checkSynthSol() + || options::produceModelCores()) && !options::produceAssertions()) { - Notice() << "SmtEngine: turning on produce-assertions to support " - << "check-models or check-synth-sol." << endl; - setOption("produce-assertions", SExpr("true")); + Notice() << "SmtEngine: turning on produce-assertions to support " + << "check-models, check-synth-sol or produce-model-cores." << endl; + setOption("produce-assertions", SExpr("true")); } // Disable options incompatible with incremental solving, unsat cores, and @@ -1452,7 +1454,7 @@ void SmtEngine::setDefaults() { // cases where we need produce models if (!options::produceModels() && (options::produceAssignments() || options::sygusRewSynthCheck() - || is_sygus)) + || options::produceModelCores() || is_sygus)) { Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); @@ -4125,6 +4127,14 @@ Model* SmtEngine::getModel() { throw ModalException(msg); } TheoryModel* m = d_theoryEngine->getModel(); + + if (options::produceModelCores()) + { + // If we enabled model cores, we compute a model core for m based on our + // assertions using the model core builder utility + std::vector easserts = getAssertions(); + ModelCoreBuilder::setModelCore(easserts, m); + } m->d_inputName = d_filename; return m; } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 470f9ac7f..9ccaa58e9 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -57,6 +57,12 @@ unsigned getSignExtendAmount(TNode node) /* ------------------------------------------------------------------------- */ +bool isOnes(TNode node) +{ + if (!node.isConst()) return false; + return node == mkOnes(getSize(node)); +} + bool isZero(TNode node) { if (!node.isConst()) return false; diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 9fccf92a7..2ece472e4 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -52,6 +52,9 @@ unsigned getExtractLow(TNode node); /* Get the number of bits by which a given node is extended. */ unsigned getSignExtendAmount(TNode node); +/* Returns true if given node represents a bit-vector comprised of ones. */ +bool isOnes(TNode node); + /* Returns true if given node represents a zero bit-vector. */ bool isZero(TNode node); diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index d0e6b0247..d2b7688ec 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -879,7 +879,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) return false; } -Node TermUtil::isSingularArg(Node n, Kind ik, int arg) +Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) { TypeNode tn = n.getType(); if (n == getTypeValue(tn, 0)) @@ -918,10 +918,6 @@ Node TermUtil::isSingularArg(Node n, Kind ik, int arg) { return n; } - else - { - // TODO? - } } else if (ik == STRING_SUBSTR) { diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index bc936e4a3..dd3e76ee2 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -313,10 +313,10 @@ public: /** is singular arg * Returns true if - * ( ... t_{arg-1}, n, t_{arg+1}...) = n - * always holds. + * ( ... t_{arg-1}, n, t_{arg+1}...) = ret + * always holds for some constant ret, which is returned by this function. */ - Node isSingularArg(Node n, Kind ik, int arg); + Node isSingularArg(Node n, Kind ik, unsigned arg); /** get type value * This gets the Node that represents value val for Type tn diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp new file mode 100644 index 000000000..03a55b3a4 --- /dev/null +++ b/src/theory/subs_minimize.cpp @@ -0,0 +1,332 @@ +/********************* */ +/*! \file subs_minimize.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 substitution minimization. + **/ + +#include "theory/subs_minimize.h" + +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +SubstitutionMinimize::SubstitutionMinimize() {} + +bool SubstitutionMinimize::find(Node n, + Node target, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars) +{ + Trace("subs-min") << "Substitution minimize : " << std::endl; + Trace("subs-min") << " substitution : " << vars << " -> " << subs + << std::endl; + Trace("subs-min") << " node : " << n << std::endl; + Trace("subs-min") << " target : " << target << std::endl; + + std::map > fvDepend; + + Trace("subs-min") << "--- Compute values for subterms..." << std::endl; + // the value of each subterm in n under the substitution + std::unordered_map value; + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = value.find(cur); + + if (it == value.end()) + { + if (cur.isVar()) + { + const std::vector::const_iterator& it = + std::find(vars.begin(), vars.end(), cur); + if (it == vars.end()) + { + value[cur] = cur; + } + else + { + ptrdiff_t pos = std::distance(vars.begin(), it); + value[cur] = subs[pos]; + } + } + else + { + value[cur] = Node::null(); + visit.push_back(cur); + if (cur.getKind() == APPLY_UF) + { + visit.push_back(cur.getOperator()); + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + else if (it->second.isNull()) + { + Node ret = cur; + if (cur.getNumChildren() > 0) + { + std::vector children; + NodeBuilder<> nb(cur.getKind()); + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + if (cur.getKind() == APPLY_UF) + { + children.push_back(cur.getOperator()); + } + else + { + nb << cur.getOperator(); + } + } + children.insert(children.end(), cur.begin(), cur.end()); + for (const Node& cn : children) + { + it = value.find(cn); + Assert(it != value.end()); + Assert(!it->second.isNull()); + nb << it->second; + } + ret = nb.constructNode(); + ret = Rewriter::rewrite(ret); + } + value[cur] = ret; + } + } while (!visit.empty()); + Assert(value.find(n) != value.end()); + Assert(!value.find(n)->second.isNull()); + + Trace("subs-min") << "... got " << value[n] << std::endl; + if (value[n] != target) + { + Trace("subs-min") << "... not equal to target " << target << std::endl; + return false; + } + + Trace("subs-min") << "--- Compute relevant variables..." << std::endl; + std::unordered_set rlvFv; + // only variables that occur in assertions are relevant + std::map iteBranch; + std::map > justifyArgs; + + visit.push_back(n); + std::unordered_set visited; + std::unordered_set::iterator itv; + do + { + cur = visit.back(); + visit.pop_back(); + itv = visited.find(cur); + if (itv == visited.end()) + { + visited.insert(cur); + it = value.find(cur); + if (it->second == cur) + { + // if its value is the same as current, there is nothing to do + } + else if (cur.isVar()) + { + // must include + rlvFv.insert(cur); + } + else if (cur.getKind() == ITE) + { + // only recurse on relevant branch + Node bval = value[cur[0]]; + Assert(!bval.isNull() && bval.isConst()); + unsigned cindex = bval.getConst() ? 1 : 2; + visit.push_back(cur[0]); + visit.push_back(cur[cindex]); + } + else if (cur.getNumChildren() > 0) + { + Kind ck = cur.getKind(); + bool alreadyJustified = false; + + // if the operator is an apply uf, check its value + if (cur.getKind() == APPLY_UF) + { + Node op = cur.getOperator(); + it = value.find(op); + Assert(it != value.end()); + TNode vop = it->second; + if (vop.getKind() == LAMBDA) + { + visit.push_back(op); + // do iterative partial evaluation on the body of the lambda + Node curr = vop[1]; + for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++) + { + it = value.find(cur[i]); + Assert(it != value.end()); + Node scurr = curr.substitute(vop[0][i], it->second); + // if the valuation of the i^th argument changes the + // interpretation of the body of the lambda, then the i^th + // argument is relevant to the substitution. Hence, we add + // i to visit, and update curr below. + if (scurr != curr) + { + curr = Rewriter::rewrite(scurr); + visit.push_back(cur[i]); + } + } + alreadyJustified = true; + } + } + if (!alreadyJustified) + { + // a subset of the arguments of cur that fully justify the evaluation + std::vector justifyArgs; + if (cur.getNumChildren() > 1) + { + for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++) + { + Node cn = cur[i]; + it = value.find(cn); + Assert(it != value.end()); + Assert(!it->second.isNull()); + if (isSingularArg(it->second, ck, i)) + { + // have we seen this argument already? if so, we are done + if (visited.find(cn) != visited.end()) + { + alreadyJustified = true; + break; + } + justifyArgs.push_back(i); + } + } + } + // we need to recurse on at most one child + if (!alreadyJustified && !justifyArgs.empty()) + { + unsigned sindex = justifyArgs[0]; + // could choose a best index, for now, we just take the first + visit.push_back(cur[sindex]); + alreadyJustified = true; + } + } + if (!alreadyJustified) + { + // must recurse on all arguments, including operator + if (cur.getKind() == APPLY_UF) + { + visit.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + } + } while (!visit.empty()); + + for (const Node& v : rlvFv) + { + Assert(std::find(vars.begin(), vars.end(), v) != vars.end()); + reqVars.push_back(v); + } + + Trace("subs-min") << "... requires " << reqVars.size() << "/" << vars.size() + << " : " << reqVars << std::endl; + + return true; +} + +bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg) +{ + // Notice that this function is hardcoded. We could compute this function + // in a theory-independent way using partial evaluation. However, we + // prefer performance to generality here. + + // TODO: a variant of this code is implemented in quantifiers::TermUtil. + // These implementations should be merged (see #1216). + if (!n.isConst()) + { + return false; + } + if (k == AND) + { + return !n.getConst(); + } + else if (k == OR) + { + return n.getConst(); + } + else if (k == IMPLIES) + { + return arg == (n.getConst() ? 1 : 0); + } + if (k == MULT + || (arg == 0 + && (k == DIVISION_TOTAL || k == INTS_DIVISION_TOTAL + || k == INTS_MODULUS_TOTAL)) + || (arg == 2 && k == STRING_SUBSTR)) + { + // zero + if (n.getConst().sgn() == 0) + { + return true; + } + } + if (k == BITVECTOR_AND || k == BITVECTOR_MULT || k == BITVECTOR_UDIV_TOTAL + || k == BITVECTOR_UREM_TOTAL + || (arg == 0 + && (k == BITVECTOR_SHL || k == BITVECTOR_LSHR + || k == BITVECTOR_ASHR))) + { + if (bv::utils::isZero(n)) + { + return true; + } + } + if (k == BITVECTOR_OR) + { + // bit-vector ones + if (bv::utils::isOnes(n)) + { + return true; + } + } + + if ((arg == 1 && k == STRING_STRCTN) || (arg == 0 && k == STRING_SUBSTR)) + { + // empty string + if (n.getConst().size() == 0) + { + return true; + } + } + if ((arg != 0 && k == STRING_SUBSTR) || (arg == 2 && k == STRING_STRIDOF)) + { + // negative integer + if (n.getConst().sgn() < 0) + { + return true; + } + } + return false; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h new file mode 100644 index 000000000..55e57b921 --- /dev/null +++ b/src/theory/subs_minimize.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \file subs_minimize.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Substitution minimization. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SUBS_MINIMIZE_H +#define __CVC4__THEORY__SUBS_MINIMIZE_H + +#include + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +/** SubstitutionMinimize + * + * This class is used for finding a minimal substitution under which an + * evaluation holds. + */ +class SubstitutionMinimize +{ + public: + SubstitutionMinimize(); + ~SubstitutionMinimize() {} + /** find + * + * If n { vars -> subs } rewrites to target, this method returns true, and + * vars[i1], ..., vars[in] are added to rewVars, such that + * n { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] } also rewrites to + * target. + * + * If n { vars -> subs } does not rewrite to target, this method returns + * false. + */ + static bool find(Node n, + Node target, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars); + + private: + /** is singular arg + * + * Returns true if + * ( ... t_{arg-1}, n, t_{arg+1}...) = c + * always holds for some constant c. + */ + static bool isSingularArg(Node n, Kind k, unsigned arg); +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__SUBS_MINIMIZE_H */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 34e1d455b..2ccc48a6a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -31,6 +31,7 @@ TheoryModel::TheoryModel(context::Context* c, : d_substitutions(c, false), d_modelBuilt(false), d_modelBuiltSuccess(false), + d_using_model_core(false), d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -79,6 +80,8 @@ void TheoryModel::reset(){ d_uf_models.clear(); d_eeContext->pop(); d_eeContext->push(); + d_using_model_core = false; + d_model_core.clear(); } void TheoryModel::getComments(std::ostream& out) const { @@ -114,12 +117,13 @@ std::vector > TheoryModel::getApproximations() const return approx; } -Node TheoryModel::getValue(TNode n, bool useDontCares) const { +Node TheoryModel::getValue(TNode n) const +{ //apply substitutions Node nn = d_substitutions.apply(n); Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model - nn = getModelValue(nn, false, useDontCares); + nn = getModelValue(nn, false); if (nn.isNull()) return nn; if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize @@ -130,8 +134,15 @@ Node TheoryModel::getValue(TNode n, bool useDontCares) const { return nn; } -bool TheoryModel::isDontCare(Expr expr) const { - return getValue(Node::fromExpr(expr), true).isNull(); +bool TheoryModel::isModelCoreSymbol(Expr sym) const +{ + if (!d_using_model_core) + { + return true; + } + Node s = Node::fromExpr(sym); + Assert(s.isVar() && s.getKind() != BOUND_VARIABLE); + return d_model_core.find(s) != d_model_core.end(); } Expr TheoryModel::getValue( Expr expr ) const{ @@ -158,7 +169,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ } } -Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const +Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const { std::unordered_map::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { @@ -303,10 +314,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c } else { - if (options::omitDontCares() && useDontCares) - { - return Node(); - } // Unknown term - return first enumerated value for this type TypeEnumerator te(n.getType()); ret = *te; @@ -491,6 +498,16 @@ void TheoryModel::recordApproximation(TNode n, TNode pred) d_approximations[n] = pred; d_approx_list.push_back(std::pair(n, pred)); } +void TheoryModel::setUsingModelCore() +{ + d_using_model_core = true; + d_model_core.clear(); +} + +void TheoryModel::recordModelCoreSymbol(Expr sym) +{ + d_model_core.insert(Node::fromExpr(sym)); +} void TheoryModel::setUnevaluatedKind(Kind k) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 47d68a365..3ffd1e8c1 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -223,10 +223,8 @@ public: /** Get value function. * This should be called only after a ModelBuilder * has called buildModel(...) on this model. - * useDontCares is whether to return Node::null() if - * n does not occur in the equality engine. */ - Node getValue(TNode n, bool useDontCares = false) const; + Node getValue(TNode n) const; /** get comments */ void getComments(std::ostream& out) const override; @@ -245,8 +243,16 @@ public: const RepSet* getRepSet() const { return &d_rep_set; } /** get the representative set object (FIXME: remove this, see #1199) */ RepSet* getRepSetPtr() { return &d_rep_set; } - /** return whether this node is a don't-care */ - bool isDontCare(Expr expr) const override; + + //---------------------------- model cores + /** set using model core */ + void setUsingModelCore() override; + /** record model core symbol */ + void recordModelCoreSymbol(Expr sym) override; + /** Return whether symbol expr is in the model core. */ + bool isModelCoreSymbol(Expr sym) const override; + //---------------------------- end model cores + /** get value function for Exprs. */ Expr getValue(Expr expr) const override; /** get cardinality for sort */ @@ -301,16 +307,16 @@ public: Node d_false; /** comment stream to include in printing */ std::stringstream d_comment_str; + /** are we using model cores? */ + bool d_using_model_core; + /** symbols that are in the model core */ + std::unordered_set d_model_core; /** Get model value function. * * This function is a helper function for getValue. * hasBoundVars is whether n may contain bound variables - * useDontCares is whether to return Node::null() if - * n does not occur in the equality engine. */ - Node getModelValue(TNode n, - bool hasBoundVars = false, - bool useDontCares = false) const; + Node getModelValue(TNode n, bool hasBoundVars = false) const; /** add term internal * * This will do any model-specific processing necessary for n, diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index ff6bc1d4e..8b690f3e1 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -500,6 +500,7 @@ REG0_TESTS = \ regress0/logops.03.cvc \ regress0/logops.04.cvc \ regress0/logops.05.cvc \ + regress0/model-core.smt2 \ regress0/nl/coeff-sat.smt2 \ regress0/nl/ext-rew-aggr-test.smt2 \ regress0/nl/magnitude-wrong-1020-m.smt2 \ diff --git a/test/regress/regress0/model-core.smt2 b/test/regress/regress0/model-core.smt2 new file mode 100644 index 000000000..6729cb5e0 --- /dev/null +++ b/test/regress/regress0/model-core.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-model-cores +; EXPECT: sat +(set-logic QF_UFLIA) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun f (Int) Int) +(assert (= (f x) 0)) +(assert (or (> z 5) (> y 5))) +(check-sat)