Move string util functions (#3115)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index ec52bf9905988f850549f96f46ee1d52f5d5cc00..63f19355740e6cdb6c3860d7f106ea23bb52386a 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -961,10 +961,8 @@ Node QuantifiersRewriter::getVarElimLitString(Node lit,
           Node slv = lit[1 - i];
           std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j);
           std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end());
-          Node tpre =
-              strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, preL);
-          Node tpost =
-              strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, postL);
+          Node tpre = strings::utils::mkConcat(STRING_CONCAT, preL);
+          Node tpost = strings::utils::mkConcat(STRING_CONCAT, postL);
           Node slvL = nm->mkNode(STRING_LENGTH, slv);
           Node tpreL = nm->mkNode(STRING_LENGTH, tpre);
           Node tpostL = nm->mkNode(STRING_LENGTH, tpost);

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index e132d8e24e4c0e40a17428d22107bdf7886cf282..42d67969262923892a7f2dec8a07e611c7e7a7f9 100644 (file)
--- 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,

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 65d616c3cd0b974b0a2a52810b8ea857af3f89af..49dd1ead6c7a75db50b0f9ddbd1010b131b3b271 100644 (file)
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -21,6 +21,7 @@
 #include "options/strings_options.h"
 #include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
 #include "theory/theory_model.h"
 
 using namespace std;
@@ -438,7 +439,7 @@ bool RegExpSolver::deriveRegExp(Node x,
         {
           vec_nodes.push_back(x[i]);
         }
-        Node left = TheoryStringsRewriter::mkConcat(STRING_CONCAT, vec_nodes);
+        Node left = utils::mkConcat(STRING_CONCAT, vec_nodes);
         left = Rewriter::rewrite(left);
         conc = NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, left, dc);
       }

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6a8cf3e985d10441e076b6a85def4683e79a134d..d720fedc82aa65b1d0ef7cc351add974a258eb9c 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -23,6 +23,7 @@
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/strings/theory_strings_utils.h"
 #include "theory/theory.h"
 #include "util/integer.h"
 #include "util/rational.h"
@@ -120,7 +121,7 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
               std::vector< Node > mchildren_s;
               std::vector< Node > children_s;
               mchildren_s.push_back( xc );
-              getConcat( rc[i], children_s );
+              utils::getConcat(rc[i], children_s);
               Node ret = simpleRegexpConsume( mchildren_s, children_s, t );
               if( !ret.isNull() ){
                 // one conjunct cannot be satisfied, return false
@@ -167,7 +168,7 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
               std::reverse( mchildren_s.begin(), mchildren_s.end() );
             }
             std::vector< Node > children_s;
-            getConcat( rc[0], children_s );
+            utils::getConcat(rc[0], children_s);
             Trace("regexp-ext-rewrite-debug")
                 << "...recursive call on body of star" << std::endl;
             Node ret = simpleRegexpConsume( mchildren_s, children_s, t );
@@ -287,7 +288,7 @@ Node TheoryStringsRewriter::rewriteEquality(Node node)
   std::vector<Node> c[2];
   for (unsigned i = 0; i < 2; i++)
   {
-    strings::TheoryStringsRewriter::getConcat(node[i], c[i]);
+    utils::getConcat(node[i], c[i]);
   }
 
   // check if the prefix, suffix mismatches
@@ -350,7 +351,7 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
   Node new_ret;
   for (unsigned i = 0; i < 2; i++)
   {
-    getConcat(node[i], c[i]);
+    utils::getConcat(node[i], c[i]);
   }
   // ------- equality unification
   bool changed = false;
@@ -392,8 +393,8 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
   if (changed)
   {
     // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y
-    Node s1 = mkConcat(STRING_CONCAT, c[0]);
-    Node s2 = mkConcat(STRING_CONCAT, c[1]);
+    Node s1 = utils::mkConcat(STRING_CONCAT, c[0]);
+    Node s2 = utils::mkConcat(STRING_CONCAT, c[1]);
     new_ret = s1.eqNode(s2);
     node = returnRewrite(node, new_ret, "str-eq-unify");
   }
@@ -462,8 +463,8 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
         }
       }
 
