Merge branch 'master' of github.com:CVC4/CVC4

13 files changed, 363 insertions, 39 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9c2ac4c1b..6e8e9ea00 100644
--- 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 0afe29ccc..5dc3043af 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -286,6 +286,8 @@ 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: 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/options_handlers.h b/src/smt/options_handlers.h
index 51ad7b6ca..c9c3d6345 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -83,9 +83,9 @@ assertions\n\
 + Output the assertions after preprocessing and before clausification.\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
   where PASS is one of the preprocessing passes: definition-expansion\n\
-  boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
-  static-learning ite-removal repeat-simplify rewrite-apply-to-const\n\
-  theory-preprocessing.\n\
+  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+  simplify static-learning ite-removal repeat-simplify\n\
+  rewrite-apply-to-const theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
   \"assertions:pre-everything\") or after all preprocessing completes\n\
@@ -181,6 +181,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
       } else if(!strcmp(p, "boolean-terms")) {
       } else if(!strcmp(p, "constrain-subtypes")) {
       } else if(!strcmp(p, "substitution")) {
+      } else if(!strcmp(p, "strings-pp")) {
       } else if(!strcmp(p, "skolem-quant")) {
       } else if(!strcmp(p, "simplify")) {
       } else if(!strcmp(p, "static-learning")) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ef4f01cd1..7ada9d350 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -313,6 +313,12 @@ class SmtEnginePrivate : public NodeManagerListener {
   Node d_ufSubstr;
 
   /**
+   * Function symbol used to implement uninterpreted undefined string
+   * semantics.  Needed to deal with partial str2int function.
+   */
+  Node d_ufS2I;
+
+  /**
    * Function symbol used to implement uninterpreted division-by-zero
    * semantics.  Needed to deal with partial division function ("/").
    */
@@ -787,6 +793,34 @@ void SmtEngine::finalOptionsAreSet() {
     return;
   }
 
+  // for strings
+  if(options::stringExp()) {
+    if( !d_logic.isQuantified() ) {
+      d_logic = d_logic.getUnlockedCopy();
+      d_logic.enableQuantifiers();
+      Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
+    }
+    if(! options::finiteModelFind.wasSetByUser()) {
+      options::finiteModelFind.set( true );
+      Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
+    }
+    if(! options::fmfBoundInt.wasSetByUser()) {
+      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;
+    }
+    */
+  }
+
   if(options::bitvectorEagerBitblast()) {
     // Eager solver should use the internal decision strategy
     options::decisionMode.set(DECISION_STRATEGY_INTERNAL);
@@ -937,29 +971,6 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
 
-
-  // for strings
-  if(options::stringExp()) {
-    if( !d_logic.isQuantified() ) {
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.enableQuantifiers();
-      d_logic.lock();
-      Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
-    }
-    if(! options::finiteModelFind.wasSetByUser()) {
-      options::finiteModelFind.set( true );
-      Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
-    }
-    if(! options::fmfBoundInt.wasSetByUser()) {
-      options::fmfBoundInt.set( true );
-      Trace("smt") << "turning on fmf-bound-int, 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
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
@@ -3118,11 +3129,18 @@ void SmtEnginePrivate::processAssertions() {
   // Assertions ARE guaranteed to be rewritten by this point
 
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+    dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
     CVC4::theory::strings::StringsPreprocess sp;
-    sp.simplify( d_assertionsToPreprocess );
+    std::vector<Node> newNodes;
+    newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
+    sp.simplify( d_assertionsToPreprocess, newNodes );
+    if(newNodes.size() > 1) {
+      d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
+    }
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
       d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
     }
+    dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
   }
   if( d_smt.d_logic.isQuantified() ){
     dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 43b582bc8..3fc08e18e 100644
--- 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 7d631e826..7fbefe251 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -21,6 +21,8 @@ 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 (total function)"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -115,6 +117,8 @@ 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_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 367f3fe4f..d8b20d890 100644
--- 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);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -404,8 +407,14 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   case kind::CONST_STRING:
   case kind::STRING_CONCAT:
   case kind::STRING_SUBSTR_TOTAL:
+  case kind::STRING_ITOS:
+  case kind::STRING_STOI:
 	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 +1766,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 +2373,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 +2445,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 73d7619db..87cc3330a 100644
--- 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 7bdacb92d..43e7829bb 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -230,7 +230,206 @@ 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 type conv P");
+			Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+								NodeManager::currentNM()->mkFunctionType(
+									argTypes, NodeManager::currentNM()->integerType()),
+								"uf type conv 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_STOI ) {
+		if(options::stringExp()) {
+			Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+			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 type conv P");
+			Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+								NodeManager::currentNM()->mkFunctionType(
+									argTypes, NodeManager::currentNM()->integerType()),
+								"uf type conv M");
+
+			Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
+			new_nodes.push_back(t.eqNode(ufP0));
+			//cc1
+			Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
+			cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
+			//cc2
+			Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
+			Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType());
+			Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType());
+			Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType());
+			Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3);
+			std::vector< Node > vec_n;
+			Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero);
+			vec_n.push_back(g);
+			g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b1);
+			vec_n.push_back(g);
+			g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) );
+			vec_n.push_back(g);
+			g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
+			vec_n.push_back(g);
+			g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
+			vec_n.push_back(g);
+			char chtmp[2];
+			chtmp[1] = '\0';
+			for(unsigned i=0; i<=9; i++) {
+				chtmp[0] = i + '0';
+				std::string stmp(chtmp);
+				g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
+				vec_n.push_back(g);
+			}
+			Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
+			cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2);
+			cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc2);
+			//cc3
+			Node b2 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->integerType());
+			Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
+			Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
+						NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
+						NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b2));
+			Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
+			Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
+			Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
+			Node w1 = NodeManager::currentNM()->mkBoundVar("w1", NodeManager::currentNM()->stringType());
+			Node w2 = NodeManager::currentNM()->mkBoundVar("w2", NodeManager::currentNM()->stringType());
+			Node b3v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, w1, w2);
+			Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
+			Node c3c1 = 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,b2,one)) ));
+			c3c1 = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GT, ufx, d_zero), c3c1);
+			c3c1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, c3c1);
+			Node lstx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]).eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b2, one));
+			Node c3c2 = ufx.eqNode(ufMx);
+			c3c2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, c3c2);
+			Node c3c3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
+			Node c3c4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
+			Node rev = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, w1).eqNode(
+						NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]),
+						NodeManager::currentNM()->mkNode(kind::PLUS, b2, 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 c3c5 = t[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, w1, ch, w2));
+			c3c5 = NodeManager::currentNM()->mkNode(kind::AND, rev, c3c5);
+			c3c5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b3v, c3c5);
+			Node cc3 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, c3c1, c3c2, c3c3, c3c4, c3c5) );
+			cc3 = NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, cc3);
+			cc3 = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, cc3);
+			//conc
+			Node conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
+			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 +445,7 @@ 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 );
+
 			d_cache[t] = skw;
 			retNode = skw;
 		} else {
@@ -277,21 +477,24 @@ 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;
 }
 
