Fix for itos reduction (#2691)

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index fcb02d0589cbc0e9d65650ffe74bde87f5478e72..a1b37e6fb2781825bcaac2b17fc825c6f865f454 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -192,7 +192,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node ud =
         nm->mkSkolem("Ud", nm->mkFunctionType(argTypes, nm->stringType()));
 
-    Node lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni));
+    Node lem = nm->mkNode(GEQ, leni, d_one);
+    conc.push_back(lem);
+
+    lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni));
     conc.push_back(lem);
 
     lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
@@ -205,23 +208,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     conc.push_back(lem);
 
     Node x = nm->mkBoundVar(nm->integerType());
+    Node xPlusOne = nm->mkNode(PLUS, x, d_one);
     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 ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
     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 usx1 = nm->mkNode(APPLY_UF, us, xPlusOne);
 
     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 leadingZeroPos =
+        nm->mkNode(AND, x.eqNode(d_zero), nm->mkNode(GT, leni, d_one));
     Node cb = nm->mkNode(
         AND,
-        nm->mkNode(GEQ, c, nm->mkNode(ITE, x.eqNode(d_zero), d_one, d_zero)),
+        nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)),
         nm->mkNode(LT, c, ten));
 
     lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb));
@@ -236,12 +242,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     // assert:
     // IF n>=0
     // THEN:
+    //   len( itost ) >= 1 ^
     //   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
+    //     ite( x=0 AND str.len(itost)>1, 49, 48 ) <= str.code( Ud( x ) ) < 58
     // ELSE
     //   itost = ""
     // thus:
@@ -254,7 +261,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     // 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 )
+    // note that str.code( "0" ) = 48. Further notice that
+    //   ite( x=0 AND str.len(itost)>1, 49, 48 )
     // enforces that int.to.str( n ) has no leading zeroes.
     retNode = itost;
   } else if( t.getKind() == kind::STRING_STOI ) {