-      Node lhs = mkConcat(STRING_CONCAT, trimmed[i]);
-      Node ss = mkConcat(STRING_CONCAT, trimmed[1 - i]);
+      Node lhs = utils::mkConcat(STRING_CONCAT, trimmed[i]);
+      Node ss = utils::mkConcat(STRING_CONCAT, trimmed[1 - i]);
       if (lhs != node[i] || ss != node[1 - i])
       {
         // e.g.
@@ -700,7 +701,7 @@ Node TheoryStringsRewriter::rewriteConcat(Node node)
   }
   std::sort(node_vec.begin() + lastIdx, node_vec.end());
 
-  retNode = mkConcat( kind::STRING_CONCAT, node_vec );
+  retNode = utils::mkConcat(STRING_CONCAT, node_vec);
   Trace("strings-rewrite-debug")
       << "Strings::rewriteConcat end " << retNode << std::endl;
   return retNode;
@@ -791,8 +792,8 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node)
     else if (!preReStr.empty())
     {
       // this groups consecutive strings a++b ---> ab
-      Node acc =
-          nm->mkNode(STRING_TO_REGEXP, mkConcat(STRING_CONCAT, preReStr));
+      Node acc = nm->mkNode(STRING_TO_REGEXP,
+                            utils::mkConcat(STRING_CONCAT, preReStr));
       cvec.push_back(acc);
       preReStr.clear();
     }
@@ -810,7 +811,7 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node)
     }
   }
   Assert(!cvec.empty());
-  retNode = mkConcat(REGEXP_CONCAT, cvec);
+  retNode = utils::mkConcat(REGEXP_CONCAT, cvec);
   if (retNode != node)
   {
     // handles all cases where consecutive re constants are combined, and cases
@@ -990,7 +991,7 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
       for (unsigned j = l; j < u; j++)
       {
         vec_nodes.push_back(r);
-        n = mkConcat(REGEXP_CONCAT, vec_nodes);
+        n = utils::mkConcat(REGEXP_CONCAT, vec_nodes);
         vec2.push_back(n);
       }
       retNode = nm->mkNode(REGEXP_UNION, vec2);
@@ -1338,12 +1339,12 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
     if( r.getKind()==kind::REGEXP_STAR ){
       for( unsigned dir=0; dir<=1; dir++ ){
         std::vector< Node > mchildren;
-        getConcat( x, mchildren );
+        utils::getConcat(x, mchildren);
         bool success = true;
         while( success ){
           success = false;
           std::vector< Node > children;
-          getConcat( r[0], children );
+          utils::getConcat(r[0], children);
           Node scn = simpleRegexpConsume( mchildren, children, dir );
           if( !scn.isNull() ){
             Trace("regexp-ext-rewrite") << "Regexp star : const conflict : " << node << std::endl;
@@ -1354,7 +1355,9 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
               Trace("regexp-ext-rewrite") << "Regexp star : full consume : " << node << std::endl;
               return NodeManager::currentNM()->mkConst( true );
             }else{
-              retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, mkConcat( kind::STRING_CONCAT, mchildren ), r );
+              retNode = nm->mkNode(STRING_IN_REGEXP,
+                                   utils::mkConcat(STRING_CONCAT, mchildren),
+                                   r);
               success = true;
             }
           }
@@ -1366,9 +1369,9 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
       }
     }else{
       std::vector< Node > children;
-      getConcat( r, children );
+      utils::getConcat(r, children);
       std::vector< Node > mchildren;
-      getConcat( x, mchildren );
+      utils::getConcat(x, mchildren);
       unsigned prevSize = children.size() + mchildren.size();
       Node scn = simpleRegexpConsume( mchildren, children );
       if( !scn.isNull() ){
@@ -1379,7 +1382,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
           // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm),
           // above, we strip components to construct an equivalent membership:
           // (str.++ xi .. xj) in (re.++ rk ... rl).
-          Node xn = mkConcat(kind::STRING_CONCAT, mchildren);
+          Node xn = utils::mkConcat(STRING_CONCAT, mchildren);
           Node emptyStr = nm->mkConst(String(""));
           if( children.empty() ){
             // If we stripped all components on the right, then the left is
@@ -1389,7 +1392,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
           }else{
             // otherwise, construct the updated regular expression
             retNode = nm->mkNode(
-                STRING_IN_REGEXP, xn, mkConcat(REGEXP_CONCAT, children));
+                STRING_IN_REGEXP, xn, utils::mkConcat(REGEXP_CONCAT, children));
           }
           Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> " << retNode << std::endl;
           return returnRewrite(node, retNode, "re-simple-consume");
@@ -1720,7 +1723,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
   }
 
   std::vector<Node> n1;
