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

2 files changed, 24 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()) {