type conversion

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9c2ac4c1bf68542dba0bd9a9f3558983101ede1a..6e8e9ea00e8ec7a292e785589bb465f611bbff49 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1280,6 +1280,8 @@ builtinOp[CVC4::Kind& kind]
   | STRREPL_TOK    { $kind = CVC4::kind::STRING_STRREPL; }
   | STRPREF_TOK    { $kind = CVC4::kind::STRING_PREFIX; }
   | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
+  | STRITOS_TOK    { $kind = CVC4::kind::STRING_ITOS; }
+  | STRSTOI_TOK    { $kind = CVC4::kind::STRING_STOI; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1660,6 +1662,8 @@ STRIDOF_TOK : 'str.indexof' ;
 STRREPL_TOK : 'str.replace' ;
 STRPREF_TOK : 'str.prefixof' ;
 STRSUFF_TOK : 'str.suffixof' ;
+STRITOS_TOK : 'int.to.str' ;
+STRSTOI_TOK : 'str.to.int' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0afe29ccc11c96c29c28c9fc9fd2a5d9740c1d89..5ac56e02764fed7e6b80ac0af361a96892f48ca8 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -286,6 +286,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_STRREPL: out << "str.replace "; break;
   case kind::STRING_PREFIX: out << "str.prefixof "; break;
   case kind::STRING_SUFFIX: out << "str.suffixof "; break;
+  case kind::STRING_ITOS: out << "int.to.str "; break;
+  case kind::STRING_STOI_TOTAL:
+  case kind::STRING_STOI: out << "str.to.int "; break;
   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
   case kind::REGEXP_CONCAT: out << "re.++ "; break;
   case kind::REGEXP_OR: out << "re.or "; break;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ef4f01cd1dea00f1046612b2eaf8a634dc578b4b..dcca1624db89da6ef3c260823bd583cdfc5696be 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -954,10 +954,16 @@ void SmtEngine::setLogicInternal() throw() {
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
+       if(! options::rewriteDivk.wasSetByUser()) {
+      options::rewriteDivk.set( true );
+      Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
+    }
+
+       /*
     if(! options::stringFMF.wasSetByUser()) {
       options::stringFMF.set( true );
       Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
-    }
+    }*/
   }
 
   // by default, symmetry breaker is on only for QF_UF

diff --git a/src/theory/arith/options b/src/theory/arith/options
index 43b582bc87d50107afa1acc8572cb24f0bb5724d..3fc08e18e18fd41b535667a3b32ae1669f9559a9 100644 (file)
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -100,7 +100,7 @@ option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-wri
 option soiQuickExplain --soi-qe bool :default false :read-write
  use quick explain to minimize the sum of infeasibility conflicts
 
-option rewriteDivk rewrite-divk --rewrite-divk bool :default false
+option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write
  rewrite division and mod when by a constant into linear terms
 
 endmodule

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 7d631e826ab98a777ca9773101208d0e280a11eb..09f536b1572f8ecc70c0a67ea18c06a70ab0a6ca 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -21,6 +21,9 @@ operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
 operator STRING_PREFIX 2 "string prefixof"
 operator STRING_SUFFIX 2 "string suffixof"
+operator STRING_ITOS 1 "integer to string"
+operator STRING_STOI 1 "string to integer (user symbol)"
+operator STRING_STOI_TOTAL 1 "string to integer (internal symbol)"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -115,6 +118,9 @@ typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
+typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
+typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
+typerule STRING_STOI_TOTAL ::CVC4::theory::strings::StringStrToIntTypeRule
 
 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 367f3fe4f11a0fc3bf4841b0aad9601982578fca..cd583c1445a37caf3ae918c64e1f2354af4114c2 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -46,6 +46,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
        //d_var_lmax( c ),
        d_str_pos_ctn( c ),
        d_str_neg_ctn( c ),
+       d_int_to_str( c ),
        d_reg_exp_mem( c ),
        d_curr_cardinality( c, 0 )
 {
@@ -55,6 +56,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
     d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
+    d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
+    //d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -404,8 +407,13 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   case kind::CONST_STRING:
   case kind::STRING_CONCAT:
   case kind::STRING_SUBSTR_TOTAL:
+  case kind::STRING_ITOS:
        d_equalityEngine.addTerm(n);
        break;
+  //case kind::STRING_ITOS:
+       //d_int_to_str;
+       //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() ) {
@@ -1757,7 +1765,8 @@ 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_SUBSTR_TOTAL ) {
+                       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 );
@@ -2363,7 +2372,7 @@ bool TheoryStrings::checkContains() {
        Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
        if(!d_conflict && !addedLemma) {
                addedLemma = checkNegContains();
-               Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+               Trace("strings-process") << "Done check negative contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
        }
        return addedLemma;
 }
@@ -2435,8 +2444,13 @@ bool TheoryStrings::checkNegContains() {
                                                        addedLemma = true;
                                                }
                                        } else if(!areDisequal(lenx, lens)) {
-                                               sendSplit(lenx, lens, "NEG-CTN-SP");
-                                               addedLemma = true;
+                                               Node s = lenx < lens ? lenx : lens;
+                                               Node eq = s.eqNode( lenx < lens ? lens : lenx );
+                                               if(d_str_neg_ctn_ulen.find(eq) == d_str_neg_ctn_ulen.end()) {
+                                                       d_str_neg_ctn_ulen[ eq ] = true;
+                                                       sendSplit(lenx, lens, "NEG-CTN-SP");
+                                                       addedLemma = true;
+                                               }
                                        } else {
                                                if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) {
                                                        Node b1 = NodeManager::currentNM()->mkBoundVar("bi", NodeManager::currentNM()->integerType());

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 73d7619db46a98ca0e5cc3fa0f54244caf076dd8..87cc3330a1104e95ecd873913c0463372b791ff3 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -290,9 +290,12 @@ private:
        // Special String Functions
        NodeList d_str_pos_ctn;
        NodeList d_str_neg_ctn;
+       NodeList d_int_to_str;
        std::map< Node, bool > d_str_ctn_eqlen;
+       std::map< Node, bool > d_str_neg_ctn_ulen;
        std::map< Node, bool > d_str_pos_ctn_rewritten;
        std::map< Node, bool > d_str_neg_ctn_rewritten;
+       std::map< std::pair <Node, int>, bool > d_int_to_str_rewritten;
 
        // Regular Expression
 private:

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 7bdacb92daeccc948677b48b38afde881777ee16..2b0cedd07efd70e85b572c35eb6c190d7a13da3d 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -230,7 +230,96 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                } else {
                        throw LogicException("string indexof not supported in this release");
                }
