diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 18:09:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-20 18:09:27 -0500 |
| commit | 0e62e42f739e467f61f5c3d10e7b1c7356db6406 (patch) | |
| tree | a4281c5b2c0881c2d622da68322e213f7168801b /src/theory/strings/regexp_elim.cpp | |
| parent | 0a0cee14c38cac0f87772c192ef387dcd36b6977 (diff) | |
Generalize mkConcat for types (#4123)
Towards theory of sequences.
The utility function mkConcat needs a type to know what to construct in the empty string case.
Diffstat (limited to 'src/theory/strings/regexp_elim.cpp')
| -rw-r--r-- | src/theory/strings/regexp_elim.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 976efad3c..259588789 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -30,6 +30,7 @@ RegExpElimination::RegExpElimination() d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); + d_regExpType = NodeManager::currentNM()->regExpType(); } Node RegExpElimination::eliminate(Node atom) @@ -382,7 +383,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 = utils::mkConcat(REGEXP_CONCAT, rexpElimChildren); + Node regElim = utils::mkConcat(rexpElimChildren, d_regExpType); sConstraints.push_back(nm->mkNode(STRING_IN_REGEXP, ss, regElim)); Node ret = nm->mkNode(AND, sConstraints); // e.g. @@ -422,7 +423,7 @@ Node RegExpElimination::eliminateConcat(Node atom) { std::vector<Node> rprefix; rprefix.insert(rprefix.end(), children.begin(), children.begin() + i); - Node rpn = utils::mkConcat(REGEXP_CONCAT, rprefix); + Node rpn = utils::mkConcat(rprefix, d_regExpType); Node substrPrefix = nm->mkNode( STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, x, d_zero, k), rpn); echildren.push_back(substrPrefix); @@ -431,7 +432,7 @@ Node RegExpElimination::eliminateConcat(Node atom) { std::vector<Node> rsuffix; rsuffix.insert(rsuffix.end(), children.begin() + i + 1, children.end()); - Node rps = utils::mkConcat(REGEXP_CONCAT, rsuffix); + Node rps = utils::mkConcat(rsuffix, d_regExpType); Node ks = nm->mkNode(PLUS, k, lens); Node substrSuffix = nm->mkNode( STRING_IN_REGEXP, |