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/subs_minimize.cpp | |
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/subs_minimize.cpp')
-rw-r--r-- | src/theory/subs_minimize.cpp | 332 |
1 files changed, 332 insertions, 0 deletions
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 |