-  getConcat(node[0], n1);
+  utils::getConcat(node[0], n1);
 
   // definite inclusion
   if (node[1] == zero)
@@ -1732,11 +1735,11 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
       if (curr != zero && !n1.empty())
       {
         childrenr.push_back(nm->mkNode(kind::STRING_SUBSTR,
-                                       mkConcat(kind::STRING_CONCAT, n1),
+                                       utils::mkConcat(STRING_CONCAT, n1),
                                        node[1],
                                        curr));
       }
-      Node ret = mkConcat(kind::STRING_CONCAT, childrenr);
+      Node ret = utils::mkConcat(STRING_CONCAT, childrenr);
       return returnRewrite(node, ret, "ss-len-include");
     }
   }
@@ -1818,7 +1821,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
         if (r == 0)
         {
           Node ret = nm->mkNode(kind::STRING_SUBSTR,
-                                mkConcat(kind::STRING_CONCAT, n1),
+                                utils::mkConcat(STRING_CONCAT, n1),
                                 curr,
                                 node[2]);
           return returnRewrite(node, ret, "ss-strip-start-pt");
@@ -1826,7 +1829,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
         else
         {
           Node ret = nm->mkNode(kind::STRING_SUBSTR,
-                                mkConcat(kind::STRING_CONCAT, n1),
+                                utils::mkConcat(STRING_CONCAT, n1),
                                 node[1],
                                 node[2]);
           return returnRewrite(node, ret, "ss-strip-end-pt");
@@ -1936,7 +1939,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       if (node[0].getKind() == STRING_CONCAT)
       {
         std::vector<Node> nc1;
-        getConcat(node[0], nc1);
+        utils::getConcat(node[0], nc1);
         NodeBuilder<> nb(OR);
         for (const Node& ncc : nc1)
         {
@@ -1968,9 +1971,9 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     }
   }
   std::vector<Node> nc1;
-  getConcat(node[0], nc1);
+  utils::getConcat(node[0], nc1);
   std::vector<Node> nc2;
-  getConcat(node[1], nc2);
+  utils::getConcat(node[1], nc2);
 
   // component-wise containment
   std::vector<Node> nc1rb;
@@ -1987,7 +1990,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
   if (stripConstantEndpoints(nc1, nc2, nb, ne))
   {
     Node ret = NodeManager::currentNM()->mkNode(
-        kind::STRING_STRCTN, mkConcat(kind::STRING_CONCAT, nc1), node[1]);
+        kind::STRING_STRCTN, utils::mkConcat(STRING_CONCAT, nc1), node[1]);
     return returnRewrite(node, ret, "ctn-strip-endpt");
   }
 
@@ -2093,7 +2096,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
           if (s.noOverlapWith(t))
           {
             std::vector<Node> nc0;
-            getConcat(node[0], nc0);
+            utils::getConcat(node[0], nc0);
             std::vector<Node> spl[2];
             spl[0].insert(spl[0].end(), nc0.begin(), nc0.begin() + i);
             Assert(i < nc0.size() - 1);
@@ -2102,11 +2105,11 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
                 kind::OR,
                 NodeManager::currentNM()->mkNode(
                     kind::STRING_STRCTN,
-                    mkConcat(kind::STRING_CONCAT, spl[0]),
+                    utils::mkConcat(STRING_CONCAT, spl[0]),
                     node[1]),
                 NodeManager::currentNM()->mkNode(
                     kind::STRING_STRCTN,
-                    mkConcat(kind::STRING_CONCAT, spl[1]),
+                    utils::mkConcat(STRING_CONCAT, spl[1]),
                     node[1]));
             return returnRewrite(node, ret, "ctn-split");
           }
