From be91d86dd0f7b33f7c373c4d9bd40e207af910d2 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 20 Feb 2014 18:31:27 -0600
Subject: [PATCH] add more tests, and define int.to.str(NEGATIVE)=""

---
 .../strings/theory_strings_preprocess.cpp     | 18 +++++++++-------
 .../strings/theory_strings_rewriter.cpp       | 18 +++++++++++-----
 test/regress/regress0/strings/type001.smt2    | 21 +++++++++++++++++++
 .../strings/{int2str.smt2 => type002.smt2}    |  0
 .../strings/{str2int.smt2 => type003.smt2}    |  0
 5 files changed, 45 insertions(+), 12 deletions(-)
 create mode 100644 test/regress/regress0/strings/type001.smt2
 rename test/regress/regress0/strings/{int2str.smt2 => type002.smt2} (100%)
 rename test/regress/regress0/strings/{str2int.smt2 => type003.smt2} (100%)

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1df79ccff..ca4a4e75e 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -235,14 +235,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			//				NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
 			//				t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
 			Node num = t[0];
-			Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
+			Node pret = t;//NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
 			Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 
-			/*Node lem = NodeManager::currentNM()->mkNode(kind::IFF,
-				t.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
-				t[0].eqNode(d_zero));
-			new_nodes.push_back(lem);*/
+			Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
+			Node lem = NodeManager::currentNM()->mkNode(kind::ITE, nonneg,
+				NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero),
+				t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
+				);
+			new_nodes.push_back(lem);
 
+			//non-neg
 			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 ),
@@ -262,8 +265,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 									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) );
+			lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero));
+			new_nodes.push_back( lem );
 
 			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));
@@ -318,6 +321,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) );
 			conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
 			conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+			conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc );
 			new_nodes.push_back( conc );
 			
 			/*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES, 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 660b7aafe..c459d7d7e 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -446,15 +446,23 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 		}
 	} 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) );
+			std::string stmp = node[0].getConst<Rational>().getNumerator().toString();
+			//std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << node[0]) )->str();
+			if(stmp[0] == '-') {
+				retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+			} else {
+				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));
+			if(s.isNumber()) {
+				std::string stmp = s.toString();
+				retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(stmp.c_str()));
+			} else {
+				retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
+			}
 		} else if(node[0].getKind() == kind::STRING_CONCAT) {
 			for(unsigned i=0; i<node[0].getNumChildren(); ++i) {
 				if(node[0][i].isConst()) {
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
new file mode 100644
index 000000000..ca93b00e5
--- /dev/null
+++ b/test/regress/regress0/strings/type001.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun z () String)
+
+;big num test
+(assert (= x (int.to.str 4785582390527685649)))
+;should be ""
+(assert (= y (int.to.str (- 9))))
+
+;big num
+(assert (= i (str.to.int "783914785582390527685649")))
+;should be -1
+(assert (= j (str.to.int "-783914785582390527685649")))
+
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/int2str.smt2 b/test/regress/regress0/strings/type002.smt2
similarity index 100%
rename from test/regress/regress0/strings/int2str.smt2
rename to test/regress/regress0/strings/type002.smt2
diff --git a/test/regress/regress0/strings/str2int.smt2 b/test/regress/regress0/strings/type003.smt2
similarity index 100%
rename from test/regress/regress0/strings/str2int.smt2
rename to test/regress/regress0/strings/type003.smt2
-- 
2.30.2