Change semantics of str.substr to allow endpoint out of bounds, and return empty string for error conditions. Improve rewriter for str.substr.

6 files changed, 116 insertions, 123 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 0f68d1207..3cdff9cba 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -15,9 +15,8 @@ typechecker "theory/strings/theory_strings_type_rules.h"
 operator STRING_CONCAT 2: "string concat (N-ary)"
 operator STRING_IN_REGEXP 2 "membership"
 operator STRING_LENGTH 1 "string length"
-operator STRING_SUBSTR 3 "string substr (user symbol)"
-operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
-operator STRING_CHARAT 2 "string charat (user symbol)"
+operator STRING_SUBSTR 3 "string substr"
+operator STRING_CHARAT 2 "string charat"
 operator STRING_STRCTN 2 "string contains"
 operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
@@ -107,7 +106,6 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index cad1f3bf1..ac4bddd73 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -975,8 +975,8 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
         Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
         Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),
               NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );
-        Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1));
-        Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)));
+        Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, d_zero, b1));
+        Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)));
         Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();
         if(r[0].getKind() == kind::STRING_TO_REGEXP) {
           s1r1 = s1.eqNode(r[0][0]).negate();
@@ -1054,8 +1054,8 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
           Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_one),
                 NodeManager::currentNM()->mkNode( kind::GEQ, lens, b1 ) );
           //internal
-          Node s1 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1);
-          Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1));
+          Node s1 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, d_zero, b1);
+          Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1));
           Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();
           Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r).negate();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fc8df8bbc..d985977d6 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -97,7 +97,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
   d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
   d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
-  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
+  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
   d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
   d_equalityEngine.addFunctionKind(kind::STRING_STOI);
   if( options::stringLazyPreproc() ){
@@ -466,7 +466,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
         d_equalityEngine.addTerm(n[1]);
         break;
       }
-      //case kind::STRING_SUBSTR_TOTAL:
+      //case kind::STRING_SUBSTR:
       default: {
         if( n.getType().isString() ) {
           registerTerm(n);
@@ -488,60 +488,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 }
 
 Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
-  switch (node.getKind()) {
-    case kind::STRING_CHARAT: {
-      if(d_ufSubstr.isNull()) {
-        std::vector< TypeNode > argTypes;
-        argTypes.push_back(NodeManager::currentNM()->stringType());
-        argTypes.push_back(NodeManager::currentNM()->integerType());
-        argTypes.push_back(NodeManager::currentNM()->integerType());
-        d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-                    NodeManager::currentNM()->mkFunctionType(
-                               argTypes, NodeManager::currentNM()->stringType()),
-                    "uf substr",
-                    NodeManager::SKOLEM_EXACT_NAME);
-      }
-      Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
-                   NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
-      Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], d_zero);
-      Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
-      Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one);
-      Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], d_one);
-      return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-      //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one);
-      break;
-    }
-
-    case kind::STRING_SUBSTR: {
-      if(d_ufSubstr.isNull()) {
-        std::vector< TypeNode > argTypes;
-        argTypes.push_back(NodeManager::currentNM()->stringType());
-        argTypes.push_back(NodeManager::currentNM()->integerType());
-        argTypes.push_back(NodeManager::currentNM()->integerType());
-        d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-                    NodeManager::currentNM()->mkFunctionType(
-                               argTypes, NodeManager::currentNM()->stringType()),
-                    "uf substr",
-                    NodeManager::SKOLEM_EXACT_NAME);
-      }
-      Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-                   NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
-                   NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
-      Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], d_zero);
-      Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], d_zero);
-      Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-      Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
-      Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
-      return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-      //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
-      break;
-    }
-
-    default :
-      return node;
-  }
-
-  Unreachable();
+  return node;
 }
 
 
@@ -3492,10 +3439,10 @@ void TheoryStrings::checkMemberships() {
                       NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
                       NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
                       NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
-                Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi);
-                Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
-                Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj);
-                Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
+                Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, d_zero, bi);
+                Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
+                Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, d_zero, bj);
+                Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
                 Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
                 Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP,  mkConcat(s12, s21), r[0]).negate();
                 Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
@@ -4178,8 +4125,8 @@ void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) {
             Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
                   NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
             Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-            Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
-            Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b2, d_one);
+            Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
+            Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b2, d_one);
 
             Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6);
 
