add leading zeros support for str.to.int

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ef5da000fa6a3e7460bb84dffee292c4e8007861..c1f2c3a9cc7239e435e7edc9c74ddcd777d954ac 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -377,8 +377,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv M");
 
-                       Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
-                       new_nodes.push_back(pret.eqNode(ufP0));
+                       //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
+                       //new_nodes.push_back(pret.eqNode(ufP0));
                        //lemma
                        Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
                                str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
@@ -389,28 +389,23 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                t.eqNode(d_zero));
                        new_nodes.push_back(lem);*/
                        if(t.getKind()==kind::STRING_U16TOS) {
-                               lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
-                               NodeManager::currentNM()->mkNode(kind::GEQ, lenp, NodeManager::currentNM()->mkConst(::CVC4::String("5"))),
-                               pret.eqNode(negone));
+                               lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp);
                                new_nodes.push_back(lem);
                        } else if(t.getKind()==kind::STRING_U32TOS) {
-                               lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
-                               NodeManager::currentNM()->mkNode(kind::GEQ, lenp, NodeManager::currentNM()->mkConst(::CVC4::String("10"))),
-                               pret.eqNode(negone));
+                               lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp);
                                new_nodes.push_back(lem);
                        }
                        //cc1
-                       Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
+                       Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
                        //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
                        //cc2
                        std::vector< Node > vec_n;
-                       Node z1 = NodeManager::currentNM()->mkSkolem("z1", NodeManager::currentNM()->stringType());
-                       Node z2 = NodeManager::currentNM()->mkSkolem("z2", NodeManager::currentNM()->stringType());
-                       Node z3 = NodeManager::currentNM()->mkSkolem("z3", NodeManager::currentNM()->stringType());
-                       Node g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
+      Node p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType());
+      Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero);
                        vec_n.push_back(g);
-                       g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
+      g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p);
                        vec_n.push_back(g);
+      Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one);
                        char chtmp[2];
                        chtmp[1] = '\0';
                        for(unsigned i=0; i<=9; i++) {
@@ -429,60 +424,42 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
                        Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
                        Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
-                       Node w1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
-                       Node w2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
-                       Node b3v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, w1, w2);
+                       std::vector< Node > vec_c3;
+                       std::vector< Node > vec_c3b;
+      //qx between 0 and 9
+                       Node c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
+      vec_c3b.push_back(c3cc);
+                       c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
+      vec_c3b.push_back(c3cc);
+      Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one);
+      for(unsigned i=0; i<=9; i++) {
+                               chtmp[0] = i + '0';
+                               std::string stmp(chtmp);
+                               c3cc = NodeManager::currentNM()->mkNode(kind::IFF, 
+          ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))),
+          sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp))));
+                               vec_c3b.push_back(c3cc);
+      }
+      //c312
                        Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
-                       Node c3c1 = 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,b2,one)) ));
-                       c3c1 = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GT, ufx, d_zero), c3c1);
-                       c3c1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, c3c1);
-                       Node lstx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]).eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b2, one));
-                       Node c3c2 = ufx.eqNode(ufMx);
-                       c3c2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, c3c2);
-                       // leading zero
-                       Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))).negate());
-                       Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
-                       // cc3
-                       Node c3c3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
-                       Node c3c4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
-                       Node rev = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, w1).eqNode(
-                                               NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]),
-                                               NodeManager::currentNM()->mkNode(kind::PLUS, b2, 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 c3c5 = t[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, w1, ch, w2));
-                       c3c5 = NodeManager::currentNM()->mkNode(kind::AND, rev, c3c5);
-                       c3c5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b3v, c3c5);
-                       std::vector< Node > svec;
-                       svec.push_back(c3c1);svec.push_back(c3c2);
-                       //svec.push_back(cc21);
-                       svec.push_back(c3c3);svec.push_back(c3c4);svec.push_back(c3c5);
-                       Node cc3 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) );
-                       cc3 = NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, cc3);
-                       cc3 = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, cc3);
-                       //conc
-                       //Node conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
-                       Node conc = NodeManager::currentNM()->mkNode(kind::ITE, ufP0.eqNode(negone),
+      c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, 
+        ufx.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, 
+          NodeManager::currentNM()->mkNode(kind::MULT, ufx1, ten),
+          ufMx)));
+                       vec_c3b.push_back(c3cc);
+      c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b);
+      c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) );
+                       c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc);
+                       vec_c3.push_back(c3cc);
+      //unbound
+      c3cc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, d_zero));
+                       vec_c3.push_back(c3cc);
+                       Node lstx = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, one);
+      Node upflstx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, lstx);
+      c3cc = upflstx.eqNode(pret);
+                       vec_c3.push_back(c3cc);
+      Node cc3 = NodeManager::currentNM()->mkNode(kind::AND, vec_c3);
+      Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone),
                                                        NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
                        new_nodes.push_back( conc );
 

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index a47b4fbca549cc8c5a67006ca0e7618fa899e495..97d814a81664c3955a131483059ec4256000b093 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -506,10 +506,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                        CVC4::String s = node[0].getConst<String>();
                        if(s.isNumber()) {
                                std::string stmp = s.toString();
-                               if(stmp[0] == '0' && stmp.size() != 1) {
+                               //if(stmp[0] == '0' && stmp.size() != 1) {
                                        //TODO: leading zeros
-                                       retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
-                               } else {
+                                       //retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
+                               //} else {
                                        bool flag = false;
                                        CVC4::Rational r2(stmp.c_str());
                                        if(node.getKind() == kind::STRING_U16TOS) {
@@ -528,7 +528,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                        } else {
                                                retNode = NodeManager::currentNM()->mkConst( r2 );
                                        }
-                               }
+                               //}
                        } else {
                                retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
                        }

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 9977da6a5ef6d062a61b517fba6241d0cd149a6e..e7b3f2277313cf7c394d71690d64cc7e207f7786 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -36,6 +36,7 @@ TESTS =       \
   model001.smt2 \
   substr001.smt2 \
   regexp001.smt2 \
+  leadingzero001.smt2 \
   loop001.smt2 \
   loop002.smt2 \
   loop003.smt2 \

diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
new file mode 100644 (file)
index 0000000..3987c92
--- /dev/null
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+\r
+(declare-fun Y () String)\r
+\r
+(assert (= Y "0001"))\r
+;(assert (= (str.to.int Y) (- 1)))\r
+(assert (= (str.to.int Y) 1))\r
+\r
+(check-sat)\r