@@ -2228,7 +2231,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
 
   // evaluation and simple cases
   std::vector<Node> children0;
-  getConcat(node[0], children0);
+  utils::getConcat(node[0], children0);
   if (children0[0].isConst() && node[1].isConst() && node[2].isConst())
   {
     CVC4::Rational rMaxInt(CVC4::String::maxSize());
@@ -2320,7 +2323,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
                                  << fstr << ", " << node[1] << ")" << std::endl;
   Trace("strings-rewrite-debug") << "...got " << cmp_conr << std::endl;
   std::vector<Node> children1;
-  getConcat(node[1], children1);
+  utils::getConcat(node[1], children1);
   if (!cmp_conr.isNull())
   {
     if (cmp_conr.getConst<bool>())
@@ -2335,7 +2338,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
         {
           // For example:
           // str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0)
-          Node nn = mkConcat(kind::STRING_CONCAT, children0);
+          Node nn = utils::mkConcat(STRING_CONCAT, children0);
           Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
           return returnRewrite(node, ret, "idof-def-ctn");
         }
@@ -2348,9 +2351,9 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
           Node ret =
               nm->mkNode(kind::PLUS,
                          nm->mkNode(kind::STRING_LENGTH,
-                                    mkConcat(kind::STRING_CONCAT, nb)),
+                                    utils::mkConcat(STRING_CONCAT, nb)),
                          nm->mkNode(kind::STRING_STRIDOF,
-                                    mkConcat(kind::STRING_CONCAT, children0),
+                                    utils::mkConcat(STRING_CONCAT, children0),
                                     node[1],
                                     node[2]));
           return returnRewrite(node, ret, "idof-strip-cnst-endpts");
@@ -2367,7 +2370,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
         // implies
         // str.indexof( str.++( x1, x2 ), y, z ) --->
         // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
-        Node nn = mkConcat(kind::STRING_CONCAT, children0);
+        Node nn = utils::mkConcat(STRING_CONCAT, children0);
         Node ret =
             nm->mkNode(kind::PLUS,
                        nm->mkNode(kind::MINUS, node[2], new_len),
@@ -2393,15 +2396,15 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
       // For example:
       // str.indexof(str.++("ABCD", x), y, 3) --->
       // str.indexof(str.++("AAAD", x), y, 3)
-      Node nodeNr = mkConcat(kind::STRING_CONCAT, nr);
+      Node nodeNr = utils::mkConcat(STRING_CONCAT, nr);
       Node normNr = lengthPreserveRewrite(nodeNr);
       if (normNr != nodeNr)
       {
         std::vector<Node> normNrChildren;
-        getConcat(normNr, normNrChildren);
+        utils::getConcat(normNr, normNrChildren);
         std::vector<Node> children(normNrChildren);
         children.insert(children.end(), children0.begin(), children0.end());
-        Node nn = mkConcat(kind::STRING_CONCAT, children);
+        Node nn = utils::mkConcat(STRING_CONCAT, children);
         Node res = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
         return returnRewrite(node, res, "idof-norm-prefix");
       }
@@ -2414,7 +2417,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
     std::vector<Node> ce;
     if (stripConstantEndpoints(children0, children1, cb, ce, -1))
     {
-      Node ret = mkConcat(kind::STRING_CONCAT, children0);
+      Node ret = utils::mkConcat(STRING_CONCAT, children0);
       ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]);
       // For example:
       // str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
@@ -2437,7 +2440,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   }
 
   std::vector<Node> children0;
-  getConcat(node[0], children0);
+  utils::getConcat(node[0], children0);
 
   if (node[1].isConst() && children0[0].isConst())
   {
@@ -2462,7 +2465,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       children.push_back(node[2]);
       children.push_back(ns3);
       children.insert(children.end(), children0.begin() + 1, children0.end());
-      Node ret = mkConcat(kind::STRING_CONCAT, children);
+      Node ret = utils::mkConcat(STRING_CONCAT, children);
       return returnRewrite(node, ret, "rpl-const-find");
     }
   }