-       } else if( t.getKind() == kind::STRING_STRREPL ){
+       } else if( t.getKind() == kind::STRING_ITOS ) {
+               if(options::stringExp()) {
+                       Node num = t[0];//NodeManager::currentNM()->mkNode(kind::ABS, t[0]);
+                       Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
+                       Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
+
+                       Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
+                       Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+                       Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
+                                               NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) );
+                       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+                       Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
+                       Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
+                       
+                       std::vector< TypeNode > argTypes;
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", 
+                                                               NodeManager::currentNM()->mkFunctionType(
+                                                                       argTypes, NodeManager::currentNM()->integerType()),
+                                                               "uf itos assist P");
+                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+                                                               NodeManager::currentNM()->mkFunctionType(
+                                                                       argTypes, NodeManager::currentNM()->integerType()),
+                                                               "uf itos assist M");
+                       
+                       new_nodes.push_back( num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)) );
+                       new_nodes.push_back( NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero) );
+
+                       Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1);
+                       Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one));
+                       Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1);
+                       Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero);
+                       Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
+                                                       NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
+                                                       NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) ));
+                       cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1);
+                       Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
+                       Node cc2 = ufx.eqNode(ufMx);
+                       cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
+                       Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
+                       Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
+                       
+                       Node b21 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->stringType());
+                       Node b22 = NodeManager::currentNM()->mkBoundVar("z", NodeManager::currentNM()->stringType());
+                       Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
+
+                       Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
+                                               NodeManager::currentNM()->mkNode(kind::MINUS, lenp,     NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) ));
+                       Node ch = 
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("0")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("1")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("2")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("3")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("4")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("5")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("6")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("7")),
+                               NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("8")),
+                               NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
+                       Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) );
+                       Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22));
+                       //Node pos = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
+                       //Node cc5 = ch.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, pret, pos, one) );
+                       Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, cc1, cc2, cc3, cc4, cc5) );
+                       conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+                       conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+                       new_nodes.push_back( conc );
+                       /*
+                       Node sign = NodeManager::currentNM()->mkNode(kind::ITE, 
+                                                       NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
+                                                       NodeManager::currentNM()->mkConst(::CVC4::String("")),
+                                                       NodeManager::currentNM()->mkConst(::CVC4::String("-")));
+                       conc = t.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sign, pret) );
+                       new_nodes.push_back( conc );*/
+
+                       d_cache[t] = t;
+                       retNode = t;
+               } else {
+                       throw LogicException("string int.to.str not supported in this release");
+               }
+       } else if( t.getKind() == kind::STRING_STRREPL ) {
                if(options::stringExp()) {
                        Node x = t[0];
                        Node y = t[1];
@@ -246,6 +335,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                                        NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ),
                                                        skw.eqNode(x) ) );
                        new_nodes.push_back( rr );
