type conversion

7 files changed, 163 insertions, 10 deletions

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..09f536b15 100644
--- 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 367f3fe4f..cd583c144 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_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 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..2b0cedd07 100644
--- 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 84f58a16d..112f5eb4f 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,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 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)