@@ -4506,7 +4453,7 @@ void TheoryStrings::assertNode( Node lit ) {
 void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( n.getKind()==kind::STRING_SUBSTR_TOTAL || n.getKind()==kind::STRING_STRIDOF ||
+    if( n.getKind()==kind::STRING_SUBSTR || n.getKind()==kind::STRING_STRIDOF ||
         n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS ||
         n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 ||
         n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index b2864656a..f57bf43f8 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -119,12 +119,6 @@ public:
   };/* class TheoryStrings::NotifyClass */
 
 private:
-  /**
-   * Function symbol used to implement uninterpreted undefined string
-   * semantics.  Needed to deal with partial charat/substr function.
-   */
-  Node d_ufSubstr;
-
   // Constants
   Node d_emptyString;
   Node d_emptyRegexp;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index b2b7bac5e..8f899cd46 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -162,7 +162,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
   Node retNode = t;
   if( options::stringLazyPreproc() ){
     //only process extended operators after preprocess
-    if( during_pp && ( t.getKind() == kind::STRING_SUBSTR_TOTAL || t.getKind() == kind::STRING_STRIDOF ||
+    if( during_pp && ( t.getKind() == kind::STRING_SUBSTR || t.getKind() == kind::STRING_STRIDOF ||
                        t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ||
                        t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ||
                        t.getKind() == kind::STRING_STRREPL ) ){
@@ -203,7 +203,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     n = Rewriter::rewrite(n);
     d_cache[t] = (t == n) ? Node::null() : n;
     retNode = n;
-  } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
+  } else if( t.getKind() == kind::STRING_SUBSTR ) {
+    /*
     Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
           NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
           NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
@@ -218,6 +219,31 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
             NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
             t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
+            */
+    Node t12 = NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] );
+    Node lt0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] );
+    //start point is greater than or equal zero
+    Node c1 = NodeManager::currentNM()->mkNode( kind::GEQ, t[1], d_zero );
+    //start point is less than end of string
+    Node c2 = NodeManager::currentNM()->mkNode( kind::GT, lt0, t[1] );
+    //length is positive
+    Node c3 = NodeManager::currentNM()->mkNode( kind::GT, t[2], d_zero );
+    Node cond = NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 );
+    
+    Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" );
+    Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" );
+    Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk2 ) );
+    //length of first skolem is second argument
+    Node b12 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ).eqNode( t[1] );
+    //length of second skolem is abs difference between end point and end of string
+    Node b13 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ).eqNode( 
+                 NodeManager::currentNM()->mkNode( kind::ITE, NodeManager::currentNM()->mkNode( kind::GEQ, lt0, t12 ), 
+                    NodeManager::currentNM()->mkNode( kind::MINUS, lt0, t12 ), d_zero ) );
+    
+    Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 );
+    Node b2 = t.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
+    
+    Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) );
     new_nodes.push_back( lemma );
     d_cache[t] = t;
   } else if( t.getKind() == kind::STRING_STRIDOF ) {
@@ -225,7 +251,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
     Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
     Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
-    Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR_TOTAL, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) );
+    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] ) );
     Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) );
     new_nodes.push_back( eq );
     Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
@@ -250,7 +276,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     //~contain(t2, s2)
     Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
                 NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
-                  NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero,
+                  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) )))),
@@ -437,7 +463,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     vec_n.push_back(g);
     g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p);
     vec_n.push_back(g);
-    Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one);
+    Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, str, p, one);
     char chtmp[2];
     chtmp[1] = '\0';
     for(unsigned i=0; i<=9; i++) {
@@ -463,7 +489,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     vec_c3b.push_back(c3cc);
     c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
     vec_c3b.push_back(c3cc);
-    Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one);
+    Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, str, b2, one);
     for(unsigned i=0; i<=9; i++) {
       chtmp[0] = i + '0';
       std::string stmp(chtmp);
@@ -516,7 +542,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     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_TOTAL, y, d_zero,
+                   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();
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6356277ed..2d6c1e3af 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1014,13 +1014,13 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   } else if(node.getKind() == kind::STRING_LENGTH) {
     if(node[0].isConst()) {
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
-    } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
+    } else if(node[0].getKind() == kind::STRING_SUBSTR) {
       //retNode = node[0][2];
     } else if(node[0].getKind() == kind::STRING_CONCAT) {
       Node tmpNode = rewriteConcatString(node[0]);
       if(tmpNode.isConst()) {
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
-      } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
+      } else if(tmpNode.getKind() == kind::STRING_SUBSTR) {
         //retNode = tmpNode[2];
       } else {
         // it has to be string concat
@@ -1028,7 +1028,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
           if(tmpNode[i].isConst()) {
             node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
-          } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) {
+          } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR) {
             node_vec.push_back( tmpNode[i][2] );
           } else {
             node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
@@ -1043,44 +1043,72 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         }
       }
     }