@@ -2500,7 +2503,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
 
         if (allEmptyEqs)
         {
-          Node nn1 = mkConcat(STRING_CONCAT, emptyNodes);
+          Node nn1 = utils::mkConcat(STRING_CONCAT, emptyNodes);
           if (node[1] != nn1)
           {
             Node ret = nm->mkNode(STRING_STRREPL, node[0], nn1, node[2]);
@@ -2512,7 +2515,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   }
 
   std::vector<Node> children1;
-  getConcat(node[1], children1);
+  utils::getConcat(node[1], children1);
 
   // check if contains definitely does (or does not) hold
   Node cmp_con = nm->mkNode(kind::STRING_STRCTN, node[0], node[1]);
@@ -2536,7 +2539,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
           std::vector<Node> cres;
           cres.push_back(node[2]);
           cres.insert(cres.end(), ce.begin(), ce.end());
-          Node ret = mkConcat(kind::STRING_CONCAT, cres);
+          Node ret = utils::mkConcat(STRING_CONCAT, cres);
           return returnRewrite(node, ret, "rpl-cctn-rpl");
         }
         else if (!ce.empty())
@@ -2549,11 +2552,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
           std::vector<Node> cc;
           cc.push_back(NodeManager::currentNM()->mkNode(
               kind::STRING_STRREPL,
-              mkConcat(kind::STRING_CONCAT, children0),
+              utils::mkConcat(STRING_CONCAT, children0),
               node[1],
               node[2]));
           cc.insert(cc.end(), ce.begin(), ce.end());
-          Node ret = mkConcat(kind::STRING_CONCAT, cc);
+          Node ret = utils::mkConcat(STRING_CONCAT, cc);
           return returnRewrite(node, ret, "rpl-cctn");
         }
       }
@@ -2601,7 +2604,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       if (node[0] == empty && allEmptyEqs)
       {
         std::vector<Node> emptyNodesList(emptyNodes.begin(), emptyNodes.end());
-        Node nn1 = mkConcat(STRING_CONCAT, emptyNodesList);
+        Node nn1 = utils::mkConcat(STRING_CONCAT, emptyNodesList);
         if (nn1 != node[1] || nn2 != node[2])
         {
           Node res = nm->mkNode(kind::STRING_STRREPL, node[0], nn1, nn2);
@@ -2633,18 +2636,18 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
         cc.insert(cc.end(), cb.begin(), cb.end());
         cc.push_back(NodeManager::currentNM()->mkNode(
             kind::STRING_STRREPL,
-            mkConcat(kind::STRING_CONCAT, children0),
+            utils::mkConcat(STRING_CONCAT, children0),
             node[1],
             node[2]));
         cc.insert(cc.end(), ce.begin(), ce.end());
-        Node ret = mkConcat(kind::STRING_CONCAT, cc);
+        Node ret = utils::mkConcat(STRING_CONCAT, cc);
         return returnRewrite(node, ret, "rpl-pull-endpt");
       }
     }
   }
 
   children1.clear();
-  getConcat(node[1], children1);
+  utils::getConcat(node[1], children1);
   Node lastChild1 = children1[children1.size() - 1];
   if (lastChild1.getKind() == kind::STRING_SUBSTR)
   {
@@ -2660,7 +2663,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     children1.pop_back();
     // Length of the non-substr components in the second argument
     Node partLen1 = nm->mkNode(kind::STRING_LENGTH,
-                               mkConcat(kind::STRING_CONCAT, children1));
+                               utils::mkConcat(STRING_CONCAT, children1));
     Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]);
 
     Node zero = nm->mkConst(Rational(0));
@@ -2678,7 +2681,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
               kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1))));
       Node res = nm->mkNode(kind::STRING_STRREPL,
                             node[0],
-                            mkConcat(kind::STRING_CONCAT, children1),
+                            utils::mkConcat(STRING_CONCAT, children1),
                             node[2]);
       return returnRewrite(node, res, "repl-subst-idx");
     }
