Improve reduction for int.to.str (#2629)

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ba6caaf79a4ae9acb84e78cfc73e76b80fdf29ba..bdb3393242f48d8167e8c32e88dff9fb28067092 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -174,106 +174,88 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 
     // Thus, indexof( x, y, n ) = skk.
     retNode = skk;
-  } else if( t.getKind() == kind::STRING_ITOS ) {
-    //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
-    //        NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
-    //        t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
-    Node num = t[0];
-    Node pret = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
-    Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
-
-    Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
-
-    Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, nonneg.negate(),
-      pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
-      );
-    new_nodes.push_back(lem);
-
-    //non-neg
-    Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-    Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
-    Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
-                                                           NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) );
-    Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-    Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
-    Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
+  }
+  else if (t.getKind() == STRING_ITOS)
+  {
+    // processing term:  int.to.str( n )
+    Node n = t[0];
+    Node itost = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
+    Node leni = nm->mkNode(STRING_LENGTH, itost);
 
+    std::vector<Node> conc;
     std::vector< TypeNode > argTypes;
-    argTypes.push_back(NodeManager::currentNM()->integerType());
-    Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
-              NodeManager::currentNM()->mkFunctionType(
-                argTypes, NodeManager::currentNM()->integerType()),
-              "uf type conv P");
-    Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
-              NodeManager::currentNM()->mkFunctionType(
-                argTypes, NodeManager::currentNM()->integerType()),
-              "uf type conv M");
-
-    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));
-    Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1);
-    Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero);
-    Node cc1 = 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,b1,one)) ));
-    cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1);
-    Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
-    Node cc2 = ufx.eqNode(ufMx);
-    cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
-    // leading zero
-    Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate());
-    Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
-    //cc3
-    Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
-    Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
-
-    Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
-    Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
-    Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
-
-    Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
-          NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, 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 c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) );
-    Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22));
-    std::vector< Node > svec;
-    svec.push_back(cc1);svec.push_back(cc2);
-    svec.push_back(cc21);
-    svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5);
-    Node conc = 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,
-            NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
-            t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
-              NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
-    new_nodes.push_back( conc );*/
-    retNode = pret;
+    argTypes.push_back(nm->integerType());
+    Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
+    Node us =
+        nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
+    Node ud =
+        nm->mkSkolem("Ud", nm->mkFunctionType(argTypes, nm->stringType()));
+
+    Node lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni));
+    conc.push_back(lem);
+
+    lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
+    conc.push_back(lem);
+
+    lem = d_empty_str.eqNode(nm->mkNode(APPLY_UF, us, leni));
+    conc.push_back(lem);
+
+    lem = itost.eqNode(nm->mkNode(APPLY_UF, us, d_zero));
+    conc.push_back(lem);
+
+    Node x = nm->mkBoundVar(nm->integerType());
+    Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
+    Node g =
+        nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, leni));
+    Node udx = nm->mkNode(APPLY_UF, ud, x);
+    Node ux = nm->mkNode(APPLY_UF, u, x);
+    Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one));
+    Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0")));
+    Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, udx), c0);
+    Node usx = nm->mkNode(APPLY_UF, us, x);
+    Node usx1 = nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, x, d_one));
+
+    Node ten = nm->mkConst(Rational(10));
+    Node eqs = usx.eqNode(nm->mkNode(STRING_CONCAT, udx, usx1));
+    Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
+    Node cb = nm->mkNode(
+        AND,
+        nm->mkNode(GEQ, c, nm->mkNode(ITE, x.eqNode(d_zero), d_one, d_zero)),
+        nm->mkNode(LT, c, ten));
+
+    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb));
+    lem = nm->mkNode(FORALL, xbv, lem);
+    conc.push_back(lem);
+
+    Node nonneg = nm->mkNode(GEQ, n, d_zero);
+
+    lem = nm->mkNode(
+        ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(d_empty_str));
+    new_nodes.push_back(lem);
+    // assert:
+    // IF n>=0
+    // THEN:
+    //   n = U( len( itost ) ) ^ U( 0 ) = 0 ^
+    //   "" = Us( len( itost ) ) ^ itost = Us( 0 ) ^
+    //   forall x. (x>=0 ^ x < str.len(itost)) =>
+    //     Us( x ) = Ud( x ) ++ Us( x+1 ) ^
+    //     U( x+1 ) = (str.code( Ud( x ) )-48) + 10*U( x ) ^
+    //     ite( x=0, 49, 48 ) <= str.code( Ud( x ) ) < 58
+    // ELSE
+    //   itost = ""
+    // thus:
+    //   int.to.str( n ) = itost
+
+    // In the above encoding, we use Us/Ud to introduce a chain of strings
+    // that allow us to refer to each character substring of itost. Notice this
+    // is more efficient than using str.substr( itost, x, 1 ).
+    // The function U is an accumulator, where U( x ) for x>0 is the value of
+    // str.to.int( str.substr( int.to.str( n ), 0, x ) ). For example, for
+    // n=345, we have that U(1), U(2), U(3) = 3, 34, 345.
+    // Above, we use str.code to map characters to their integer value, where
+    // note that str.code( "0" ) = 48. Further notice that ite( x=0, 49, 48 )
+    // enforces that int.to.str( n ) has no leading zeroes.
+    retNode = itost;
   } else if( t.getKind() == kind::STRING_STOI ) {
     Node str = t[0];
     Node pret = nm->mkSkolem("stoit", nm->integerType(), "created for stoi");