From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 6 Mar 2018 02:36:17 +0000 (-0600)
Subject: Update semantics for string indexof and replace (#1630)
X-Git-Tag: cvc5-1.0.0~5250
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e2d714a0839fb80d9a40e9b6fdd8a6fe325a1664;p=cvc5.git

Update semantics for string indexof and replace (#1630)
---

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 6f533bfe0..b8185e9c8 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -843,7 +843,7 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
               Node pbv_e = its->second.evaluate(bvr, pt_index);
               Assert(bv_e != pbv_e);
               Trace("sygus-rr-debug") << "; unsound: where they evaluate to "
-                                      << pbv_e << " and " << bv_e << std::endl;
+                                      << bv_e << " and " << pbv_e << std::endl;
             }
             else
             {
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1a61cb449..d412eaa33 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -72,6 +72,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   unsigned prev_new_nodes = new_nodes.size();
   Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl;
   Node retNode = t;
+  NodeManager *nm = NodeManager::currentNM();
 
   if( t.getKind() == kind::STRING_SUBSTR ) {
     Node skt;
@@ -105,52 +106,87 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node lemma = NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 );
     new_nodes.push_back( lemma );
     retNode = skt;
-  } else if( t.getKind() == kind::STRING_STRIDOF ) {
-    Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
-    Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
-    Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
+  }
+  else if (t.getKind() == kind::STRING_STRIDOF)
+  {
+    // processing term:  indexof( x, y, n )
+
     Node skk;
     if( options::stringUfReduct() ){
       skk = getUfAppForNode( kind::STRING_STRIDOF, t );
     }else{
-      skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
+      skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof");
     }
-    Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) );
-    //TODO: simplify this (only applies when idof != -1)
-    Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) );
-    new_nodes.push_back( eq );
-    
-    //learn range of idof?
-    Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
-    Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone );
+
+    Node negone = nm->mkConst(::CVC4::Rational(-1));
+    Node krange = nm->mkNode(kind::GEQ, skk, negone);
+    // assert:   indexof( x, y, n ) >= -1
     new_nodes.push_back( krange );
-    krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk);
+    krange = nm->mkNode(kind::GEQ, nm->mkNode(kind::STRING_LENGTH, t[0]), skk);
+    // assert:   len( x ) >= indexof( x, y, z )
     new_nodes.push_back( krange );
 
-    // s2 = ""
-    Node c1 = t[1].eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
-    //~contain(t234, s2)
-    Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, st, t[1] ).negate();
-    //left
-    Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3 );
-    //t3 = s2
-    Node c4 = t[1].eqNode( sk3 );
-    //~contain(t2, s2)
-    Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
-                NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
-                  NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, t[1], d_zero,
-                    NodeManager::currentNM()->mkNode(kind::MINUS,
-                      NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]),
-                      NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
-                t[1] ).negate();
-    //k=str.len(s2)
-    Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, t[2],
-                            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 )) );
-    //right
-    Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, c1.negate() );
-    Node cond = skk.eqNode( negone );
-    Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
+    // substr( x, n, len( x ) - n )
+    Node st = nm->mkNode(
+        kind::STRING_SUBSTR,
+        t[0],
+        t[2],
+        nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, t[0]), t[2]));
+    Node io2 = nm->mkSkolem("io2", nm->stringType(), "created for indexof");
+    Node io4 = nm->mkSkolem("io4", nm->stringType(), "created for indexof");
+
+    // ~contains( substr( x, n, len( x ) - n ), y )
+    Node c11 = nm->mkNode(kind::STRING_STRCTN, st, t[1]).negate();
+    // n > len( x )
+    Node c12 =
+        nm->mkNode(kind::GT, t[2], nm->mkNode(kind::STRING_LENGTH, t[0]));
+    // 0 > n
+    Node c13 = nm->mkNode(kind::GT, d_zero, t[2]);
+    Node cond1 = nm->mkNode(kind::OR, c11, c12, c13);
+    // skk = -1
+    Node cc1 = skk.eqNode(negone);
+
+    // y = ""
+    Node cond2 = t[1].eqNode(nm->mkConst(CVC4::String("")));
+    // skk = n
+    Node cc2 = skk.eqNode(t[2]);
+
+    // substr( x, n, len( x ) - n ) = str.++( io2, y, io4 )
+    Node c31 = st.eqNode(nm->mkNode(kind::STRING_CONCAT, io2, t[1], io4));
+    // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
+    Node c32 =
+        nm->mkNode(
+              kind::STRING_STRCTN,
+              nm->mkNode(
+                  kind::STRING_CONCAT,
+                  io2,
+                  nm->mkNode(kind::STRING_SUBSTR,
+                             t[1],
+                             d_zero,
+                             nm->mkNode(kind::MINUS,
+                                        nm->mkNode(kind::STRING_LENGTH, t[1]),
+                                        d_one))),
+              t[1])
+            .negate();
+    // skk = n + len( io2 )
+    Node c33 = skk.eqNode(
+        nm->mkNode(kind::PLUS, t[2], nm->mkNode(kind::STRING_LENGTH, io2)));
+    Node cc3 = nm->mkNode(kind::AND, c31, c32, c33);
+
+    // assert:
+    // IF:   ~contains( substr( x, n, len( x ) - n ), y ) OR n > len(x) OR 0 > n
+    // THEN: skk = -1
+    // ELIF: y = ""
+    // THEN: skk = n
+    // ELSE: substr( x, n, len( x ) - n ) = str.++( io2, y, io4 ) ^
+    //       ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) ^
+    //       skk = n + len( io2 )
+    // for fresh io2, io4.
+    Node rr = nm->mkNode(
+        kind::ITE, cond1, cc1, nm->mkNode(kind::ITE, cond2, cc2, cc3));
     new_nodes.push_back( rr );