-  } else if( node.getKind() == kind::STRING_SUBSTR_TOTAL ){
+  }else if( node.getKind() == kind::STRING_CHARAT ){
+    Node one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+    retNode = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[0], node[1], one);
+  }else if( node.getKind() == kind::STRING_SUBSTR ){
     Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-    if(node[2] == zero) {
+    if( node[2].isConst() && node[2].getConst<Rational>().sgn()<=0 ) {
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-    } else if( node[1].isConst() && node[2].isConst() ) {
-      if(node[1].getConst<Rational>().sgn()>=0 && node[2].getConst<Rational>().sgn()>=0) {
-        CVC4::Rational sum(node[1].getConst<Rational>() + node[2].getConst<Rational>());
-        if( node[0].isConst() ) {
-          CVC4::Rational size(node[0].getConst<String>().size());
-          if( size >= sum ) {
-            //because size is smaller than MAX_INT
-            size_t i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
-            size_t j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
-            retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
-          } else {
-            retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-          }
-        } else if(node[0].getKind() == kind::STRING_CONCAT && node[0][0].isConst()) {
-          CVC4::Rational size2(node[0][0].getConst<String>().size());
-          if( size2 >= sum ) {
-            //because size2 is smaller than MAX_INT
-            size_t i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
-            size_t j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
-            retNode = NodeManager::currentNM()->mkConst( node[0][0].getConst<String>().substr(i, j) );
-          }
-        }
-      } else {
+    }else if( node[1].isConst() ){
+      if( node[1].getConst<Rational>().sgn()<0 ){
+        //bring forward to start at zero?  don't use this semantics, e.g. does not compose well with error conditions for str.indexof.
+        //retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, node[0], zero, NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-      }
-    } else if(node[1] == zero ) {
-      if( node[2].getKind() == kind::STRING_LENGTH && node[2][0]==node[0] ){
-        retNode = node[0];
       }else{
-        //check if lengths rewrite to the same thing
-        Node lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] );
-        lt = Rewriter::rewrite( lt );
-        if( lt==node[2] ){
-          retNode = node[0];
+        if( node[2].isConst() ){
+          Assert( node[2].getConst<Rational>().sgn()>=0);
+          CVC4::Rational v1( node[1].getConst<Rational>() );
+          CVC4::Rational v2( node[2].getConst<Rational>() );
+          std::vector< Node > children;
+          getConcat( node[0], children );
+          if( children[0].isConst() ){
+            CVC4::Rational size(children[0].getConst<String>().size());
+            if( v1 >= size ){
+              if( node[0].isConst() ){
+                retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+              }else{
+                children.erase( children.begin(), children.begin()+1 );
+                retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ), 
+                                                            NodeManager::currentNM()->mkNode( kind::MINUS, node[1], NodeManager::currentNM()->mkConst( size ) ),
+                                                            node[2] );
+              }
+            }else{
+              //since size is smaller than MAX_INT, v1 is smaller than MAX_INT
+              size_t i = v1.getNumerator().toUnsignedInt();
+              CVC4::Rational sum(v1 + v2);
+              bool full_spl = false;
+              size_t j;
+              if( sum>size ){
+                j = size.getNumerator().toUnsignedInt();
+              }else{
+                //similarly, sum is smaller than MAX_INT
+                j = sum.getNumerator().toUnsignedInt();
+                full_spl = true;
+              }
+              //split the first component of the string
+              Node spl = NodeManager::currentNM()->mkConst( children[0].getConst<String>().substr(i, j-i) );
+              if( node[0].isConst() || full_spl ){
+                retNode = spl;
+              }else{
+                children[0] = spl;
+                retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ), zero, node[2] );
+              }
+            }
+          }
+        }else{
+          if( node[1]==zero ){
+            if( node[2].getKind() == kind::STRING_LENGTH && node[2][0]==node[0] ){
+              retNode = node[0];
+            }else{
+              //check if the length argument is always at least the length of the string
+              Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, node[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ) );
+              cmp = Rewriter::rewrite( cmp );
+              if( cmp==NodeManager::currentNM()->mkConst(true) ){
+                retNode = node[0];
+              }
+            }
+          }
         }
       }
     }
@@ -1105,7 +1133,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
       Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
       retNode = NodeManager::currentNM()->mkNode(kind::AND,
             NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens),
-            node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1],
+            node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
                     NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ), lens)));
     }
   }else if( node.getKind() == kind::STRING_SUFFIX ){
@@ -1123,7 +1151,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
       Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
       retNode = NodeManager::currentNM()->mkNode(kind::AND,
             NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens),
-            node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1],
+            node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
                     NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens)));
     }
   }else if(node.getKind() == kind::STRING_ITOS || node.getKind() == kind::STRING_U16TOS || node.getKind() == kind::STRING_U32TOS) {