@@ -2864,7 +2867,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       std::vector<Node> checkLhs;
       checkLhs.insert(
           checkLhs.end(), children0.begin(), children0.begin() + checkIndex);
-      Node lhs = mkConcat(STRING_CONCAT, checkLhs);
+      Node lhs = utils::mkConcat(STRING_CONCAT, checkLhs);
       Node rhs = children0[checkIndex];
       Node ctn = checkEntailContains(lhs, rhs);
       if (!ctn.isNull() && ctn.getConst<bool>())
@@ -2881,7 +2884,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     {
       std::vector<Node> remc(children0.begin() + lastCheckIndex,
                              children0.end());
-      Node rem = mkConcat(STRING_CONCAT, remc);
+      Node rem = utils::mkConcat(STRING_CONCAT, remc);
       Node ret =
           nm->mkNode(STRING_CONCAT,
                      nm->mkNode(STRING_STRREPL, lastLhs, node[1], node[2]),
@@ -2940,7 +2943,7 @@ Node TheoryStringsRewriter::rewriteReplaceAll(Node node)
       }
     } while (curr != std::string::npos && curr < s.size());
     // constant evaluation
-    Node res = mkConcat(STRING_CONCAT, children);
+    Node res = utils::mkConcat(STRING_CONCAT, children);
     return returnRewrite(node, res, "replall-const");
   }
 
@@ -3066,9 +3069,9 @@ Node TheoryStringsRewriter::rewriteStringLeq(Node n)
   }
 
   std::vector<Node> n1;
-  getConcat(n[0], n1);
+  utils::getConcat(n[0], n1);
   std::vector<Node> n2;
-  getConcat(n[1], n2);
+  utils::getConcat(n[1], n2);
   Assert(!n1.empty() && !n2.empty());
 
   // constant prefixes
@@ -3194,21 +3197,6 @@ Node TheoryStringsRewriter::rewriteStringCode(Node n)
   return n;
 }
 
-void TheoryStringsRewriter::getConcat( Node n, std::vector< Node >& c ) {
-  if( n.getKind()==kind::STRING_CONCAT || n.getKind()==kind::REGEXP_CONCAT ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      c.push_back( n[i] );
-    }
-  }else{
-    c.push_back( n );
-  }
-}
-
-Node TheoryStringsRewriter::mkConcat( Kind k, std::vector< Node >& c ){
-  Assert( !c.empty() || k==kind::STRING_CONCAT );
-  return c.size()>1 ? NodeManager::currentNM()->mkNode( k, c ) : ( c.size()==1 ? c[0] : NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
-}
-
 Node TheoryStringsRewriter::splitConstant( Node a, Node b, int& index, bool isRev ) {
   Assert( a.isConst() && b.isConst() );
   index = a.getConst<String>().size() <= b.getConst<String>().size() ? 1 : 0;
@@ -3314,7 +3302,7 @@ Node TheoryStringsRewriter::collectConstantStringAt( std::vector< Node >& vec, u
     if( isRev ){
       std::reverse( c.begin(), c.end() );
     }
-    Node cc = Rewriter::rewrite( mkConcat( kind::STRING_CONCAT, c ) );
+    Node cc = Rewriter::rewrite(utils::mkConcat(STRING_CONCAT, c));
     Assert( cc.isConst() );
     return cc;
   }else{
@@ -3909,7 +3897,7 @@ Node TheoryStringsRewriter::canonicalStrForSymbolicLength(Node len)
         return Node::null();
       }
       std::vector<Node> snChildren;
-      getConcat(sn, snChildren);
+      utils::getConcat(sn, snChildren);
       concatBuilder.append(snChildren);
     }
     res = concatBuilder.constructNode();
@@ -3924,7 +3912,7 @@ Node TheoryStringsRewriter::canonicalStrForSymbolicLength(Node len)
 
     Node nRep = canonicalStrForSymbolicLength(len[1]);
     std::vector<Node> nRepChildren;
-    getConcat(nRep, nRepChildren);
+    utils::getConcat(nRep, nRepChildren);
     NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
     for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++)
     {
@@ -4526,9 +4514,9 @@ bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b)
   NodeManager* nm = NodeManager::currentNM();
 
   std::vector<Node> avec;