+
+    // Thus, indexof( x, y, n ) = skk.
     retNode = skk;
   } else if( t.getKind() == kind::STRING_ITOS ) {
     //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
@@ -363,28 +399,64 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
             NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
     new_nodes.push_back( conc );
     retNode = pret;
-  } else if( t.getKind() == kind::STRING_STRREPL ) {
+  }
+  else if (t.getKind() == kind::STRING_STRREPL)
+  {
+    // processing term: replace( x, y, z )
     Node x = t[0];
     Node y = t[1];
     Node z = t[2];
-    Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" );
-    Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" );
-    Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" );
-    Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
-    cond = NodeManager::currentNM()->mkNode( kind::AND, cond, NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
-    Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
-    Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
-    Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
-                NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
-                   NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, y, d_zero,
-                      NodeManager::currentNM()->mkNode(kind::MINUS,
-                        NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y),
-                        NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate();
-    Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond,
-                                                NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3),
-                                                skw.eqNode(x) );
+    TypeNode tn = t[0].getType();
+    Node rp1 = nm->mkSkolem("rp1", tn, "created for replace");
+    Node rp2 = nm->mkSkolem("rp2", tn, "created for replace");
+    Node rpw = nm->mkSkolem("rpw", tn, "created for replace");
+
+    // y = ""
+    Node cond1 = y.eqNode(nm->mkConst(CVC4::String("")));
+    // rpw = str.++( z, x )
+    Node c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x));
+
+    // contains( x, y )
+    Node cond2 = nm->mkNode(kind::STRING_STRCTN, x, y);
+    // x = str.++( rp1, y, rp2 )
+    Node c21 = x.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, y, rp2));
+    // rpw = str.++( rp1, z, rp2 )
+    Node c22 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, z, rp2));
+    // ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y )
+    Node c23 =
+        nm->mkNode(kind::STRING_STRCTN,
+                   nm->mkNode(
+                       kind::STRING_CONCAT,
+                       rp1,
+                       nm->mkNode(kind::STRING_SUBSTR,
+                                  y,
+                                  d_zero,
+                                  nm->mkNode(kind::MINUS,
+                                             nm->mkNode(kind::STRING_LENGTH, y),
+                                             d_one))),
+                   y)
+            .negate();
+
+    // assert:
+    //   IF    y=""
+    //   THEN: rpw = str.++( z, x )
+    //   ELIF: contains( x, y )
+    //   THEN: x = str.++( rp1, y, rp2 ) ^
+    //         rpw = str.++( rp1, z, rp2 ) ^
+    //         ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y ),
+    //   ELSE: rpw = x
+    // for fresh rp1, rp2, rpw
+    Node rr = nm->mkNode(kind::ITE,
+                         cond1,
+                         c1,
+                         nm->mkNode(kind::ITE,
+                                    cond2,
+                                    nm->mkNode(kind::AND, c21, c22, c23),
+                                    rpw.eqNode(x)));
     new_nodes.push_back( rr );
