add more tests, and define int.to.str(NEGATIVE)=""

5 files changed, 45 insertions, 12 deletions

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
index ac4d9ab8a..ac4d9ab8a 100644
--- a/test/regress/regress0/strings/int2str.smt2
+++ b/test/regress/regress0/strings/type002.smt2
diff --git a/test/regress/regress0/strings/str2int.smt2 b/test/regress/regress0/strings/type003.smt2
index b8f0ac5ae..b8f0ac5ae 100644
--- a/test/regress/regress0/strings/str2int.smt2
+++ b/test/regress/regress0/strings/type003.smt2