diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-19 08:14:42 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-19 08:14:42 -0700 |
commit | 6a0a7f45a5ff176eb53f1d4939144140a1109893 (patch) | |
tree | 4501c19225cd6780f1c8c3884bae940960264cb2 /src/theory | |
parent | 5a73656535d8363b46818e7f2dc81059d1399005 (diff) | |
parent | c116c6c1ec757fe51f2b874e750ad8281baea103 (diff) |
Merge branch 'master' into fixMacBuildfixMacBuild
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 36 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 13 | ||||
-rw-r--r-- | src/theory/subs_minimize.cpp | 146 | ||||
-rw-r--r-- | src/theory/subs_minimize.h | 46 |
4 files changed, 212 insertions, 29 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7c008dc14..1dc894117 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -507,9 +507,7 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node) } // (= "" (str.replace x "A" "")) ---> (str.prefix x "A") - Node one = nm->mkConst(Rational(1)); - Node ylen = nm->mkNode(STRING_LENGTH, ne[1]); - if (checkEntailArithEq(ylen, one) && ne[2] == empty) + if (checkEntailLengthOne(ne[1]) && ne[2] == empty) { Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]); return returnRewrite(node, ret, "str-emp-repl-emp"); @@ -1658,11 +1656,8 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) // if (str.len y) = 1 and (str.len z) = 1 if (node[1] == zero) { - Node one = nm->mkConst(Rational(1)); - Node n1len = nm->mkNode(kind::STRING_LENGTH, node[0][1]); - Node n2len = nm->mkNode(kind::STRING_LENGTH, node[0][2]); - if (checkEntailArith(one, n1len) && checkEntailArith(one, n2len) - && checkEntailNonEmpty(node[0][1]) && checkEntailNonEmpty(node[0][2])) + if (checkEntailLengthOne(node[0][1], true) + && checkEntailLengthOne(node[0][2], true)) { Node ret = nm->mkNode( kind::STRING_STRREPL, @@ -1739,8 +1734,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } // (str.substr s x x) ---> "" if (str.len s) <= 1 - Node one = nm->mkConst(CVC4::Rational(1)); - if (node[1] == node[2] && checkEntailArith(one, tot_len)) + if (node[1] == node[2] && checkEntailLengthOne(node[0])) { Node ret = nm->mkConst(::CVC4::String("")); return returnRewrite(node, ret, "ss-len-one-z-z"); @@ -2155,8 +2149,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { // (str.contains (str.replace x y x) z) ---> (str.contains x z) // if (str.len z) <= 1 - Node one = nm->mkConst(Rational(1)); - if (checkEntailArith(one, len_n2)) + if (checkEntailLengthOne(node[1])) { Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]); return returnRewrite(node, ret, "ctn-repl-len-one-to-ctn"); @@ -2474,7 +2467,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x) // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "") - if (checkEntailArith(nm->mkConst(Rational(1)), l0)) + if (checkEntailLengthOne(node[0])) { Node empty = nm->mkConst(String("")); Node rn1 = Rewriter::rewrite( @@ -2850,7 +2843,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.replace( x ++ y ++ x ++ y, "A", z ) --> // str.replace( x ++ y, "A", z ) ++ x ++ y // since if "A" occurs in x ++ y ++ x ++ y, then it must occur in x ++ y. - if (node[1].isConst() && node[1].getConst<String>().size() == 1) + if (checkEntailLengthOne(node[1])) { Node lastLhs; unsigned lastCheckIndex = 0; @@ -3826,6 +3819,15 @@ bool TheoryStringsRewriter::checkEntailNonEmpty(Node a) return checkEntailArith(len, true); } +bool TheoryStringsRewriter::checkEntailLengthOne(Node s, bool strict) +{ + NodeManager* nm = NodeManager::currentNM(); + Node one = nm->mkConst(Rational(1)); + Node len = nm->mkNode(STRING_LENGTH, s); + len = Rewriter::rewrite(len); + return checkEntailArith(one, len) && (!strict || checkEntailArith(len, true)); +} + bool TheoryStringsRewriter::checkEntailArithEq(Node a, Node b) { if (a == b) @@ -4714,8 +4716,7 @@ Node TheoryStringsRewriter::getStringOrEmpty(Node n) break; } - Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0])); - if (strlen == nm->mkConst(Rational(1)) && n[2] == empty) + if (checkEntailLengthOne(n[0]) && n[2] == empty) { // (str.replace "A" x "") --> "A" res = n[0]; @@ -4727,8 +4728,7 @@ Node TheoryStringsRewriter::getStringOrEmpty(Node n) } case kind::STRING_SUBSTR: { - Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0])); - if (strlen == nm->mkConst(Rational(1))) + if (checkEntailLengthOne(n[0])) { // (str.substr "A" x y) --> "A" res = n[0]; diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 3d71423ab..2e356f8f7 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -455,6 +455,19 @@ class TheoryStringsRewriter { * the call checkArithEntail( len( a ), true ). */ static bool checkEntailNonEmpty(Node a); + + /** + * Checks whether string has at most/exactly length one. Length one strings + * can be used for more aggressive rewriting because there is guaranteed that + * it cannot be overlap multiple components in a string concatenation. + * + * @param s The string to check + * @param strict If true, the string must have exactly length one, otherwise + * at most length one + * @return True if the string has at most/exactly length one, false otherwise + */ + static bool checkEntailLengthOne(Node s, bool strict = false); + /** check arithmetic entailment equal * Returns true if it is always the case that a = b. */ diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index 03a55b3a4..58daf5c75 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -14,6 +14,7 @@ #include "theory/subs_minimize.h" +#include "expr/node_algorithm.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -25,20 +26,157 @@ namespace theory { SubstitutionMinimize::SubstitutionMinimize() {} -bool SubstitutionMinimize::find(Node n, +bool SubstitutionMinimize::find(Node t, Node target, const std::vector<Node>& vars, const std::vector<Node>& subs, std::vector<Node>& reqVars) { + return findInternal(t, target, vars, subs, reqVars); +} + +void getConjuncts(Node n, std::vector<Node>& conj) +{ + if (n.getKind() == AND) + { + for (const Node& nc : n) + { + conj.push_back(nc); + } + } + else + { + conj.push_back(n); + } +} + +bool SubstitutionMinimize::findWithImplied(Node t, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars, + std::vector<Node>& impliedVars) +{ + NodeManager* nm = NodeManager::currentNM(); + Node truen = nm->mkConst(true); + if (!findInternal(t, truen, vars, subs, reqVars)) + { + return false; + } + if (reqVars.empty()) + { + return true; + } + + // map from conjuncts of t to whether they may be used to show an implied var + std::vector<Node> tconj; + getConjuncts(t, tconj); + // map from conjuncts to their free symbols + std::map<Node, std::unordered_set<Node, NodeHashFunction> > tcFv; + + std::unordered_set<Node, NodeHashFunction> reqSet; + std::vector<Node> reqSubs; + std::map<Node, unsigned> reqVarToIndex; + for (const Node& v : reqVars) + { + reqVarToIndex[v] = reqSubs.size(); + const std::vector<Node>::const_iterator& it = + std::find(vars.begin(), vars.end(), v); + Assert(it != vars.end()); + ptrdiff_t pos = std::distance(vars.begin(), it); + reqSubs.push_back(subs[pos]); + } + std::vector<Node> finalReqVars; + for (const Node& v : vars) + { + if (reqVarToIndex.find(v) == reqVarToIndex.end()) + { + // not a required variable, nothing to do + continue; + } + unsigned vindex = reqVarToIndex[v]; + Node prev = reqSubs[vindex]; + // make identity substitution + reqSubs[vindex] = v; + bool madeImplied = false; + // it is a required variable, can we make an implied variable? + for (const Node& tc : tconj) + { + // ensure we've computed its free symbols + std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator + itf = tcFv.find(tc); + if (itf == tcFv.end()) + { + expr::getSymbols(tc, tcFv[tc]); + itf = tcFv.find(tc); + } + // only have a chance if contains v + if (itf->second.find(v) == itf->second.end()) + { + continue; + } + // try the current substitution + Node tcs = tc.substitute( + reqVars.begin(), reqVars.end(), reqSubs.begin(), reqSubs.end()); + Node tcsr = Rewriter::rewrite(tcs); + std::vector<Node> tcsrConj; + getConjuncts(tcsr, tcsrConj); + for (const Node& tcc : tcsrConj) + { + if (tcc.getKind() == EQUAL) + { + for (unsigned r = 0; r < 2; r++) + { + if (tcc[r] == v) + { + Node res = tcc[1 - r]; + if (res.isConst()) + { + Assert(res == prev); + madeImplied = true; + break; + } + } + } + } + if (madeImplied) + { + break; + } + } + if (madeImplied) + { + break; + } + } + if (!madeImplied) + { + // revert the substitution + reqSubs[vindex] = prev; + finalReqVars.push_back(v); + } + else + { + impliedVars.push_back(v); + } + } + reqVars.clear(); + reqVars.insert(reqVars.end(), finalReqVars.begin(), finalReqVars.end()); + + return true; +} + +bool SubstitutionMinimize::findInternal(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; @@ -124,8 +262,6 @@ bool SubstitutionMinimize::find(Node n, 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; diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h index 55e57b921..bf6ccffae 100644 --- a/src/theory/subs_minimize.h +++ b/src/theory/subs_minimize.h @@ -36,21 +36,55 @@ class 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 t { vars -> subs } rewrites to target, this method returns true, and + * vars[i_1], ..., vars[i_n] are added to reqVars, such that i_1, ..., i_n are + * distinct, and t { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] } + * rewrites to target. * - * If n { vars -> subs } does not rewrite to target, this method returns + * If t { vars -> subs } does not rewrite to target, this method returns * false. */ - static bool find(Node n, + static bool find(Node t, Node target, const std::vector<Node>& vars, const std::vector<Node>& subs, std::vector<Node>& reqVars); + /** find with implied + * + * This method should be called on a formula t. + * + * If t { vars -> subs } rewrites to true, this method returns true, + * vars[i_1], ..., vars[i_n] are added to reqVars, and + * vars[i_{n+1}], ..., vars[i_{n+m}] are added to impliedVars such that + * i_1...i_{n+m} are distinct, i_{n+1} < ... < i_{n+m}, and: + * + * (1) t { vars[i_1]->subs[i_1], ..., vars[i_{n+k}]->subs[i_{n+k}] } implies + * vars[i_{n+k+1}] = subs[i_{n+k+1}] for k = 0, ..., m-1. + * + * (2) t { vars[i_1] -> subs[i_1], ..., vars[i_{n+m}] -> subs[i_{n+m}] } + * rewrites to true. + * + * For example, given (x>0 ^ x = y ^ y = z){ x -> 1, y -> 1, z -> 1, w -> 0 }, + * this method may add { x } to reqVars, and { y, z } to impliedVars. + * + * Notice that the order of variables in vars matters. By the semantics above, + * variables that appear earlier in the variable list vars are more likely + * to appear in reqVars, whereas those later in the vars are more likely to + * appear in impliedVars. + */ + static bool findWithImplied(Node t, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars, + std::vector<Node>& impliedVars); private: + /** Common helper function for the above functions. */ + static bool findInternal(Node t, + Node target, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars); /** is singular arg * * Returns true if |