-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
-	std::vector< Node > new_nodes;
+void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) {
 	for( unsigned i=0; i<vec_node.size(); i++ ){
 		vec_node[i] = simplify( vec_node[i], new_nodes );
 	}
+}
+
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+	std::vector< Node > new_nodes;
+	simplify(vec_node, new_nodes);
 	vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 }
 
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 7aa0a2af8..c2d5d656a 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -39,6 +39,7 @@ private:
 	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );
 	Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
+    void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
     void simplify(std::vector< Node > &vec_node);
 	StringsPreprocess();
 };
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 84f58a16d..660b7aafe 100644
--- 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,28 @@ 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) {
+		if(node[0].isConst()) {
+			CVC4::String s = node[0].getConst<String>();
+			int rt = s.toNumber();
+			retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(rt));
+		} else if(node[0].getKind() == kind::STRING_CONCAT) {
+			for(unsigned i=0; i<node[0].getNumChildren(); ++i) {
+				if(node[0][i].isConst()) {
+					CVC4::String t = node[0][i].getConst<String>();
+					if(!t.isNumber()) {
+						retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
+						break;
+					}
+				}
+			}
+		}
 	} 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 2b198892b..0c365e993 100644
--- 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)
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 4c69592d4..4d12803ff 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -354,6 +354,27 @@ public:
     ret_vec.insert( ret_vec.end(), itr, itr + j );
       return String(ret_vec);
   }
+  bool isNumber() const {
+	 for(unsigned int i=0; i<d_str.size(); ++i) {
+	   char c = convertUnsignedIntToChar( d_str[i] );
+	   if(c<'0' || c>'9') {
+		   return false;
+	   }
+	 }
+	 return true;
+  }
+  int toNumber() const {
+	 if(isNumber()) {
+		 int ret=0;
+		 for(unsigned int i=0; i<d_str.size(); ++i) {
+		   char c = convertUnsignedIntToChar( d_str[i] );
+		   ret = ret * 10 + (int)c - (int)'0';
+		 }
+		 return ret;
+	 } else {
+		 return -1;
+	 }
+  }
 };/* class String */
 
 namespace strings {