diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-24 09:32:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-24 09:32:14 -0500 |
| commit | afe40162490ac54e1741e80d43496268ae76201d (patch) | |
| tree | 3eec0ce98cd8dbffb5cb1dc3d0d3a884a158d6bc /src/theory/strings/regexp_elim.cpp | |
| parent | 5f384849d20c915374c7b189a232c5d811c186ef (diff) | |
Move string util functions (#3115)
Diffstat (limited to 'src/theory/strings/regexp_elim.cpp')
| -rw-r--r-- | src/theory/strings/regexp_elim.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index e132d8e24..42d679692 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -17,6 +17,7 @@ #include "options/strings_options.h" #include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/theory_strings_utils.h" using namespace CVC4; using namespace CVC4::kind; @@ -51,7 +52,7 @@ Node RegExpElimination::eliminateConcat(Node atom) Node lenx = nm->mkNode(STRING_LENGTH, x); Node re = atom[1]; std::vector<Node> children; - TheoryStringsRewriter::getConcat(re, children); + utils::getConcat(re, children); // If it can be reduced to memberships in fixed length regular expressions. // This includes concatenations where at most one child is of the form @@ -380,8 +381,7 @@ Node RegExpElimination::eliminateConcat(Node atom) Assert(rexpElimChildren.size() + sConstraints.size() == nchildren); Node ss = nm->mkNode(STRING_SUBSTR, x, sStartIndex, sLength); Assert(!rexpElimChildren.empty()); - Node regElim = - TheoryStringsRewriter::mkConcat(REGEXP_CONCAT, rexpElimChildren); + Node regElim = utils::mkConcat(REGEXP_CONCAT, rexpElimChildren); sConstraints.push_back(nm->mkNode(STRING_IN_REGEXP, ss, regElim)); Node ret = nm->mkNode(AND, sConstraints); // e.g. @@ -421,7 +421,7 @@ Node RegExpElimination::eliminateConcat(Node atom) { std::vector<Node> rprefix; rprefix.insert(rprefix.end(), children.begin(), children.begin() + i); - Node rpn = TheoryStringsRewriter::mkConcat(REGEXP_CONCAT, rprefix); + Node rpn = utils::mkConcat(REGEXP_CONCAT, rprefix); Node substrPrefix = nm->mkNode( STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, x, d_zero, k), rpn); echildren.push_back(substrPrefix); @@ -430,7 +430,7 @@ Node RegExpElimination::eliminateConcat(Node atom) { std::vector<Node> rsuffix; rsuffix.insert(rsuffix.end(), children.begin() + i + 1, children.end()); - Node rps = TheoryStringsRewriter::mkConcat(REGEXP_CONCAT, rsuffix); + Node rps = utils::mkConcat(REGEXP_CONCAT, rsuffix); Node ks = nm->mkNode(PLUS, k, lens); Node substrSuffix = nm->mkNode( STRING_IN_REGEXP, |