-  getConcat(getMultisetApproximation(a), avec);
+  utils::getConcat(getMultisetApproximation(a), avec);
   std::vector<Node> bvec;
-  getConcat(b, bvec);
+  utils::getConcat(b, bvec);
 
   std::map<Node, unsigned> num_nconst[2];
   std::map<Node, unsigned> num_const[2];
@@ -4612,7 +4600,7 @@ Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a)
   NodeManager* nm = NodeManager::currentNM();
 
   std::vector<Node> avec;
-  getConcat(getMultisetApproximation(a), avec);
+  utils::getConcat(getMultisetApproximation(a), avec);
 
   bool cValid = false;
   unsigned c = 0;
@@ -5189,7 +5177,7 @@ Node TheoryStringsRewriter::inferEqsFromContains(Node x, Node y)
   // (= x (str.++ y1' ... ym'))
   if (!cs.empty())
   {
-    nb << nm->mkNode(EQUAL, x, mkConcat(STRING_CONCAT, cs));
+    nb << nm->mkNode(EQUAL, x, utils::mkConcat(STRING_CONCAT, cs));
   }
   // (= y1'' "") ... (= yk'' "")
   for (const Node& zeroLen : zeroLens)

diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index ee92828dec33a7c8fd4f3f5780b3cf0a48ce141d..b19d49e6740d0fa4461381ca0fcea03b603c4572 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -252,16 +252,6 @@ class TheoryStringsRewriter {
    */
   static Node rewriteStringCode(Node node);
 
-  /** gets the "vector form" of term n, adds it to c.
-  * For example:
-  * when n = str.++( x, y ), c is { x, y }
-  * when n = str.++( x, str.++( y, z ), w ), c is { x, str.++( y, z ), w )
-  * when n = x, c is { x }
-  *
-  * Also applies to regular expressions (re.++ above).
-  */
-  static void getConcat( Node n, std::vector< Node >& c );
-  static Node mkConcat( Kind k, std::vector< Node >& c );
   static Node splitConstant( Node a, Node b, int& index, bool isRev );
   /** can constant contain list
    * return true if constant c can contain the list l in order

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 42a8af5a11b5218e1afdf87cc142c4bc6f776754..bb2054b0e43eb20e4f00b5ac3f84db5cac991d0e 100644 (file)
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -44,6 +44,30 @@ Node mkAnd(std::vector<Node>& a)
   return NodeManager::currentNM()->mkNode(AND, au);
 }
 
+void getConcat(Node n, std::vector<Node>& c)
+{
+  Kind k = n.getKind();
+  if (k == STRING_CONCAT || k == REGEXP_CONCAT)
+  {
+    for (const Node& nc : n)
+    {
+      c.push_back(nc);
+    }
+  }
+  else
+  {
+    c.push_back(n);
+  }
+}
+
+Node mkConcat(Kind k, std::vector<Node>& c)
+{
+  Assert(!c.empty() || k == STRING_CONCAT);
+  NodeManager* nm = NodeManager::currentNM();
+  return c.size() > 1 ? nm->mkNode(k, c)
+                      : (c.size() == 1 ? c[0] : nm->mkConst(String("")));
+}
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory

diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 9e0779e169a0d7ca798b62b53147c746d8ccd4c0..296f4e46e4893dc766e3f36ab581be95249e4220 100644 (file)
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -34,6 +34,24 @@ namespace utils {
  */
 Node mkAnd(std::vector<Node>& a);
 
+/**
+ * Gets the "vector form" of term n, adds it to c.
+ *
+ * For example:
+ * when n = str.++( x, y ), c is { x, y }
+ * when n = str.++( x, str.++( y, z ), w ), c is { x, str.++( y, z ), w )
+ * when n = x, c is { x }
+ *
+ * Also applies to regular expressions (re.++ above).
+ */
+void getConcat(Node n, std::vector<Node>& c);
+
+/**
+ * Make the concatentation from vector c
+ * The kind k is either STRING_CONCAT or REGEXP_CONCAT.
+ */
+Node mkConcat(Kind k, std::vector<Node>& c);
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory