diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-11 13:08:00 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-11 11:08:00 -0700 |
commit | 64c48c4d3b4c26b0ba28ab1ab11ef2314ca0cbee (patch) | |
tree | ece6319150e855d2b0850f7508d9e3ee080b7f03 /src/theory | |
parent | 2fb903ed7309fd97c848b03f6587c9d0604efd24 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.h | 6 | ||||
-rw-r--r-- | src/theory/subs_minimize.cpp | 332 | ||||
-rw-r--r-- | src/theory/subs_minimize.h | 66 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 35 | ||||
-rw-r--r-- | src/theory/theory_model.h | 26 |
8 files changed, 453 insertions, 27 deletions
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 - * <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 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<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 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 <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 */ 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<std::pair<Expr, Expr> > 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<Node, Node, NodeHashFunction>::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<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) { 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<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, |