-    retNode = skw;
+
+    // Thus, replace( x, y, z ) = rpw.
+    retNode = rpw;
   } else if( t.getKind() == kind::STRING_STRCTN ){
     Node x = t[0];
     Node s = t[1];
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 1555b0aa0..e66861579 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1827,16 +1827,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
     return returnRewrite(node, negone, "idof-neg");
   }
 
-  if (node[1].isConst())
-  {
-    if (node[1].getConst<String>().size() == 0)
-    {
-      // str.indexof( x, "", z ) --> -1
-      Node negone = nm->mkConst(Rational(-1));
-      return returnRewrite(node, negone, "idof-empty");
-    }
-  }
-
   // evaluation and simple cases
   std::vector<Node> children0;
   getConcat(node[0], children0);
@@ -1884,16 +1874,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
   {
     fstr = nm->mkNode(kind::STRING_SUBSTR, node[0], node[2], len0);
     fstr = Rewriter::rewrite(fstr);
-    if (fstr.isConst())
-    {
-      CVC4::String fs = fstr.getConst<String>();
-      if (fs.size() == 0)
-      {
-        // substr( x, z, len(x) ) --> ""  implies str.indexof( x, y, z ) --> -1
-        Node negone = nm->mkConst(Rational(-1));
-        return returnRewrite(node, negone, "idof-base-len");
-      }
-    }
   }
 
   Node cmp_con = nm->mkNode(kind::STRING_STRCTN, fstr, node[1]);
@@ -1960,25 +1940,22 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
 
 Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   Assert(node.getKind() == kind::STRING_STRREPL);
-  if( node[1]==node[2] ){
+  NodeManager* nm = NodeManager::currentNM();
+
+  if (node[1] == node[2])
+  {
     return returnRewrite(node, node[0], "rpl-id");
   }
-  if (node[0].isConst())
+
+  if (node[0] == node[1])
   {
-    CVC4::String s = node[0].getConst<String>();
-    if (s.isEmptyString())
-    {
-      return returnRewrite(node, node[0], "rpl-empty");
-    }
-    if (node[0] == node[2] && s.size() == 1)
-    {
-      // str.replace( "A", x, "A" ) -> "A"
-      return returnRewrite(node, node[0], "rpl-char-id");
-    }
+    return returnRewrite(node, node[2], "rpl-replace");
   }
+
   if (node[1].isConst() && node[1].getConst<String>().isEmptyString())
   {
-    return returnRewrite(node, node[0], "rpl-rpl-empty");
+    Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]);
+    return returnRewrite(node, ret, "rpl-rpl-empty");
   }
 
   std::vector<Node> children0;
