This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
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 \
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 \
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"
for(size_t i = 0; i < m.getNumCommands(); ++i) {
const Command* cmd = m.getCommand(i);
const DeclareFunctionCommand* dfc = dynamic_cast<const DeclareFunctionCommand*>(cmd);
- if (dfc != NULL && m.isDontCare(dfc->getFunction())) {
+ if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction()))
+ {
continue;
}
toStream(out, m, cmd);
/** 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 */
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 */
--- /dev/null
+/********************* */
+/*! \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<Expr>& 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<Node> 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<Node> vars;
+ std::vector<Node> subs;
+ Trace("model-core") << "Assignments: " << std::endl;
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::vector<TNode> 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<Node> 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 */
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Expr>& assertions, Model* m);
+}; /* class TheoryModelCoreBuilder */
+
+} // namespace CVC4
+
+#endif /* __CVC4__THEORY__MODEL_CORE_BUILDER_H */
#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"
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
// 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"));
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<Expr> easserts = getAssertions();
+ ModelCoreBuilder::setModelCore(easserts, m);
+ }
m->d_inputName = d_filename;
return m;
}
/* ------------------------------------------------------------------------- */
+bool isOnes(TNode node)
+{
+ if (!node.isConst()) return false;
+ return node == mkOnes(getSize(node));
+}
+
bool isZero(TNode node)
{
if (!node.isConst()) return false;
/* 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);
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))
{
return n;
}
- else
- {
- // TODO?
- }
}
else if (ik == STRING_SUBSTR)
{
/** is singular arg
* Returns true if
- * <k>( ... t_{arg-1}, n, t_{arg+1}...) = n
- * always holds.
+ * <k>( ... 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
--- /dev/null
+/********************* */
+/*! \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<Node>& vars,
+ const std::vector<Node>& subs,
+ std::vector<Node>& 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<Node, std::unordered_set<Node, NodeHashFunction> > fvDepend;
+
+ Trace("subs-min") << "--- Compute values for subterms..." << std::endl;
+ // the value of each subterm in n under the substitution
+ std::unordered_map<TNode, Node, TNodeHashFunction> value;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> 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<Node>::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<Node> 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<Node, NodeHashFunction> rlvFv;
+ // only variables that occur in assertions are relevant
+ std::map<Node, unsigned> iteBranch;
+ std::map<Node, std::vector<unsigned> > justifyArgs;
+
+ visit.push_back(n);
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::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<bool>() ? 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<unsigned> 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<bool>();
+ }
+ else if (k == OR)
+ {
+ return n.getConst<bool>();
+ }
+ else if (k == IMPLIES)
+ {
+ return arg == (n.getConst<bool>() ? 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<Rational>().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<String>().size() == 0)
+ {
+ return true;
+ }
+ }
+ if ((arg != 0 && k == STRING_SUBSTR) || (arg == 2 && k == STRING_STRIDOF))
+ {
+ // negative integer
+ if (n.getConst<Rational>().sgn() < 0)
+ {
+ return true;
+ }
+ }
+ return false;
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& vars,
+ const std::vector<Node>& subs,
+ std::vector<Node>& reqVars);
+
+ private:
+ /** is singular arg
+ *
+ * Returns true if
+ * <k>( ... 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 */
: d_substitutions(c, false),
d_modelBuilt(false),
d_modelBuiltSuccess(false),
+ d_using_model_core(false),
d_enableFuncModels(enableFuncModels)
{
d_true = NodeManager::currentNM()->mkConst( true );
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 {
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
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{
}
}
-Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const
+Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
{
std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
if (it != d_modelCache.end()) {
}
else
{
- if (options::omitDontCares() && useDontCares)
- {
- return Node();
- }
// Unknown term - return first enumerated value for this type
TypeEnumerator te(n.getType());
ret = *te;
d_approximations[n] = pred;
d_approx_list.push_back(std::pair<Node, Node>(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)
{
/** 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;
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 */
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<Node, NodeHashFunction> 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,
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 \
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff