From b9fed18079d1dca67739796bf1110268c070c307 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 18 Oct 2018 11:58:51 -0500 Subject: [PATCH] Improve reduction for str.to.int (#2636) --- .../strings/theory_strings_preprocess.cpp | 179 ++++++++---------- .../strings/theory_strings_preprocess.h | 1 + test/regress/CMakeLists.txt | 1 + test/regress/Makefile.tests | 1 + .../regress1/strings/stoi-400million.smt2 | 7 + 5 files changed, 93 insertions(+), 96 deletions(-) create mode 100644 test/regress/regress1/strings/stoi-400million.smt2 diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index bdb339324..fcb02d058 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -37,6 +37,7 @@ StringsPreprocess::StringsPreprocess(SkolemCache *sc, context::UserContext *u) //Constants d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); d_empty_str = NodeManager::currentNM()->mkConst(String("")); } @@ -257,104 +258,90 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // 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"); - Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str); - - Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); - Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); + Node s = t[0]; + Node stoit = nm->mkSkolem("stoit", nm->integerType(), "created for stoi"); + Node lens = nm->mkNode(STRING_LENGTH, s); + + std::vector conc1; + Node lem = stoit.eqNode(d_neg_one); + conc1.push_back(lem); + + Node sEmpty = s.eqNode(d_empty_str); + Node k = nm->mkSkolem("k", nm->integerType()); + Node kc1 = nm->mkNode(GEQ, k, d_zero); + Node kc2 = nm->mkNode(LT, k, lens); + Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0"))); + Node codeSk = nm->mkNode( + MINUS, + nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)), + c0); + Node ten = nm->mkConst(Rational(10)); + Node kc3 = nm->mkNode( + OR, nm->mkNode(LT, codeSk, d_zero), nm->mkNode(GEQ, codeSk, ten)); + conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3))); + + std::vector conc2; 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"); - - //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(""))), - pret.eqNode(negone)); + 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())); + + lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens)); + conc2.push_back(lem); + + lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero)); + conc2.push_back(lem); + + lem = d_empty_str.eqNode(nm->mkNode(APPLY_UF, us, lens)); + conc2.push_back(lem); + + lem = s.eqNode(nm->mkNode(APPLY_UF, us, d_zero)); + conc2.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, lens)); + 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 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 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, 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); + conc2.push_back(lem); + + Node sneg = nm->mkNode(LT, stoit, d_zero); + lem = nm->mkNode(ITE, sneg, nm->mkNode(AND, conc1), nm->mkNode(AND, conc2)); new_nodes.push_back(lem); - /*lem = NodeManager::currentNM()->mkNode(kind::EQUAL, - t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))), - t.eqNode(d_zero)); - new_nodes.push_back(lem);*/ - //cc1 - 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 p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType()); - Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero); - vec_n.push_back(g); - g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p); - vec_n.push_back(g); - Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, str, p, one); - char chtmp[2]; - chtmp[1] = '\0'; - for(unsigned i=0; i<=9; i++) { - chtmp[0] = i + '0'; - std::string stmp(chtmp); - g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate(); - vec_n.push_back(g); - } - Node cc2 = NodeManager::currentNM()->mkNode(kind::AND, vec_n); - //cc3 - Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2); - Node g2 = NodeManager::currentNM()->mkNode(kind::AND, - NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero), - NodeManager::currentNM()->mkNode(kind::GT, lenp, b2)); - 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); - 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, str, b2, one); - for(unsigned i=0; i<=9; i++) { - chtmp[0] = i + '0'; - std::string stmp(chtmp); - c3cc = NodeManager::currentNM()->mkNode(kind::EQUAL, - 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); - 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 = 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 ); - retNode = pret; + + // assert: + // IF stoit < 0 + // THEN: + // stoit = -1 ^ + // ( s = "" OR + // ( k>=0 ^ k= 58 ))) + // ELSE: + // stoit = U( len( s ) ) ^ U( 0 ) = 0 ^ + // "" = Us( len( s ) ) ^ s = Us( 0 ) ^ + // forall x. (x>=0 ^ x < str.len(s)) => + // Us( x ) = Ud( x ) ++ Us( x+1 ) ^ + // U( x+1 ) = ( str.code( Ud( x ) ) - 48 ) + 10*U( x ) + // 48 <= str.code( Ud( x ) ) < 58 + // Thus, str.to.int( s ) = stoit + + retNode = stoit; } else if (t.getKind() == kind::STRING_STRREPL) { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index c670a5483..ff0195dc1 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -68,6 +68,7 @@ private: /** commonly used constants */ Node d_zero; Node d_one; + Node d_neg_one; Node d_empty_str; /** pointer to the skolem cache used by this class */ SkolemCache *d_sc; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cd95c6653..59edb6986 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1535,6 +1535,7 @@ set(regress_1_tests regress1/strings/repl-empty-sem.smt2 regress1/strings/repl-soundness-sem.smt2 regress1/strings/rew-020618.smt2 + regress1/strings/stoi-400million.smt2 regress1/strings/str-code-sat.smt2 regress1/strings/str-code-unsat-2.smt2 regress1/strings/str-code-unsat-3.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b4e151a17..194a4ddaf 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1532,6 +1532,7 @@ REG1_TESTS = \ regress1/strings/repl-empty-sem.smt2 \ regress1/strings/repl-soundness-sem.smt2 \ regress1/strings/rew-020618.smt2 \ + regress1/strings/stoi-400million.smt2 \ regress1/strings/str-code-sat.smt2 \ regress1/strings/str-code-unsat-2.smt2 \ regress1/strings/str-code-unsat-3.smt2 \ diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2 new file mode 100644 index 000000000..9b9acf673 --- /dev/null +++ b/test/regress/regress1/strings/stoi-400million.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(declare-fun s () String) +(assert (> (str.to.int s) 400000000)) +(check-sat) -- 2.30.2