From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 07:34:33 +0000 (-0500)
Subject: Convert more cases of strings to words (#4206)
X-Git-Tag: cvc5-1.0.0~3367
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f3a0445fe772360d8a2da3069a5f082c031d7f8;p=cvc5.git

Convert more cases of strings to words (#4206)
---

diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index fdc8120ff..dfbbdfebf 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -97,8 +97,8 @@ Node SygusUnif::constructBestConditional(Node ce,
 
 Node SygusUnif::constructBestStringToConcat(
     const std::vector<Node>& strs,
-    const std::map<Node, unsigned>& total_inc,
-    const std::map<Node, std::vector<unsigned>>& incr)
+    const std::map<Node, size_t>& total_inc,
+    const std::map<Node, std::vector<size_t>>& incr)
 {
   Assert(!strs.empty());
   std::vector<Node> strs_tmp = strs;
@@ -106,7 +106,7 @@ Node SygusUnif::constructBestStringToConcat(
   // prefer one that has incremented by more than 0
   for (const Node& ns : strs_tmp)
   {
-    const std::map<Node, unsigned>::const_iterator iti = total_inc.find(ns);
+    const std::map<Node, size_t>::const_iterator iti = total_inc.find(ns);
     if (iti != total_inc.end() && iti->second > 0)
     {
       return ns;
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 185a927df..f6e85abcd 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -182,8 +182,8 @@ class SygusUnif
   */
   virtual Node constructBestStringToConcat(
       const std::vector<Node>& strs,
-      const std::map<Node, unsigned>& total_inc,
-      const std::map<Node, std::vector<unsigned> >& incr);
+      const std::map<Node, size_t>& total_inc,
+      const std::map<Node, std::vector<size_t>>& incr);
   //------------------------------ end constructing solutions
   /** map terms to their sygus size */
   std::map<Node, unsigned> d_termToSize;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index dc21107b1..1fc7903fa 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/strings/word.h"
 #include "util/random.h"
 
 #include <math.h>
@@ -65,7 +66,7 @@ bool UnifContextIo::updateContext(SygusUnifIo* sui,
 }
 
 bool UnifContextIo::updateStringPosition(SygusUnifIo* sui,
-                                         std::vector<unsigned>& pos,
+                                         std::vector<size_t>& pos,
                                          NodeRole nrole)
 {
   Assert(pos.size() == d_str_pos.size());
@@ -106,7 +107,7 @@ void UnifContextIo::initialize(SygusUnifIo* sui)
     // output type of the examples
     TypeNode exotn = sui->d_examples_out[0].getType();
 
-    if (exotn.isString())
+    if (exotn.isStringLike())
     {
       for (unsigned i = 0; i < sz; i++)
       {
@@ -119,10 +120,10 @@ void UnifContextIo::initialize(SygusUnifIo* sui)
 
 void UnifContextIo::getCurrentStrings(SygusUnifIo* sui,
                                       const std::vector<Node>& vals,
-                                      std::vector<String>& ex_vals)
+                                      std::vector<Node>& ex_vals)
 {
   bool isPrefix = d_curr_role == role_string_prefix;
-  String dummy;
+  Node dummy;
   for (unsigned i = 0; i < vals.size(); i++)
   {
     if (d_vals[i] == sui->d_true)
@@ -132,14 +133,16 @@ void UnifContextIo::getCurrentStrings(SygusUnifIo* sui,
       if (pos_value > 0)
       {
         Assert(d_curr_role != role_invalid);
-        String s = vals[i].getConst<String>();
-        Assert(pos_value <= s.size());
-        ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value)
-                                   : s.prefix(s.size() - pos_value));
+        Node s = vals[i];
+        size_t sSize = strings::Word::getLength(s);
+        Assert(pos_value <= sSize);
+        ex_vals.push_back(isPrefix
+                              ? strings::Word::suffix(s, sSize - pos_value)
+                              : strings::Word::prefix(s, sSize - pos_value));
       }
       else
       {
-        ex_vals.push_back(vals[i].getConst<String>());
+        ex_vals.push_back(vals[i]);
       }
     }
     else
@@ -152,14 +155,14 @@ void UnifContextIo::getCurrentStrings(SygusUnifIo* sui,
 
 bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
                                        bool isPrefix,
-                                       const std::vector<String>& ex_vals,
+                                       const std::vector<Node>& ex_vals,
                                        const std::vector<Node>& vals,
-                                       std::vector<unsigned>& inc,
-                                       unsigned& tot)
+                                       std::vector<size_t>& inc,
+                                       size_t& tot)
 {
   for (unsigned j = 0; j < vals.size(); j++)
   {
-    unsigned ival = 0;
+    size_t ival = 0;
     if (d_vals[j] == sui->d_true)
     {
       // example is active in this context
@@ -169,12 +172,12 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
         // position
         return false;
       }
-      String mystr = vals[j].getConst<String>();
-      ival = mystr.size();
-      if (mystr.size() <= ex_vals[j].size())
+      ival = strings::Word::getLength(vals[j]);
+      size_t exjLen = strings::Word::getLength(ex_vals[j]);
+      if (ival <= exjLen)
       {
-        if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival)
-                       : ex_vals[j].rstrncmp(mystr, ival)))
+        if (!(isPrefix ? strings::Word::strncmp(ex_vals[j], vals[j], ival)
+                       : strings::Word::rstrncmp(ex_vals[j], vals[j], ival)))
         {
           Trace("sygus-sui-dt-debug") << "X";
           return false;
@@ -198,7 +201,7 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
   return true;
 }
 bool UnifContextIo::isStringSolved(SygusUnifIo* sui,
-                                   const std::vector<String>& ex_vals,
+                                   const std::vector<Node>& ex_vals,
                                    const std::vector<Node>& vals)
 {
   for (unsigned j = 0; j < vals.size(); j++)
@@ -211,8 +214,7 @@ bool UnifContextIo::isStringSolved(SygusUnifIo* sui,
         // value is unknown, thus it does not solve
         return false;
       }
-      String mystr = vals[j].getConst<String>();
-      if (ex_vals[j] != mystr)
+      if (ex_vals[j] != vals[j])
       {
         return false;
       }
@@ -889,7 +891,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
 bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
 {
   TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
-  if (xbt.isString())
+  if (xbt.isStringLike())
   {
     std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
     if (itx != d_use_str_contains_eexc.end())
@@ -1091,7 +1093,7 @@ Node SygusUnifIo::constructSol(
     }
     if (ret_dt.isNull())
     {
-      if (d_tds->sygusToBuiltinType(e.getType()).isString())
+      if (d_tds->sygusToBuiltinType(e.getType()).isStringLike())
       {
         // check if a current value that closes all examples
         // get the term enumerator for this type
@@ -1103,7 +1105,7 @@ Node SygusUnifIo::constructSol(
 
           EnumCache& ecachet = d_ecache[et];
           // get the current examples
-          std::vector<String> ex_vals;
+          std::vector<Node> ex_vals;
           x.getCurrentStrings(this, d_examples_out, ex_vals);
           Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 
@@ -1213,12 +1215,12 @@ Node SygusUnifIo::constructSol(
     // check if each return value is a prefix/suffix of all open examples
     if (!retValMod || x.getCurrentRole() == nrole)
     {
-      std::map<Node, std::vector<unsigned> > incr;
+      std::map<Node, std::vector<size_t>> incr;
       bool isPrefix = nrole == role_string_prefix;
-      std::map<Node, unsigned> total_inc;
+      std::map<Node, size_t> total_inc;
       std::vector<Node> inc_strs;
       // make the value of the examples
-      std::vector<String> ex_vals;
+      std::vector<Node> ex_vals;
       x.getCurrentStrings(this, d_examples_out, ex_vals);
       if (Trace.isOn("sygus-sui-dt-debug"))
       {
@@ -1244,7 +1246,7 @@ Node SygusUnifIo::constructSol(
         TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t);
         Trace("sygus-sui-dt-debug") << " : ";
         Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
-        unsigned tot = 0;
+        size_t tot = 0;
         bool exsuccess = x.getStringIncrement(this,
                                               isPrefix,
                                               ex_vals,
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index da08044bf..06197ce66 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -83,7 +83,7 @@ class UnifContextIo : public UnifContext
   * role to nrole.
   */
   bool updateStringPosition(SygusUnifIo* sui,
-                            std::vector<unsigned>& pos,
+                            std::vector<size_t>& pos,
                             NodeRole nrole);
   /** get current strings
   *
@@ -94,7 +94,7 @@ class UnifContextIo : public UnifContext
   */
   void getCurrentStrings(SygusUnifIo* sui,
                          const std::vector<Node>& vals,
-                         std::vector<String>& ex_vals);
+                         std::vector<Node>& ex_vals);
   /** get string increment
   *
   * If this method returns true, then inc and tot are updated such that
@@ -107,13 +107,13 @@ class UnifContextIo : public UnifContext
   */
   bool getStringIncrement(SygusUnifIo* sui,
                           bool isPrefix,
-                          const std::vector<String>& ex_vals,
+                          const std::vector<Node>& ex_vals,
                           const std::vector<Node>& vals,
-                          std::vector<unsigned>& inc,
-                          unsigned& tot);
+                          std::vector<size_t>& inc,
+                          size_t& tot);
   /** returns true if ex_vals[i] = vals[i] for all active indices i. */
   bool isStringSolved(SygusUnifIo* sui,
-                      const std::vector<String>& ex_vals,
+                      const std::vector<Node>& ex_vals,
                       const std::vector<Node>& vals);
   //----------end for CONCAT strategies
 
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 088bc4a16..d19ce538d 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -50,7 +50,6 @@ InferenceManager::InferenceManager(TheoryStrings& p,
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
   d_one = nm->mkConst(Rational(1));
-  d_emptyString = nm->mkConst(::CVC4::String(""));
   d_true = nm->mkConst(true);
   d_false = nm->mkConst(false);
 }
@@ -453,7 +452,8 @@ Node InferenceManager::getRegisterTermAtomicLemma(
 
   if (s == LENGTH_GEQ_ONE)
   {
-    Node neq_empty = n.eqNode(d_emptyString).negate();
+    Node emp = Word::mkEmptyWord(n.getType());
+    Node neq_empty = n.eqNode(emp).negate();
     Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
     Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
     Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
@@ -472,10 +472,11 @@ Node InferenceManager::getRegisterTermAtomicLemma(
   }
   Assert(s == LENGTH_SPLIT);
 
+  Node emp = Word::mkEmptyWord(n.getType());
   std::vector<Node> lems;
   // split whether the string is empty
   Node n_len_eq_z = n_len.eqNode(d_zero);
-  Node n_len_eq_z_2 = n.eqNode(d_emptyString);
+  Node n_len_eq_z_2 = n.eqNode(emp);
   Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
   case_empty = Rewriter::rewrite(case_empty);
   Node case_nempty = nm->mkNode(GT, n_len, d_zero);
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index af1f28a23..60139ca83 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -356,7 +356,6 @@ class InferenceManager
   SequencesStatistics& d_statistics;
 
   /** Common constants */
-  Node d_emptyString;
   Node d_true;
   Node d_false;
   Node d_zero;
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 0520ec88a..0d6b6c7fe 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -288,7 +288,9 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
   if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) {
     retNode = d_deriv_cache[dv].first;
     ret = d_deriv_cache[dv].second;
-  } else if( c.isEmptyString() ) {
+  }
+  else if (c.empty())
+  {
     Node expNode;
     ret = delta( r, expNode );
     if(ret == 0) {
@@ -536,7 +538,9 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
   NodeManager* nm = NodeManager::currentNM();
   if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
     retNode = d_dv_cache[dv];
-  } else if( c.isEmptyString() ){
+  }
+  else if (c.empty())
+  {
     Node exp;
     int tmp = delta( r, exp );
     if(tmp == 0) {
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 35c52646d..540a10a9e 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -600,7 +600,7 @@ bool RegExpSolver::deriveRegExp(Node x,
   Trace("regexp-derive") << "RegExpSolver::deriveRegExp: x=" << x
                          << ", r= " << r << std::endl;
   CVC4::String s = getHeadConst(x);
-  if (!s.isEmptyString() && d_regexp_opr.checkConstRegExp(r))
+  if (!s.empty() && d_regexp_opr.checkConstRegExp(r))
   {
     Node conc = Node::null();
     Node dc = r;
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 152f71019..d8b8765eb 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -99,20 +99,22 @@ Node SequencesRewriter::rewriteEquality(Node node)
     {
       unsigned index1 = r == 0 ? i : (c[0].size() - 1) - i;
       unsigned index2 = r == 0 ? i : (c[1].size() - 1) - i;
-      if (c[0][index1].isConst() && c[1][index2].isConst())
+      Node s = c[0][index1];
+      Node t = c[1][index2];
+      if (s.isConst() && t.isConst())
       {
-        CVC4::String s = c[0][index1].getConst<String>();
-        CVC4::String t = c[1][index2].getConst<String>();
-        unsigned len_short = s.size() <= t.size() ? s.size() : t.size();
-        bool isSameFix =
-            r == 1 ? s.rstrncmp(t, len_short) : s.strncmp(t, len_short);
+        size_t lenS = Word::getLength(s);
+        size_t lenT = Word::getLength(t);
+        size_t lenShort = lenS <= lenT ? lenS : lenT;
+        bool isSameFix = r == 1 ? Word::rstrncmp(s, t, lenShort)
+                                : Word::strncmp(s, t, lenShort);
         if (!isSameFix)
         {
           Node ret = NodeManager::currentNM()->mkConst(false);
           return returnRewrite(node, ret, Rewrite::EQ_NFIX);
         }
       }
-      if (c[0][index1] != c[1][index2])
+      if (s != t)
       {
         break;
       }
@@ -280,7 +282,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
   }
 
   // ------- rewrites for (= "" _)
-  Node empty = nm->mkConst(::CVC4::String(""));
+  Node empty = Word::mkEmptyWord(stype);
   for (size_t i = 0; i < 2; i++)
   {
     if (node[i] == empty)
@@ -585,7 +587,6 @@ Node SequencesRewriter::rewriteConcat(Node node)
   Assert(node.getKind() == kind::STRING_CONCAT);
   Trace("strings-rewrite-debug")
       << "Strings::rewriteConcat start " << node << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> node_vec;
   Node preNode = Node::null();
   for (Node tmpNode : node)
@@ -598,8 +599,10 @@ Node SequencesRewriter::rewriteConcat(Node node)
       {
         if (tmpNode[0].isConst())
         {
-          preNode = nm->mkConst(
-              preNode.getConst<String>().concat(tmpNode[0].getConst<String>()));
+          std::vector<Node> wvec;
+          wvec.push_back(preNode);
+          wvec.push_back(tmpNode[0]);
+          preNode = Word::mkWord(wvec);
           node_vec.push_back(preNode);
         }
         else
@@ -1114,14 +1117,14 @@ Node SequencesRewriter::rewriteMembership(TNode node)
   {
     if (x.isConst())
     {
-      String s = x.getConst<String>();
-      if (s.size() == 0)
+      size_t xlen = Word::getLength(x);
+      if (xlen == 0)
       {
         Node retNode = nm->mkConst(true);
         // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
         return returnRewrite(node, retNode, Rewrite::RE_EMPTY_IN_STR_STAR);
       }
-      else if (s.size() == 1)
+      else if (xlen == 1)
       {
         if (r[0].getKind() == STRING_TO_REGEXP)
         {
@@ -1317,7 +1320,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
       // above, we strip components to construct an equivalent membership:
       // (str.++ xi .. xj) in (re.++ rk ... rl).
       Node xn = utils::mkConcat(mchildren, stype);
-      Node emptyStr = nm->mkConst(String(""));
+      Node emptyStr = Word::mkEmptyWord(stype);
       if (children.empty())
       {
         // If we stripped all components on the right, then the left is
@@ -1913,7 +1916,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         Node ret;
         if (nc2.size() > 1)
         {
-          Node emp = nm->mkConst(CVC4::String(""));
+          Node emp = Word::mkEmptyWord(stype);
           NodeBuilder<> nb2(kind::AND);
           for (const Node& n2 : nc2)
           {
@@ -1969,7 +1972,7 @@ Node SequencesRewriter::rewriteContains(Node node)
   {
     if (node[1].isConst())
     {
-      CVC4::String t = node[1].getConst<String>();
+      Node t = node[1];
       // Below, we are looking for a constant component of node[0]
       // has no overlap with node[1], which means we can split.
       // Notice that if the first or last components had no
@@ -1981,9 +1984,8 @@ Node SequencesRewriter::rewriteContains(Node node)
         // constant contains
         if (node[0][i].isConst())
         {
-          CVC4::String s = node[0][i].getConst<String>();
           // if no overlap, we can split into disjunction
-          if (s.noOverlapWith(t))
+          if (Word::noOverlapWith(node[0][i], node[1]))
           {
             std::vector<Node> nc0;
             utils::getConcat(node[0], nc0);
@@ -2067,7 +2069,7 @@ Node SequencesRewriter::rewriteContains(Node node)
       Node ctn = d_stringsEntail.checkContains(node[1], node[0][2]);
       if (!ctn.isNull() && !ctn.getConst<bool>())
       {
-        Node empty = nm->mkConst(String(""));
+        Node empty = Word::mkEmptyWord(stype);
         Node ret = nm->mkNode(
             kind::STRING_STRCTN,
             nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
@@ -2093,7 +2095,7 @@ Node SequencesRewriter::rewriteContains(Node node)
     // Note: Length-based reasoning is not sufficient to get this rewrite. We
     // can neither show that str.len(str.replace("", x, y)) - str.len(x) >= 0
     // nor str.len(x) - str.len(str.replace("", x, y)) >= 0
-    Node emp = nm->mkConst(CVC4::String(""));
+    Node emp = Word::mkEmptyWord(stype);
     if (node[0] == node[1][1] && node[1][0] == emp)
     {
       Node ret = nm->mkNode(kind::EQUAL, emp, node[1]);
@@ -2169,7 +2171,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       Node negone = nm->mkConst(Rational(-1));
       return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
     }
-    Node emp = nm->mkConst(CVC4::String(""));
+    Node emp = Word::mkEmptyWord(stype);
     if (node[0] != emp)
     {
       // indexof( x, x, z ) ---> indexof( "", "", z )
@@ -2390,7 +2392,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
     // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "")
     if (StringsEntail::checkLengthOne(node[0]))
     {
-      Node empty = nm->mkConst(String(""));
+      Node empty = Word::mkEmptyWord(stype);
       Node rn1 = Rewriter::rewrite(
           rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty)));
       if (rn1 != node[1])
@@ -2480,7 +2482,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
     // substitute y with "" in the third argument. Note that the third argument
     // does not matter when the str.replace does not apply.
     //
-    Node empty = nm->mkConst(::CVC4::String(""));
+    Node empty = Word::mkEmptyWord(stype);
 
     std::vector<Node> emptyNodes;
     bool allEmptyEqs;
@@ -2890,9 +2892,8 @@ Node SequencesRewriter::rewriteStrReverse(Node node)
   Node x = node[0];
   if (x.isConst())
   {
-    std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
-    std::reverse(nvec.begin(), nvec.end());
-    Node retNode = nm->mkConst(String(nvec));
+    // reverse the characters in the constant
+    Node retNode = Word::reverse(x);
     return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
   }
   else if (x.getKind() == STRING_CONCAT)
@@ -2928,8 +2929,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   }
   if (n[0].isConst())
   {
-    CVC4::String t = n[0].getConst<String>();
-    if (t.isEmptyString())
+    if (Word::isEmpty(n[0]))
     {
       Node ret = NodeManager::currentNM()->mkConst(true);
       return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST);
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 99219af82..097964672 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -857,7 +857,6 @@ Node StringsEntail::getMultisetApproximation(Node a)
 
 Node StringsEntail::getStringOrEmpty(Node n)
 {
-  NodeManager* nm = NodeManager::currentNM();
   Node res;
   while (res.isNull())
   {
@@ -865,15 +864,14 @@ Node StringsEntail::getStringOrEmpty(Node n)
     {
       case STRING_STRREPL:
       {
-        Node empty = nm->mkConst(::CVC4::String(""));
-        if (n[0] == empty)
+        if (Word::isEmpty(n[0]))
         {
           // (str.replace "" x y) --> y
           n = n[2];
           break;
         }
 
-        if (checkLengthOne(n[0]) && n[2] == empty)
+        if (checkLengthOne(n[0]) && Word::isEmpty(n[2]))
         {
           // (str.replace "A" x "") --> "A"
           res = n[0];
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index f27a19065..bd749576e 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -233,7 +233,7 @@ Node StringsRewriter::rewriteStringLeq(Node n)
   // empty strings
   for (unsigned i = 0; i < 2; i++)
   {
-    if (n[i].isConst() && n[i].getConst<String>().isEmptyString())
+    if (n[i].isConst() && n[i].getConst<String>().empty())
     {
       Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
       return returnRewrite(n, ret, Rewrite::STR_LEQ_EMPTY);
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 5fc13f023..939146a3d 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -368,7 +368,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
 
     // y = ""
-    Node cond1 = y.eqNode(nm->mkConst(CVC4::String("")));
+    Node emp = Word::mkEmptyWord(tn);
+    Node cond1 = y.eqNode(emp);
     // rpw = str.++( z, x )
     Node c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x));
 
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index 085078dea..e9ab2652e 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -283,7 +283,7 @@ std::size_t Word::roverlap(TNode x, TNode y)
   return 0;
 }
 
-Node Word::splitConstant(Node x, Node y, size_t& index, bool isRev)
+Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
 {
   Assert(x.isConst() && y.isConst());
   size_t lenA = getLength(x);
@@ -308,6 +308,21 @@ Node Word::splitConstant(Node x, Node y, size_t& index, bool isRev)
   return Node::null();
 }
 
+Node Word::reverse(TNode x)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Kind k = x.getKind();
+  if (k == CONST_STRING)
+  {
+    String sx = x.getConst<String>();
+    std::vector<unsigned> nvec = sx.getVec();
+    std::reverse(nvec.begin(), nvec.end());
+    return nm->mkConst(String(nvec));
+  }
+  Unimplemented();
+  return Node::null();
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h
index 454710c98..b84ea6874 100644
--- a/src/theory/strings/word.h
+++ b/src/theory/strings/word.h
@@ -151,7 +151,12 @@ class Word
    * If a and b do not share a common prefix (resp. suffix), then this method
    * returns the null node.
    */
-  static Node splitConstant(Node a, Node b, size_t& index, bool isRev);
+  static Node splitConstant(TNode x, TNode y, size_t& index, bool isRev);
+  /** reverse
+   *
+   * Return the result of reversing x.
+   */
+  static Node reverse(TNode x);
 };
 
 // ------------------------------ end for words (string or sequence constants)
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 21862a251..e5e6e392e 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -17,6 +17,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -448,7 +449,7 @@ bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg)
   if ((arg == 1 && k == STRING_STRCTN) || (arg == 0 && k == STRING_SUBSTR))
   {
     // empty string
-    if (n.getConst<String>().size() == 0)
+    if (strings::Word::getLength(n) == 0)
     {
       return true;
     }
diff --git a/src/util/string.h b/src/util/string.h
index 032105812..637ffe365 100644
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -117,8 +117,6 @@ class CVC4_PUBLIC String {
   std::string toString(bool useEscSequences = false) const;
   /** is this the empty string? */
   bool empty() const { return d_str.empty(); }
-  /** is this the empty string? */
-  bool isEmptyString() const { return empty(); }
   /** is less than or equal to string y */
   bool isLeq(const String& y) const;
   /** Return the length of the string */