+                       //rr = cond.negate();
+                       //new_nodes.push_back( rr );
+
                        d_cache[t] = skw;
                        retNode = skw;
                } else {
@@ -277,11 +369,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 
        Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl;
        if(!new_nodes.empty()) {
-               Trace("strings-preprocess") << " ... new nodes:";
+               Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n";
                for(unsigned int i=0; i<new_nodes.size(); ++i) {
-                       Trace("strings-preprocess") << " " << new_nodes[i];
+                       Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n";
                }
-               Trace("strings-preprocess") << std::endl;
        }
 
        return retNode;

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 84f58a16d993cb333c37ad719845f7bf4df3059e..112f5eb4fbc73c4f4d6328be80299f8f5f2e2095 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -353,7 +353,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                } else if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
                        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
                        int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
-                       if( node[0].getConst<String>().size() >= (unsigned) (i + j) && i>=0 && j>=0 ) {
+                       if( i>=0 && j>=0 && node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
                                retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
                        } else {
                                retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -405,6 +405,8 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                        retNode = node[0];
                                }
                        }
+               } else {
+                       retNode = node[0];
                }
        } else if(node.getKind() == kind::STRING_PREFIX) {
                if(node[0].isConst() && node[1].isConst()) {
@@ -442,6 +444,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                                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_ITOS) {
+               if(node[0].isConst()) {
+                       int i = node[0].getConst<Rational>().getNumerator().toUnsignedInt();
+                       std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << i) )->str();
+                       retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) );
+               }
+       } else if(node.getKind() == kind::STRING_STOI_TOTAL) {
+               //TODO
+               Assert(false, "stoi not supported.");
        } else if(node.getKind() == kind::STRING_IN_REGEXP) {
                retNode = rewriteMembership(node);
        }

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 2b198892b725de4edc1169b1cef0c940ffcdf3f3..0c365e9938cd2d551b1c143a36eedf5674d39893 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -204,6 +204,34 @@ public:
   }
 };
 
+class StringIntToStrTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+        TypeNode t = n[0].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
+class StringStrToIntTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string to int 0");
+        }
+    }
+    return nodeManager->integerType();
+  }
+};
+
 class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)