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

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1df79ccff1af85745b6e3a0276d7b38e7c2987a1..ca4a4e75e1799272d0867915ee795ad59f19132c 100644 (file)
--- 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 660b7aafe4cc5ee7cbdda89279ca7f4bf13db224..c459d7d7eb81dd051b3b26e007f8b330dc3da83d 100644 (file)
--- 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/int2str.smt2 b/test/regress/regress0/strings/int2str.smt2
deleted file mode 100644 (file)
index ac4d9ab..0000000
--- a/test/regress/regress0/strings/int2str.smt2
+++ /dev/null
@@ -1,18 +0,0 @@
-(set-logic QF_S)\r
-(set-info :status sat)\r
-(set-option :strings-exp true)\r
-\r
-(declare-fun x () String)\r
-(declare-fun y () String)\r
-(declare-fun z () String)\r
-(declare-fun i () Int)\r
-\r
-(assert (>= i 420))\r
-(assert (= x (int.to.str i)))\r
-(assert (= x (str.++ y "0" z)))\r
-(assert (not (= y "")))\r
-(assert (not (= z "")))\r
-\r
-\r
-\r
-(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/str2int.smt2 b/test/regress/regress0/strings/str2int.smt2
deleted file mode 100644 (file)
index b8f0ac5..0000000
--- a/test/regress/regress0/strings/str2int.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-(set-logic QF_S)\r
-(set-info :status sat)\r
-(set-option :strings-exp true)\r
-\r
-(declare-fun i () Int)\r
-(declare-fun s () String)\r
-\r
-(assert (< 67 (str.to.int s)))\r
-(assert (= (str.len s) 2))\r
-(assert (not (= s "68")))\r
-\r
-(check-sat)\r

diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
new file mode 100644 (file)
index 0000000..ca93b00
--- /dev/null
+++ b/test/regress/regress0/strings/type001.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+(set-option :strings-exp true)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+(declare-fun i () Int)\r
+(declare-fun j () Int)\r
+(declare-fun z () String)\r
+\r
+;big num test\r
+(assert (= x (int.to.str 4785582390527685649)))\r
+;should be ""\r
+(assert (= y (int.to.str (- 9))))\r
+\r
+;big num\r
+(assert (= i (str.to.int "783914785582390527685649")))\r
+;should be -1\r
+(assert (= j (str.to.int "-783914785582390527685649")))\r
+\r
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2
new file mode 100644 (file)
index 0000000..ac4d9ab
--- /dev/null
+++ b/test/regress/regress0/strings/type002.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+(set-option :strings-exp true)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+(declare-fun z () String)\r
+(declare-fun i () Int)\r
+\r
+(assert (>= i 420))\r
+(assert (= x (int.to.str i)))\r
+(assert (= x (str.++ y "0" z)))\r
+(assert (not (= y "")))\r
+(assert (not (= z "")))\r
+\r
+\r
+\r
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/type003.smt2 b/test/regress/regress0/strings/type003.smt2
new file mode 100644 (file)
index 0000000..b8f0ac5
--- /dev/null
+++ b/test/regress/regress0/strings/type003.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+(set-option :strings-exp true)\r
+\r
+(declare-fun i () Int)\r
+(declare-fun s () String)\r
+\r
+(assert (< 67 (str.to.int s)))\r
+(assert (= (str.len s) 2))\r
+(assert (not (= s "68")))\r
+\r
+(check-sat)\r