diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-30 11:57:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-30 11:57:58 -0500 |
commit | bc0c0b8b9ea77e8e4e328dbe66a4582fa7883eda (patch) | |
tree | 4f43e20e294ade551676847668ceb424d44bab4f /src/theory/strings/regexp_elim.cpp | |
parent | 3eac9d04c5d4bfba81142d4a5fe91b86590b32ae (diff) |
Add regular expression elimination module (#2400)
Diffstat (limited to 'src/theory/strings/regexp_elim.cpp')
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 446 |
1 files changed, 446 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp new file mode 100644 index 000000000..7d65a872c --- /dev/null +++ b/src/theory/strings/regexp_elim.cpp @@ -0,0 +1,446 @@ +/********************* */ +/*! \file regexp_elim.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 techniques for eliminating regular expressions + ** + **/ + +#include "theory/strings/regexp_elim.h" + +#include "options/strings_options.h" +#include "theory/strings/theory_strings_rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +RegExpElimination::RegExpElimination() +{ + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); +} + +Node RegExpElimination::eliminate(Node atom) +{ + Assert(atom.getKind() == STRING_IN_REGEXP); + if (atom[1].getKind() == REGEXP_CONCAT) + { + return eliminateConcat(atom); + } + else if (atom[1].getKind() == REGEXP_STAR) + { + return eliminateStar(atom); + } + return Node::null(); +} + +Node RegExpElimination::eliminateConcat(Node atom) +{ + NodeManager* nm = NodeManager::currentNM(); + Node x = atom[0]; + Node lenx = nm->mkNode(STRING_LENGTH, x); + Node re = atom[1]; + // memberships of the form x in re.++ * s1 * ... * sn *, where * are + // any number of repetitions (exact or indefinite) of re.allchar. + Trace("re-elim-debug") << "Try re concat with gaps " << atom << std::endl; + std::vector<Node> children; + TheoryStringsRewriter::getConcat(re, children); + bool onlySigmasAndConsts = true; + std::vector<Node> sep_children; + std::vector<unsigned> gap_minsize; + std::vector<bool> gap_exact; + // the first gap is initially strict zero + gap_minsize.push_back(0); + gap_exact.push_back(true); + for (const Node& c : children) + { + Trace("re-elim-debug") << " " << c << std::endl; + onlySigmasAndConsts = false; + if (c.getKind() == STRING_TO_REGEXP) + { + onlySigmasAndConsts = true; + sep_children.push_back(c[0]); + // the next gap is initially strict zero + gap_minsize.push_back(0); + gap_exact.push_back(true); + } + else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA) + { + // found a gap of any size + onlySigmasAndConsts = true; + gap_exact[gap_exact.size() - 1] = false; + } + else if (c.getKind() == REGEXP_SIGMA) + { + // add one to the minimum size of the gap + onlySigmasAndConsts = true; + gap_minsize[gap_minsize.size() - 1]++; + } + if (!onlySigmasAndConsts) + { + Trace("re-elim-debug") << "...cannot handle " << c << std::endl; + break; + } + } + // we should always rewrite concatenations that are purely re.allchar + // and re.*( re.allchar ). + Assert(!onlySigmasAndConsts || !sep_children.empty()); + if (onlySigmasAndConsts && !sep_children.empty()) + { + bool canProcess = true; + std::vector<Node> conj; + // The following constructs a set of constraints that encodes that a + // set of string terms are found, in order, in string x. + // prev_end stores the current (symbolic) index in x that we are + // searching. + Node prev_end = d_zero; + unsigned gap_minsize_end = gap_minsize.back(); + bool gap_exact_end = gap_exact.back(); + std::vector<Node> non_greedy_find_vars; + for (unsigned i = 0, size = sep_children.size(); i < size; i++) + { + Node sc = sep_children[i]; + if (gap_minsize[i] > 0) + { + // the gap to this child is at least gap_minsize[i] + prev_end = + nm->mkNode(PLUS, prev_end, nm->mkConst(Rational(gap_minsize[i]))); + } + Node lensc = nm->mkNode(STRING_LENGTH, sc); + if (gap_exact[i]) + { + // if the gap is exact, it is a substring constraint + Node curr = prev_end; + Node ss = nm->mkNode(STRING_SUBSTR, x, curr, lensc); + conj.push_back(ss.eqNode(sc)); + prev_end = nm->mkNode(PLUS, curr, lensc); + } + else + { + // otherwise, we can use indexof to represent some next occurrence + if (gap_exact[i + 1] && i + 1 != size) + { + if (!options::regExpElimAgg()) + { + canProcess = false; + break; + } + // if the gap after this one is strict, we need a non-greedy find + // thus, we add a symbolic constant + Node k = nm->mkBoundVar(nm->integerType()); + non_greedy_find_vars.push_back(k); + prev_end = nm->mkNode(PLUS, prev_end, k); + } + Node curr = nm->mkNode(STRING_STRIDOF, x, sc, prev_end); + Node idofFind = curr.eqNode(d_neg_one).negate(); + conj.push_back(idofFind); + prev_end = nm->mkNode(PLUS, curr, lensc); + } + } + + if (canProcess) + { + // since sep_children is non-empty, conj is non-empty + Assert(!conj.empty()); + // Process the last gap, if necessary. + // Notice that if the last gap is not exact and its minsize is zero, + // then the last indexof/substr constraint entails the following + // constraint, so it is not necessary to add. + if (gap_minsize_end > 0 || gap_exact_end) + { + Node fit = nm->mkNode( + gap_exact_end ? EQUAL : LEQ, + nm->mkNode(PLUS, prev_end, nm->mkConst(Rational(gap_minsize_end))), + lenx); + conj.push_back(fit); + } + Node res = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); + // process the non-greedy find variables + if (!non_greedy_find_vars.empty()) + { + std::vector<Node> children; + for (const Node& v : non_greedy_find_vars) + { + Node bound = nm->mkNode( + AND, nm->mkNode(LEQ, d_zero, v), nm->mkNode(LT, v, lenx)); + children.push_back(bound); + } + children.push_back(res); + Node body = nm->mkNode(AND, children); + Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars); + res = nm->mkNode(EXISTS, bvl, body); + } + // e.g., writing "A" for (str.to.re "A") and _ for re.allchar: + // x in (re.++ "A" (re.* _) "B" (re.* _)) ---> + // substr(x,0,1)="A" ^ indexof(x,"B",1)!=-1 + // x in (re.++ (re.* _) "A" _ _ _ (re.* _) "B" _ _ (re.* _)) ---> + // indexof(x,"A",0)!=-1 ^ + // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 ) != -1 ^ + // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 )+1+2 <= len(x) + + // An example of a non-greedy find: + // x in re.++( re.*( _ ), "A", _, "B", re.*( _ ) ) ---> + // exists k. 0 <= k < len( x ) ^ + // indexof( x, "A", k ) != -1 ^ + // substr( x, indexof( x, "A", k )+2, 1 ) = "B" + return returnElim(atom, res, "concat-with-gaps"); + } + } + + if (!options::regExpElimAgg()) + { + return Node::null(); + } + // only aggressive rewrites below here + + // if the first or last child is constant string, we can split the membership + // into a conjunction of two memberships. + Node sStartIndex = d_zero; + Node sLength = lenx; + std::vector<Node> sConstraints; + std::vector<Node> rexpElimChildren; + unsigned nchildren = children.size(); + Assert(nchildren > 1); + for (unsigned r = 0; r < 2; r++) + { + unsigned index = r == 0 ? 0 : nchildren - 1; + Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP); + Node c = children[index]; + if (c.getKind() == STRING_TO_REGEXP) + { + Node s = c[0]; + Node lens = nm->mkNode(STRING_LENGTH, s); + Node sss = r == 0 ? d_zero : nm->mkNode(MINUS, lenx, lens); + Node ss = nm->mkNode(STRING_SUBSTR, x, sss, lens); + sConstraints.push_back(ss.eqNode(s)); + if (r == 0) + { + sStartIndex = lens; + } + sLength = nm->mkNode(MINUS, sLength, lens); + } + if (r == 1 && !sConstraints.empty()) + { + // add the middle children + for (unsigned i = 1; i < (nchildren - 1); i++) + { + rexpElimChildren.push_back(children[i]); + } + } + if (c.getKind() != STRING_TO_REGEXP) + { + rexpElimChildren.push_back(c); + } + } + Assert(rexpElimChildren.size() + sConstraints.size() == nchildren); + if (!sConstraints.empty()) + { + Node ss = nm->mkNode(STRING_SUBSTR, x, sStartIndex, sLength); + Assert(!rexpElimChildren.empty()); + Node regElim = + TheoryStringsRewriter::mkConcat(REGEXP_CONCAT, rexpElimChildren); + sConstraints.push_back(nm->mkNode(STRING_IN_REGEXP, ss, regElim)); + Node ret = nm->mkNode(AND, sConstraints); + // e.g. + // x in re.++( "A", R ) ---> substr(x,0,1)="A" ^ substr(x,1,len(x)-1) in R + return returnElim(atom, ret, "concat-splice"); + } + Assert(nchildren > 1); + for (unsigned i = 0; i < nchildren; i++) + { + if (children[i].getKind() == STRING_TO_REGEXP) + { + Node s = children[i][0]; + Node lens = nm->mkNode(STRING_LENGTH, s); + // there exists an index in this string such that the substring is this + Node k; + std::vector<Node> echildren; + if (i == 0) + { + k = d_zero; + } + else if (i + 1 == nchildren) + { + k = nm->mkNode(MINUS, lenx, lens); + } + else + { + k = nm->mkBoundVar(nm->integerType()); + Node bound = + nm->mkNode(AND, + nm->mkNode(LEQ, d_zero, k), + nm->mkNode(LT, k, nm->mkNode(MINUS, lenx, lens))); + echildren.push_back(bound); + } + Node substrEq = nm->mkNode(STRING_SUBSTR, x, k, lens).eqNode(s); + echildren.push_back(substrEq); + if (i > 0) + { + std::vector<Node> rprefix; + rprefix.insert(rprefix.end(), children.begin(), children.begin() + i); + Node rpn = TheoryStringsRewriter::mkConcat(REGEXP_CONCAT, rprefix); + Node substrPrefix = nm->mkNode( + STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, x, d_zero, k), rpn); + echildren.push_back(substrPrefix); + } + if (i + 1 < nchildren) + { + std::vector<Node> rsuffix; + rsuffix.insert(rsuffix.end(), children.begin() + i + 1, children.end()); + Node rps = TheoryStringsRewriter::mkConcat(REGEXP_CONCAT, rsuffix); + Node ks = nm->mkNode(PLUS, k, lens); + Node substrSuffix = nm->mkNode( + STRING_IN_REGEXP, + nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(MINUS, lenx, ks)), + rps); + echildren.push_back(substrSuffix); + } + Node body = nm->mkNode(AND, echildren); + if (k.getKind() == BOUND_VARIABLE) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, k); + body = nm->mkNode(EXISTS, bvl, body); + } + // e.g. x in re.++( R1, "AB", R2 ) ---> + // exists k. + // 0 <= k <= (len(x)-2) ^ + // substr( x, k, 2 ) = "AB" ^ + // substr( x, 0, k ) in R1 ^ + // substr( x, k+2, len(x)-(k+2) ) in R2 + return returnElim(atom, body, "concat-find"); + } + } + return Node::null(); +} + +Node RegExpElimination::eliminateStar(Node atom) +{ + if (!options::regExpElimAgg()) + { + return Node::null(); + } + // only aggressive rewrites below here + + NodeManager* nm = NodeManager::currentNM(); + Node x = atom[0]; + Node lenx = nm->mkNode(STRING_LENGTH, x); + Node re = atom[1]; + // for regular expression star, + // if the period is a fixed constant, we can turn it into a bounded + // quantifier + std::vector<Node> disj; + if (re[0].getKind() == REGEXP_UNION) + { + for (const Node& r : re[0]) + { + disj.push_back(r); + } + } + else + { + disj.push_back(re[0]); + } + bool lenOnePeriod = true; + std::vector<Node> char_constraints; + Node index = nm->mkBoundVar(nm->integerType()); + Node substr_ch = nm->mkNode(STRING_SUBSTR, x, index, d_one); + substr_ch = Rewriter::rewrite(substr_ch); + // handle the case where it is purely characters + for (const Node& r : disj) + { + Assert(r.getKind() != REGEXP_UNION); + Assert(r.getKind() != REGEXP_SIGMA); + lenOnePeriod = false; + // lenOnePeriod is true if this regular expression is a single character + // regular expression + if (r.getKind() == STRING_TO_REGEXP) + { + Node s = r[0]; + if (s.isConst() && s.getConst<String>().size() == 1) + { + lenOnePeriod = true; + } + } + else if (r.getKind() == REGEXP_RANGE) + { + lenOnePeriod = true; + } + if (!lenOnePeriod) + { + break; + } + else + { + Node regexp_ch = nm->mkNode(STRING_IN_REGEXP, substr_ch, r); + regexp_ch = Rewriter::rewrite(regexp_ch); + Assert(regexp_ch.getKind() != STRING_IN_REGEXP); + char_constraints.push_back(regexp_ch); + } + } + if (lenOnePeriod) + { + Assert(!char_constraints.empty()); + Node bound = nm->mkNode( + AND, nm->mkNode(LEQ, d_zero, index), nm->mkNode(LT, index, lenx)); + Node conc = char_constraints.size() == 1 ? char_constraints[0] + : nm->mkNode(OR, char_constraints); + Node body = nm->mkNode(OR, bound.negate(), conc); + Node bvl = nm->mkNode(BOUND_VAR_LIST, index); + Node res = nm->mkNode(FORALL, bvl, body); + // e.g. + // x in (re.* (re.union "A" "B" )) ---> + // forall k. 0<=k<len(x) => (substr(x,k,1) in "A" OR substr(x,k,1) in "B") + return returnElim(atom, res, "star-char"); + } + // otherwise, for stars of constant length these are periodic + if (disj.size() == 1) + { + Node r = disj[0]; + if (r.getKind() == STRING_TO_REGEXP) + { + Node s = r[0]; + if (s.isConst()) + { + Node lens = nm->mkNode(STRING_LENGTH, s); + lens = Rewriter::rewrite(lens); + Assert(lens.isConst()); + std::vector<Node> conj; + Node bound = nm->mkNode( + AND, + nm->mkNode(LEQ, d_zero, index), + nm->mkNode(LT, index, nm->mkNode(INTS_DIVISION, lenx, lens))); + Node conc = + nm->mkNode(STRING_SUBSTR, x, nm->mkNode(MULT, index, lens), lens) + .eqNode(s); + Node body = nm->mkNode(OR, bound.negate(), conc); + Node bvl = nm->mkNode(BOUND_VAR_LIST, index); + Node res = nm->mkNode(FORALL, bvl, body); + res = nm->mkNode( + AND, nm->mkNode(INTS_MODULUS, lenx, lens).eqNode(d_zero), res); + // e.g. + // x in ("abc")* ---> + // forall k. 0 <= k < (len( x ) div 3) => substr(x,3*k,3) = "abc" ^ + // len(x) mod 3 = 0 + return returnElim(atom, res, "star-constant"); + } + } + } + return Node::null(); +} + +Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id) +{ + Trace("re-elim") << "re-elim: " << atom << " to " << atomElim << " by " << id + << "." << std::endl; + return atomElim; +} |