fix expanding def

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8754dc08449d4b44ca270b331988fce90638dcb8..ef4f01cd1dea00f1046612b2eaf8a634dc578b4b 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -310,7 +310,7 @@ class SmtEnginePrivate : public NodeManagerListener {
    * Function symbol used to implement uninterpreted undefined string
    * semantics.  Needed to deal with partial charat/substr function.
    */
-  //Node d_substrUndef;
+  Node d_ufSubstr;
 
   /**
    * Function symbol used to implement uninterpreted division-by-zero
@@ -1555,9 +1555,53 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         node = expandBVDivByZero(node);
         break;
 
-         //case kind::STRING_CHARAT:
-         //case kind::STRING_SUBSTR:
-
+         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, n[0] ), n[1] );
+               Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+               Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero);
+               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
+               Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+               Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], one);
+               Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], one);
+               node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+               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, n[0] ),
+                                                       NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
+               Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+               Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], zero);
+               Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], zero);
+               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+               Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], n[2]);
+               Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], n[2]);
+               node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+               break;
+         }
       case kind::DIVISION: {
         // partial function: division
         if(d_divByZero.isNull()) {

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index b3a75a560205422bef2ba91d48dc0e170c130198..7d631e826ab98a777ca9773101208d0e280a11eb 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -14,6 +14,7 @@ operator STRING_CONCAT 2: "string concat"
 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_STRCTN 2 "string contains"
 operator STRING_STRIDOF 3 "string indexof"
@@ -107,6 +108,7 @@ 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/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f1b6c133a09ebeb22058f8370542bea4dce57962..0b4fe80c5a00d79e6466cbf410979c2935e1bbd1 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -54,8 +54,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_CHARAT);
-    //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
+    d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -404,12 +403,9 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     break;
   case kind::CONST_STRING:
   case kind::STRING_CONCAT:
+  case kind::STRING_SUBSTR_TOTAL:
        d_equalityEngine.addTerm(n);
        break;
-  case kind::STRING_CHARAT:
-  case kind::STRING_SUBSTR:
-       //d_equalityEngine.addTerm(n);
-       break;
   default:
     if(n.getType().isString() ) {
          if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) {
@@ -1761,7 +1757,7 @@ bool TheoryStrings::checkSimple() {
                        //if n is concat, and
                        //if n has not instantiatied the concat..length axiom
                        //then, add lemma
-                       if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT || n.getKind()==kind::STRING_CHARAT || n.getKind()==kind::STRING_SUBSTR ) {
+                       if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT || n.getKind()==kind::STRING_SUBSTR_TOTAL ) {
                                if( d_length_nodes.find(n)==d_length_nodes.end() ) {
                                        if( d_length_inst.find(n)==d_length_inst.end() ) {
                                                //Node nr = d_equalityEngine.getRepresentative( n );
@@ -1788,23 +1784,8 @@ bool TheoryStrings::checkSimple() {
                                                        } else if( n.getKind() == kind::CONST_STRING ) {
                                                                //add lemma
                                                                lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-                                                       } /*else if( n.getKind() == kind::STRING_CHARAT ) {
-                                                               lsum = d_one;
-                                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-                                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-                                                               d_statistics.d_new_skolems += 2;
-                                                               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
-                                                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
-                                                               Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero);
-                                                               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
-                                                               Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ) );
-                                                               Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-                                                               Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
-                                                               Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
-                                                               d_out->lemma(lemma);
-                                                       } else if( n.getKind() == kind::STRING_SUBSTR ) {
-                                                               lsum = n[2];
+                                                       } else if( n.getKind() == kind::STRING_SUBSTR_TOTAL ) {
+                                                               lsum = n[2];/*
                                                                Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
                                                                Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
                                                                d_statistics.d_new_skolems += 2;
@@ -1820,8 +1801,8 @@ bool TheoryStrings::checkSimple() {
                                                                Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
                                                                lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
                                                                Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
-                                                               d_out->lemma(lemma);
-                                                       }*/
+                                                               d_out->lemma(lemma);*/
+                                                       }
                                                        Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
                                                        ceq = Rewriter::rewrite(ceq);
                                                        Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
@@ -2421,18 +2402,6 @@ bool TheoryStrings::checkPosContains() {
 }
 
 bool TheoryStrings::checkNegContains() {
-       //Initialize UF
-       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);
-       }
        bool is_unk = false;
        bool addedLemma = false;
        for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