@@ -2047,26 +2024,13 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   {
     if (cmp_conr.getConst<bool>())
     {
-      // currently by the semantics of replace, if the second argument is
-      // empty, then we return the first argument.
-      // hence, we test whether the second argument must be non-empty here.
-      // if it definitely non-empty, we can use rules that successfully replace
-      // node[1]->node[2] among those below.
-      Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
-      Node zero = NodeManager::currentNM()->mkConst(CVC4::Rational(0));
-      bool is_non_empty = checkEntailArith(l1, zero, true);
-
-      if (node[0] == node[1] && is_non_empty)
-      {
-        return returnRewrite(node, node[2], "rpl-replace");
-      }
       // component-wise containment
       std::vector<Node> cb;
       std::vector<Node> ce;
       int cc = componentContains(children0, children1, cb, ce, true, 1);
       if (cc != -1)
       {
-        if (cc == 0 && children0[0] == children1[0] && is_non_empty)
+        if (cc == 0 && children0[0] == children1[0])
         {
           // definitely a prefix, can do the replace
           // for example,
@@ -2106,24 +2070,27 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
 
   if (cmp_conr != cmp_con)
   {
-    // pull endpoints that can be stripped
-    // for example,
-    //   str.replace( str.++( "b", x, "b" ), "a", y ) --->
-    //   str.++( "b", str.replace( x, "a", y ), "b" )
-    std::vector<Node> cb;
-    std::vector<Node> ce;
-    if (stripConstantEndpoints(children0, children1, cb, ce))
+    if (checkEntailNonEmpty(node[1]))
     {
-      std::vector<Node> cc;
-      cc.insert(cc.end(), cb.begin(), cb.end());
-      cc.push_back(NodeManager::currentNM()->mkNode(
-          kind::STRING_STRREPL,
-          mkConcat(kind::STRING_CONCAT, children0),
-          node[1],
-          node[2]));
-      cc.insert(cc.end(), ce.begin(), ce.end());
-      Node ret = mkConcat(kind::STRING_CONCAT, cc);
-      return returnRewrite(node, ret, "rpl-pull-endpt");
+      // pull endpoints that can be stripped
+      // for example,
+      //   str.replace( str.++( "b", x, "b" ), "a", y ) --->
+      //   str.++( "b", str.replace( x, "a", y ), "b" )
+      std::vector<Node> cb;
+      std::vector<Node> ce;
+      if (stripConstantEndpoints(children0, children1, cb, ce))
+      {
+        std::vector<Node> cc;
+        cc.insert(cc.end(), cb.begin(), cb.end());
+        cc.push_back(NodeManager::currentNM()->mkNode(
+            kind::STRING_STRREPL,
+            mkConcat(kind::STRING_CONCAT, children0),
+            node[1],
+            node[2]));
+        cc.insert(cc.end(), ce.begin(), ce.end());
+        Node ret = mkConcat(kind::STRING_CONCAT, cc);
+        return returnRewrite(node, ret, "rpl-pull-endpt");
+      }
     }
   }
 
@@ -2661,13 +2628,13 @@ bool TheoryStringsRewriter::componentContainsBase(
               NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n2[0]);
           if (dir == 1)
           {
-            // To be suffix, start + length must be greater than
+            // To be a suffix, start + length must be greater than
             // or equal to the length of the string.
             success = checkEntailArith(end_pos, len_n2s);
           }
           else if (dir == -1)
           {
-            // To be prefix, must literally start at 0, since
+            // To be a prefix, must literally start at 0, since
             //   if we knew it started at <0, it should be rewritten to "",
             //   if we knew it started at 0, then n2[1] should be rewritten to
             //   0.
@@ -2678,6 +2645,12 @@ bool TheoryStringsRewriter::componentContainsBase(
           {
             if (computeRemainder)
             {
+              // we can only compute the remainder if start_pos and end_pos
+              // are known to be non-negative.
+              if (!checkEntailArith(start_pos) || !checkEntailArith(end_pos))
+              {
+                return false;
+              }
               if (dir != 1)
               {
                 n1rb = NodeManager::currentNM()->mkNode(
@@ -2883,6 +2856,13 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
   return changed;
 }
 
+bool TheoryStringsRewriter::checkEntailNonEmpty(Node a)
+{
+  Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a);
+  len = Rewriter::rewrite(len);
+  return checkEntailArith(len, true);
+}
+
 bool TheoryStringsRewriter::checkEntailArithEq(Node a, Node b)
 {
   if (a == b)
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index e0d265334..217546c71 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -91,19 +91,24 @@ private:
   * Context-Dependent Rewriting", CAV 2017.
   */
   static Node rewriteContains(Node node);
+  /** rewrite indexof
+  * This is the entry point for post-rewriting terms n of the form
+  *   str.indexof( s, t, n )
+  * Returns the rewritten form of node.
+  */
   static Node rewriteIndexof(Node node);
   /** rewrite replace
   * This is the entry point for post-rewriting terms n of the form
   *   str.replace( s, t, r )
-  * Returns the rewritten form of n.
+  * Returns the rewritten form of node.
   */
-  static Node rewriteReplace(Node n);
+  static Node rewriteReplace(Node node);
   /** rewrite prefix/suffix
   * This is the entry point for post-rewriting terms n of the form
   *   str.prefixof( s, t ) / str.suffixof( s, t )
-  * Returns the rewritten form of n.
+  * Returns the rewritten form of node.
   */
-  static Node rewritePrefixSuffix(Node n);
+  static Node rewritePrefixSuffix(Node node);
 
   /** gets the "vector form" of term n, adds it to c.
   * For example:
@@ -269,6 +274,29 @@ private:
    * componentContainsBase(y, str.substr(y,0,5), n1rb, n1re, -1, true)
    *   returns true,
    *   n1re is set to str.substr(y,5,str.len(y)).
+   *
+   *
+   * Notice that this function may return false when it cannot compute a
+   * remainder when it otherwise would have returned true. For example:
+   *
+   * componentContainsBase(y, str.substr(y,x,z), n1rb, n1re, 0, false)
+   *   returns true.
+   *
+   * Hence, we know that str.substr(y,x,z) is contained in y. However:
+   *
+   * componentContainsBase(y, str.substr(y,x,z), n1rb, n1re, 0, true)
+   *   returns false.
+   *
+   * The reason is since computeRemainder=true, it must be that
+   *   y = str.++( n1rb, str.substr(y,x,z), n1re )
+   * for some n1rb, n1re. However, to construct such n1rb, n1re would require
+   * e.g. the terms:
+   *   y = str.++( ite( x+z < 0 OR x < 0, "", str.substr(y,0,x) ),
+   *               str.substr(y,x,z),
+   *               ite( x+z < 0 OR x < 0, y, str.substr(y,x+z,len(y)) ) )
+   *
+   * Since we do not wish to introduce ITE terms in the rewriter, we instead
+   * return false, indicating that we cannot compute the remainder.
    */
   static bool componentContainsBase(
       Node n1, Node n2, Node& n1rb, Node& n1re, int dir, bool computeRemainder);
@@ -305,6 +333,12 @@ private:
                                      std::vector<Node>& nb,
                                      std::vector<Node>& ne,
                                      int dir = 0);
+  /** entail non-empty
+   *
+   * Checks whether string a is entailed to be non-empty. Is equivalent to
+   * the call checkArithEntail( len( a ), true ).
+   */
+  static bool checkEntailNonEmpty(Node a);
   /** check arithmetic entailment equal
    * Returns true if it is always the case that a = b.
    */
diff --git a/test/regress/regress0/strings/idof-sem.smt2 b/test/regress/regress0/strings/idof-sem.smt2
index 90dcc83a0..0de8f6a67 100644
--- a/test/regress/regress0/strings/idof-sem.smt2
+++ b/test/regress/regress0/strings/idof-sem.smt2
@@ -1,6 +1,6 @@
 (set-logic SLIA)
 (set-option :strings-exp true)
-(set-info :status unsat)
+(set-info :status sat)
 (declare-fun x () String)
 (assert (not (= (str.indexof x "" 0) (- 1))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/repl-rewrites2.smt2 b/test/regress/regress0/strings/repl-rewrites2.smt2
index 42699bc8b..e56a8ea44 100644
--- a/test/regress/regress0/strings/repl-rewrites2.smt2
+++ b/test/regress/regress0/strings/repl-rewrites2.smt2
@@ -5,10 +5,11 @@
 (declare-fun x () String)
 (declare-fun y () String)
 (assert (or
-(not (= (str.replace "" "" "c") ""))
+(not (= (str.replace "" "" "c") "c"))
 (not (= (str.replace (str.++ "abc" y) "b" x) (str.++ "a" x "c" y)))
 (not (= (str.replace "" "abc" "de") ""))
 (not (= (str.replace "ab" "ab" "de") "de"))
-(not (= (str.replace "ab" "" "de") "ab"))
+(not (= (str.replace "ab" "" "de") "deab"))
+(not (= (str.replace "abb" "b" "de") "adeb"))
 ))
 (check-sat)
diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am
index 493cd5b6d..f6326e0c6 100644
--- a/test/regress/regress1/strings/Makefile.am
+++ b/test/regress/regress1/strings/Makefile.am
@@ -25,7 +25,6 @@ TESTS =	\
 	bug768.smt2 \
 	bug799-min.smt2 \
 	chapman150408.smt2 \
-	cmu-disagree-0707-dd.smt2 \
 	cmu-inc-nlpp-071516.smt2 \
 	cmu-substr-rw.smt2 \
 	crash-1019.smt2 \
@@ -73,7 +72,8 @@ TESTS =	\
 	str002.smt2 \
 	str007.smt2 \
 	rew-020618.smt2 \
-	double-replace.smt2
+	double-replace.smt2 \
+	string-unsound-sem.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2
deleted file mode 100644
index c44dfa396..000000000
--- a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2
+++ /dev/null
@@ -1,22 +0,0 @@
-(set-logic ALL_SUPPORTED)
-(set-info :status sat)
-(set-option :strings-exp true)
-
-(declare-fun url () String)
-
-(assert 
-(and 
-(and 
-(and 
-(and 
-
-(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) 
-
-(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http")))
-(> (str.indexof url ":" 0) 0))
-(>= (- (str.indexof url "#" 2) 2) 0)) 
-(>= (str.indexof url ":" 0) 0))
-)
-
-(check-sat)
-
diff --git a/test/regress/regress1/strings/double-replace.smt2 b/test/regress/regress1/strings/double-replace.smt2
index 0800592d6..bfbc3afc1 100644
--- a/test/regress/regress1/strings/double-replace.smt2
+++ b/test/regress/regress1/strings/double-replace.smt2
@@ -1,7 +1,8 @@
 (set-logic SLIA)
+(set-option :strings-fmf true)
 (set-option :strings-exp true)
 (set-info :status sat)
 (declare-fun x () String)
 (declare-fun y () String)
 (assert (not (= (str.replace (str.replace x y x) x y) x)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/repl-empty-sem.smt2 b/test/regress/regress1/strings/repl-empty-sem.smt2
index 61f70bc23..56d4f1b86 100644
--- a/test/regress/regress1/strings/repl-empty-sem.smt2
+++ b/test/regress/regress1/strings/repl-empty-sem.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --strings-exp
-; EXPECT: unsat
+; EXPECT: sat
 (set-logic ALL)
-(set-info :status unsat)
+(set-info :status sat)
 (declare-fun x () String)
 (declare-fun z () String)
 (assert (= (str.len z) 0))
diff --git a/test/regress/regress1/strings/repl-soundness-sem.smt2 b/test/regress/regress1/strings/repl-soundness-sem.smt2
index d56d7945f..f65b3b56a 100644
--- a/test/regress/regress1/strings/repl-soundness-sem.smt2
+++ b/test/regress/regress1/strings/repl-soundness-sem.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --strings-exp
-; EXPECT: sat
+; EXPECT: unsat
 (set-logic ALL)
-(set-info :status sat)
+(set-info :status unsat)
 (declare-fun x () String)
 (declare-fun y () String)
 (assert (and
diff --git a/test/regress/regress1/strings/rew-020618.smt2 b/test/regress/regress1/strings/rew-020618.smt2
index 5fb58a272..95dbf4d29 100644
--- a/test/regress/regress1/strings/rew-020618.smt2
+++ b/test/regress/regress1/strings/rew-020618.smt2
@@ -9,7 +9,7 @@
 (= (str.++ s s) "A")
 (not (str.contains s ""))
 (str.contains "" (str.++ s "A"))
-(not (= (str.replace "A" s "A") "A"))
+(not (= (str.replace "A" "" "A") "AA"))
 (not (= (str.prefixof s "A") (str.suffixof s "A")))
 (not (str.prefixof s s))
 (not (str.prefixof "" s))
diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2
new file mode 100644
index 000000000..771d8d4b0
--- /dev/null
+++ b/test/regress/regress1/strings/string-unsound-sem.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () Int)
+(assert (and
+(not (= (str.replace "A" (int.to.str z) x) (str.++ "A" (str.replace "" (int.to.str z) x))))
+(not (= (str.replace x (str.at x z) "") (str.++ (str.replace (str.++ (str.substr x 0 z) (str.substr x z 1)) (str.substr x z 1) "") (str.substr x (+ 1 z) (str.len x)))))
+)
+)
+(check-sat)
diff --git a/test/regress/regress2/strings/Makefile.am b/test/regress/regress2/strings/Makefile.am
index 9b397699c..4e6f3aa56 100644
--- a/test/regress/regress2/strings/Makefile.am
+++ b/test/regress/regress2/strings/Makefile.am
@@ -19,7 +19,8 @@ endif
 TESTS =	\
 	cmu-dis-0707-3.smt2 \
 	cmu-prereg-fmf.smt2 \
-	cmu-repl-len-nterm.smt2
+	cmu-repl-len-nterm.smt2 \
+	cmu-disagree-0707-dd.smt2
 
 
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2
new file mode 100644
index 000000000..c44dfa396
--- /dev/null
+++ b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2
@@ -0,0 +1,22 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun url () String)
+
+(assert 
+(and 
+(and 
+(and 
+(and 
+
+(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) 
+
+(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http")))
+(> (str.indexof url ":" 0) 0))
+(>= (- (str.indexof url "#" 2) 2) 0)) 
+(>= (str.indexof url ":" 0) 0))
+)
+
+(check-sat)
+