From 55c7c653812e8d9ee68739b38e1bacb67a44d64d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 16 Oct 2018 12:03:34 -0500 Subject: [PATCH] Improve reduction for int.to.str (#2629) --- .../strings/theory_strings_preprocess.cpp | 178 ++++++++---------- 1 file changed, 80 insertions(+), 98 deletions(-) diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index ba6caaf79..bdb339324 100644 --- 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 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"); -- 2.30.2