@@ -2474,10 +2443,8 @@ bool TheoryStrings::checkNegContains() {
                                                        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("bj", NodeManager::currentNM()->integerType());
-                                                       //Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
-                                                       //Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, s, b2);
-                                                       Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
-                                                       Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, s, b2, d_one);
+                                                       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 s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
                                                        Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 3143d6e898a6b01050196d934536cc1bda96ff88..73d7619db46a98ca0e5cc3fa0f54244caf076dd8 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -115,7 +115,6 @@ private:
     Node d_false;
     Node d_zero;
        Node d_one;
-       Node d_ufSubstr;
        // Options
        bool d_all_warning;
        bool d_opt_fmf;

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 707fae459008f8260600847246fcb4d616622ac9..1e2eb2572b027d2b2f5851e19b8d7d1519934e5a 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -127,19 +127,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       return (*i).second.isNull() ? t : (*i).second;
     }
 
-       //Initialize UF
-       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);
-       }
-
        Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
        Node retNode = t;
        /*int c_id = checkFixLenVar(t);
@@ -181,41 +168,23 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        // TODO
                //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
                //}
-       } else if( t.getKind() == kind::STRING_CHARAT ) {
-               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[1] );
-               Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, t[1], d_zero);
-               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
-               Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-               Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[0], t[1], one);
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, uf, sk3 ) );
-               Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-               Node len_uf_eq_j = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
-               Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, 
-                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_uf_eq_j )) );
-               new_nodes.push_back( lemma );
-               retNode = uf;
-               d_cache[t] = uf;
-       } else if( t.getKind() == kind::STRING_SUBSTR ) {
+       } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
                Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
                                                        NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
                                                        NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
                Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
                Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-               Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[0], t[1], t[2]);
                Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
                Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, uf, sk3 ) );
+               Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
                Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-               Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
+               //Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
                Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, 
-                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_uf_eq_j )) );
+                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i )) );
                new_nodes.push_back( lemma );
-               retNode = uf;
-               d_cache[t] = uf;
+               retNode = t;
+               d_cache[t] = t;
        } else if( t.getKind() == kind::STRING_STRIDOF ) {
                if(options::stringExp()) {
                        Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index a8074861efc62366abba1b7930debfc509f8a2da..7aa0a2af841df93d994634c6a46c7c9b9d368f53 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -33,7 +33,6 @@ class StringsPreprocess {
        std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
        //Constants
        Node d_zero;
-       Node d_ufSubstr;
 private:
        bool checkStarPlus( Node t );
        int checkFixLenVar( Node t );

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 1dc9cbe851472fbb20b8b6e07c689f41115c8b7b..b0899492700b5241034237cc38009ec4bfec748d 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -323,17 +323,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_CHARAT) {
-            retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
-               } else if(node[0].getKind() == kind::STRING_SUBSTR) {
+        } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
             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_CHARAT) {
-                               retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
-            } else if(tmpNode.getKind() == kind::STRING_SUBSTR) {
+            } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
                                retNode = tmpNode[2];
             } else {
                 // it has to be string concat
@@ -341,9 +337,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_CHARAT) {
-                        node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) );
-                                       } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR) {
+                                       } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) {
                         node_vec.push_back( tmpNode[i][2] );
                     } else {
                         node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
@@ -352,7 +346,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
             }
         }
-    } else if(node.getKind() == kind::STRING_SUBSTR) {
+    } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
                Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
                if(node[2] == zero) {
                        retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -375,13 +369,6 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
-       } else if(node.getKind() == kind::STRING_CHARAT) {
-               if( node[0].isConst() && node[1].isConst() ) {
-                       int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
-                       if( node[0].getConst<String>().size() > (unsigned) i ) {
-                               retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, 1) );
-                       }
-               }
        } else if(node.getKind() == kind::STRING_STRIDOF) {
                if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
                        CVC4::String s = node[0].getConst<String>();
@@ -432,7 +419,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, node[1],
+                                               node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1],
                                                                                NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ), lens)));
                }
        } else if(node.getKind() == kind::STRING_SUFFIX) {
@@ -450,7 +437,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, node[1],
+                                               node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1],
                                                                                NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens)));
                }
        } else if(node.getKind() == kind::STRING_IN_REGEXP) {