diff options
Diffstat (limited to 'src/theory/strings/theory_strings_preprocess.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 457 |
1 files changed, 324 insertions, 133 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 939146a3d..af946567b 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -2,9 +2,9 @@ /*! \file theory_strings_preprocess.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tianyi Liang + ** Andrew Reynolds, Andres Noetzli, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -38,48 +38,45 @@ StringsPreprocess::StringsPreprocess(SkolemCache* sc, SequencesStatistics& stats) : d_sc(sc), d_statistics(stats) { - //Constants - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); - d_one = NodeManager::currentNM()->mkConst(Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); } StringsPreprocess::~StringsPreprocess(){ } -Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { - unsigned prev_new_nodes = new_nodes.size(); - Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl; +Node StringsPreprocess::reduce(Node t, + std::vector<Node>& asserts, + SkolemCache* sc) +{ + Trace("strings-preprocess-debug") + << "StringsPreprocess::reduce: " << t << std::endl; Node retNode = t; - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); + Node zero = nm->mkConst(Rational(0)); + Node one = nm->mkConst(Rational(1)); + Node negOne = nm->mkConst(Rational(-1)); if( t.getKind() == kind::STRING_SUBSTR ) { // processing term: substr( s, n, m ) Node s = t[0]; Node n = t[1]; Node m = t[2]; - Node skt = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); + Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); Node t12 = nm->mkNode(PLUS, n, m); t12 = Rewriter::rewrite(t12); Node lt0 = nm->mkNode(STRING_LENGTH, s); //start point is greater than or equal zero - Node c1 = nm->mkNode(GEQ, n, d_zero); + Node c1 = nm->mkNode(GEQ, n, zero); //start point is less than end of string Node c2 = nm->mkNode(GT, lt0, n); //length is positive - Node c3 = nm->mkNode(GT, m, d_zero); + Node c3 = nm->mkNode(GT, m, zero); Node cond = nm->mkNode(AND, c1, c2, c3); Node emp = Word::mkEmptyWord(t.getType()); - Node sk1 = n == d_zero ? emp - : d_sc->mkSkolemCached( - s, n, SkolemCache::SK_PREFIX, "sspre"); - Node sk2 = ArithEntail::check(t12, lt0) - ? emp - : d_sc->mkSkolemCached( - s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); + Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); + Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2)); //length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); @@ -89,7 +86,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node b13 = nm->mkNode( OR, nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))), - nm->mkNode(EQUAL, lsk2, d_zero)); + nm->mkNode(EQUAL, lsk2, zero)); // Length of the result is at most m Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m); @@ -112,7 +109,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // satisfied. If n + m is less than the length of s, then len(sk2) = 0 // cannot be satisfied because we have the constraint that len(skt) <= m, // so sk2 must be greater than 0. - new_nodes.push_back( lemma ); + asserts.push_back(lemma); // Thus, substr( s, n, m ) = skt retNode = skt; @@ -123,15 +120,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x = t[0]; Node y = t[1]; Node n = t[2]; - Node skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof"); + Node skk = sc->mkTypedSkolemCached( + nm->integerType(), t, SkolemCache::SK_PURIFY, "iok"); Node negone = nm->mkConst(Rational(-1)); Node krange = nm->mkNode(GEQ, skk, negone); // assert: indexof( x, y, n ) >= -1 - new_nodes.push_back( krange ); + asserts.push_back(krange); krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk); // assert: len( x ) >= indexof( x, y, z ) - new_nodes.push_back( krange ); + asserts.push_back(krange); // substr( x, n, len( x ) - n ) Node st = nm->mkNode(STRING_SUBSTR, @@ -139,16 +137,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n)); Node io2 = - d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); + sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); Node io4 = - d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost"); + sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost"); // ~contains( substr( x, n, len( x ) - n ), y ) Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate(); // n > len( x ) Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x)); // 0 > n - Node c13 = nm->mkNode(GT, d_zero, n); + Node c13 = nm->mkNode(GT, zero, n); Node cond1 = nm->mkNode(OR, c11, c12, c13); // skk = -1 Node cc1 = skk.eqNode(negone); @@ -171,8 +169,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { nm->mkNode( STRING_SUBSTR, y, - d_zero, - nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), d_one))), + zero, + nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))), y) .negate(); // skk = n + len( io2 ) @@ -189,7 +187,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // skk = n + len( io2 ) // for fresh io2, io4. Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3)); - new_nodes.push_back( rr ); + asserts.push_back(rr); // Thus, indexof( x, y, n ) = skk. retNode = skk; @@ -198,7 +196,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { { // processing term: int.to.str( n ) Node n = t[0]; - Node itost = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost"); + Node itost = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost"); Node leni = nm->mkNode(STRING_LENGTH, itost); std::vector<Node> conc; @@ -206,21 +204,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { argTypes.push_back(nm->integerType()); Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); - Node lem = nm->mkNode(GEQ, leni, d_one); + Node lem = nm->mkNode(GEQ, leni, 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)); + lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero)); conc.push_back(lem); - Node x = nm->mkBoundVar(nm->integerType()); - Node xPlusOne = nm->mkNode(PLUS, x, d_one); + Node x = SkolemCache::mkIndexVar(t); + Node xPlusOne = nm->mkNode(PLUS, x, 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 sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one); + Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni)); + Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); @@ -229,10 +226,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node ten = nm->mkConst(Rational(10)); 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)); + nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one)); Node cb = nm->mkNode( AND, - nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)), + nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, one, zero)), nm->mkNode(LT, c, ten)); Node ux1lem = nm->mkNode(GEQ, n, ux1); @@ -241,11 +238,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = nm->mkNode(FORALL, xbv, lem); conc.push_back(lem); - Node nonneg = nm->mkNode(GEQ, n, d_zero); + Node nonneg = nm->mkNode(GEQ, n, zero); Node emp = Word::mkEmptyWord(t.getType()); lem = nm->mkNode(ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(emp)); - new_nodes.push_back(lem); + asserts.push_back(lem); // assert: // IF n>=0 // THEN: @@ -274,26 +271,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { retNode = itost; } else if( t.getKind() == kind::STRING_STOI ) { Node s = t[0]; - Node stoit = nm->mkSkolem("stoit", nm->integerType(), "created for stoi"); + Node stoit = sc->mkTypedSkolemCached( + nm->integerType(), t, SkolemCache::SK_PURIFY, "stoit"); Node lens = nm->mkNode(STRING_LENGTH, s); std::vector<Node> conc1; - Node lem = stoit.eqNode(d_neg_one); + Node lem = stoit.eqNode(negOne); conc1.push_back(lem); Node emp = Word::mkEmptyWord(s.getType()); Node sEmpty = s.eqNode(emp); Node k = nm->mkSkolem("k", nm->integerType()); - Node kc1 = nm->mkNode(GEQ, k, d_zero); + Node kc1 = nm->mkNode(GEQ, k, zero); Node kc2 = nm->mkNode(LT, k, lens); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); Node codeSk = nm->mkNode( MINUS, - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)), + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)), c0); Node ten = nm->mkConst(Rational(10)); Node kc3 = nm->mkNode( - OR, nm->mkNode(LT, codeSk, d_zero), nm->mkNode(GEQ, codeSk, ten)); + OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten)); conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3))); std::vector<Node> conc2; @@ -304,24 +302,22 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens)); conc2.push_back(lem); - lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero)); + lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero)); conc2.push_back(lem); - lem = nm->mkNode(GT, lens, d_zero); + lem = nm->mkNode(GT, lens, zero); conc2.push_back(lem); - Node x = nm->mkBoundVar(nm->integerType()); + Node x = SkolemCache::mkIndexVar(t); 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 sx = nm->mkNode(STRING_SUBSTR, s, x, d_one); + Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens)); + Node sx = nm->mkNode(STRING_SUBSTR, s, x, one); 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, nm->mkNode(PLUS, x, one)); Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); 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)); + Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten)); Node ux1lem = nm->mkNode(GEQ, stoit, ux1); @@ -329,9 +325,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = nm->mkNode(FORALL, xbv, lem); conc2.push_back(lem); - Node sneg = nm->mkNode(LT, stoit, d_zero); + Node sneg = nm->mkNode(LT, stoit, zero); lem = nm->mkNode(ITE, sneg, nm->mkNode(AND, conc1), nm->mkNode(AND, conc2)); - new_nodes.push_back(lem); + asserts.push_back(lem); // assert: // IF stoit < 0 @@ -362,10 +358,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node z = t[2]; TypeNode tn = t[0].getType(); Node rp1 = - d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre"); + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre"); Node rp2 = - d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost"); - Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw"); + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost"); + Node rpw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw"); // y = "" Node emp = Word::mkEmptyWord(tn); @@ -387,10 +383,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { rp1, nm->mkNode(kind::STRING_SUBSTR, y, - d_zero, + zero, nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, y), - d_one))), + one))), y) .negate(); @@ -410,7 +406,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { cond2, nm->mkNode(kind::AND, c21, c22, c23), rpw.eqNode(x))); - new_nodes.push_back( rr ); + asserts.push_back(rr); // Thus, replace( x, y, z ) = rpw. retNode = rpw; @@ -421,16 +417,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x = t[0]; Node y = t[1]; Node z = t[2]; - Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw"); + Node rpaw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw"); - Node numOcc = d_sc->mkTypedSkolemCached( + Node numOcc = sc->mkTypedSkolemCached( nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc"); std::vector<TypeNode> argTypes; argTypes.push_back(nm->integerType()); Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType())); TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType()); - Node uf = d_sc->mkTypedSkolemCached( + Node uf = sc->mkTypedSkolemCached( ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf"); Node ufno = nm->mkNode(APPLY_UF, uf, numOcc); @@ -438,27 +434,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x)); std::vector<Node> lem; - lem.push_back(nm->mkNode(GEQ, numOcc, d_zero)); - lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, d_zero))); + lem.push_back(nm->mkNode(GEQ, numOcc, zero)); + lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, zero))); lem.push_back(usno.eqNode(rem)); - lem.push_back(nm->mkNode(APPLY_UF, uf, d_zero).eqNode(d_zero)); - lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(d_neg_one)); + lem.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero)); + lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(negOne)); - Node i = nm->mkBoundVar(nm->integerType()); + Node i = SkolemCache::mkIndexVar(t); Node bvli = nm->mkNode(BOUND_VAR_LIST, i); Node bound = - nm->mkNode(AND, nm->mkNode(GEQ, i, d_zero), nm->mkNode(LT, i, numOcc)); + nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc)); Node ufi = nm->mkNode(APPLY_UF, uf, i); - Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, d_one)); + Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one)); Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi); Node cc = nm->mkNode( STRING_CONCAT, nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)), z, - nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, d_one))); + nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one))); std::vector<Node> flem; - flem.push_back(ii.eqNode(d_neg_one).negate()); + flem.push_back(ii.eqNode(negOne).negate()); flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc)); flem.push_back( ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y)))); @@ -487,27 +483,194 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node emp = Word::mkEmptyWord(t.getType()); Node assert = nm->mkNode(ITE, y.eqNode(emp), rpaw.eqNode(x), nm->mkNode(AND, lem)); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, replaceall( x, y, z ) = rpaw retNode = rpaw; } + else if (t.getKind() == STRING_REPLACE_RE) + { + Node x = t[0]; + Node y = t[1]; + Node z = t[2]; + Node k = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "k"); + + std::vector<Node> emptyVec; + Node sigmaStar = + nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec)); + Node re = nm->mkNode(REGEXP_CONCAT, sigmaStar, y, sigmaStar); + // in_re(x, re.++(_*, y, _*)) + Node hasMatch = nm->mkNode(STRING_IN_REGEXP, x, re); + + // in_re("", y) + Node matchesEmpty = + nm->mkNode(STRING_IN_REGEXP, nm->mkConst(String("")), y); + // k = z ++ x + Node res1 = k.eqNode(nm->mkNode(STRING_CONCAT, z, x)); + + Node k1 = + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_MATCH_PRE, "rre_pre"); + Node k2 = + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_MATCH, "rre_match"); + Node k3 = + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_MATCH_POST, "rre_post"); + // x = k1 ++ k2 ++ k3 + Node splitX = x.eqNode(nm->mkNode(STRING_CONCAT, k1, k2, k3)); + // ~in_re(k1 ++ str.substr(k2, 0, str.len(k2) - 1), re.++(_*, y, _*)) + Node k2len = nm->mkNode(STRING_LENGTH, k2); + Node firstMatch = + nm->mkNode( + STRING_IN_REGEXP, + nm->mkNode( + STRING_CONCAT, + k1, + nm->mkNode( + STRING_SUBSTR, k2, zero, nm->mkNode(MINUS, k2len, one))), + re) + .negate(); + // in_re(k2, y) + Node k2Match = nm->mkNode(STRING_IN_REGEXP, k2, y); + // k = k1 ++ z ++ k3 + Node res2 = k.eqNode(nm->mkNode(STRING_CONCAT, k1, z, k3)); + + // IF in_re(x, re.++(_*, y, _*)) + // THEN: + // IF in_re("", y) + // THEN: k = z ++ x + // ELSE: + // x = k1 ++ k2 ++ k3 ^ + // ~in_re(k1 ++ substr(k2, 0, str.len(k2) - 1), re.++(_*, y, _*)) ^ + // in_re(k2, y) ^ k = k1 ++ z ++ k3 + // ELSE: k = x + asserts.push_back(nm->mkNode( + ITE, + hasMatch, + nm->mkNode(ITE, + matchesEmpty, + res1, + nm->mkNode(AND, splitX, firstMatch, k2Match, res2)), + k.eqNode(x))); + retNode = k; + } + else if (t.getKind() == STRING_REPLACE_RE_ALL) + { + Node x = t[0]; + Node y = t[1]; + Node z = t[2]; + Node k = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "k"); + + Node numOcc = sc->mkTypedSkolemCached( + nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc"); + std::vector<TypeNode> argTypes; + argTypes.push_back(nm->integerType()); + Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, t.getType())); + TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType()); + Node uf = sc->mkTypedSkolemCached( + ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf"); + Node ul = + sc->mkTypedSkolemCached(ufType, x, y, SkolemCache::SK_OCCUR_LEN, "Ul"); + + Node emp = Word::mkEmptyWord(t.getType()); + + std::vector<Node> emptyVec; + Node sigmaStar = + nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec)); + Node yp = nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp)); + Node re = nm->mkNode(REGEXP_CONCAT, sigmaStar, yp, sigmaStar); + // in_re(x, _* ++ y' ++ _*) + Node hasMatch = nm->mkNode(STRING_IN_REGEXP, x, re); + + Node ufno = nm->mkNode(APPLY_UF, uf, numOcc); + Node usno = nm->mkNode(APPLY_UF, us, numOcc); + Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x)); + + std::vector<Node> lemmas; + // numOcc > 0 + lemmas.push_back(nm->mkNode(GT, numOcc, zero)); + // k = Us(0) + lemmas.push_back(k.eqNode(nm->mkNode(APPLY_UF, us, zero))); + // Us(numOcc) = substr(x, Uf(numOcc)) + lemmas.push_back(usno.eqNode(rem)); + // Uf(0) = 0 + lemmas.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero)); + // not(in_re(substr(x, Uf(numOcc)), re.++(_*, y', _*))) + lemmas.push_back(nm->mkNode(STRING_IN_REGEXP, rem, re).negate()); + + Node i = SkolemCache::mkIndexVar(t); + Node bvli = nm->mkNode(BOUND_VAR_LIST, i); + Node bound = + nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc)); + Node ip1 = nm->mkNode(PLUS, i, one); + Node ufi = nm->mkNode(APPLY_UF, uf, i); + Node uli = nm->mkNode(APPLY_UF, ul, i); + Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1); + Node ii = nm->mkNode(MINUS, ufip1, uli); + Node match = nm->mkNode(STRING_SUBSTR, x, ii, uli); + Node pfxMatch = + nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)); + Node nonMatch = + nm->mkNode(STRING_SUBSTR, + x, + ufi, + nm->mkNode(MINUS, nm->mkNode(MINUS, ufip1, one), ufi)); + + std::vector<Node> flem; + // Ul(i) > 0 + flem.push_back(nm->mkNode(GT, uli, zero)); + // Uf(i + 1) >= Uf(i) + Ul(i) + flem.push_back(nm->mkNode(GEQ, ufip1, nm->mkNode(PLUS, ufi, uli))); + // in_re(substr(x, ii, Ul(i)), y') + flem.push_back(nm->mkNode(STRING_IN_REGEXP, match, yp)); + // ~in_re(substr(x, Uf(i), Uf(i + 1) - 1 - Uf(i)), re.++(_*, y', _*)) + flem.push_back(nm->mkNode(STRING_IN_REGEXP, nonMatch, re).negate()); + // Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1) + flem.push_back( + nm->mkNode(APPLY_UF, us, i) + .eqNode(nm->mkNode( + STRING_CONCAT, pfxMatch, z, nm->mkNode(APPLY_UF, us, ip1)))); + + Node forall = nm->mkNode( + FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem))); + lemmas.push_back(forall); + + // IF in_re(x, re.++(_*, y', _*)) + // THEN: + // numOcc > 0 ^ + // k = Us(0) ^ Us(numOcc) = substr(x, Uf(numOcc)) ^ + // Uf(0) = 0 ^ not(in_re(substr(x, Uf(numOcc)), re.++(_*, y', _*))) + // forall i. 0 <= i < nummOcc => + // Ul(i) > 0 ^ + // Uf(i + 1) >= Uf(i) + Ul(i) ^ + // in_re(substr(x, ii, Ul(i)), y') ^ + // ~in_re(substr(x, Uf(i), Uf(i + 1) - 1 - Uf(i)), re.++(_*, y', _*)) ^ + // Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1) + // where ii = Uf(i + 1) - Ul(i) + // ELSE: k = x + // where y' = re.diff(y, "") + // + // Conceptually, y' is the regex y but excluding the empty string (because + // we do not want to match empty strings), numOcc is the number of shortest + // matches of y' in x, Uf(i) is the end position of the i-th match, Ul(i) + // is the length of the i^th match, and Us(i) is the result of processing + // the remainder after processing the i^th occurrence of y in x. + asserts.push_back( + nm->mkNode(ITE, hasMatch, nm->mkNode(AND, lemmas), k.eqNode(x))); + retNode = k; + } else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER) { Node x = t[0]; - Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); + Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); Node lenx = nm->mkNode(STRING_LENGTH, x); Node lenr = nm->mkNode(STRING_LENGTH, r); Node eqLenA = lenx.eqNode(lenr); - Node i = nm->mkBoundVar(nm->integerType()); + Node i = SkolemCache::mkIndexVar(t); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); - Node ci = - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one)); - Node ri = - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one)); + Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one)); + Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one)); Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); @@ -521,7 +684,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { ci); Node bound = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr)); + nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr)); Node rangeA = nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res))); @@ -533,7 +696,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // str.code( str.substr(r,i,1) ) = ite( 97 <= ci <= 122, ci-32, ci) // where ci = str.code( str.substr(x,i,1) ) Node assert = nm->mkNode(AND, eqLenA, rangeA); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, toLower( x ) = r retNode = r; @@ -541,22 +704,22 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { else if (t.getKind() == STRING_REV) { Node x = t[0]; - Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); + Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); Node lenx = nm->mkNode(STRING_LENGTH, x); Node lenr = nm->mkNode(STRING_LENGTH, r); Node eqLenA = lenx.eqNode(lenr); - Node i = nm->mkBoundVar(nm->integerType()); + Node i = SkolemCache::mkIndexVar(t); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); Node revi = nm->mkNode( - MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, d_one)); - Node ssr = nm->mkNode(STRING_SUBSTR, r, i, d_one); - Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, d_one); + MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one)); + Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one); + Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one); Node bound = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr)); + nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr)); Node rangeA = nm->mkNode( FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx))); // assert: @@ -564,7 +727,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // forall i. 0 <= i < len(r) => // substr(r,i,1) = substr(x,len(x)-(i+1),1) Node assert = nm->mkNode(AND, eqLenA, rangeA); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, (str.rev x) = r retNode = r; @@ -576,31 +739,38 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { //negative contains reduces to existential Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); - Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); + Node b1 = SkolemCache::mkIndexVar(t); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); - Node body = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::LEQ, d_zero, b1 ), - NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ), - NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s ) - ); + Node body = NodeManager::currentNM()->mkNode( + kind::AND, + NodeManager::currentNM()->mkNode(kind::LEQ, zero, b1), + NodeManager::currentNM()->mkNode( + kind::LEQ, + b1, + NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)), + NodeManager::currentNM()->mkNode( + kind::EQUAL, + NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), + s)); retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body ); } else if (t.getKind() == kind::STRING_LEQ) { - Node ltp = nm->mkSkolem("ltp", nm->booleanType()); + Node ltp = sc->mkTypedSkolemCached( + nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp"); Node k = nm->mkSkolem("k", nm->integerType()); std::vector<Node> conj; - conj.push_back(nm->mkNode(GEQ, k, d_zero)); + conj.push_back(nm->mkNode(GEQ, k, zero)); Node substr[2]; Node code[2]; for (unsigned r = 0; r < 2; r++) { Node ta = t[r]; Node tb = t[1 - r]; - substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k); + substr[r] = nm->mkNode(STRING_SUBSTR, ta, zero, k); code[r] = - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one)); + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, one)); conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta))); } conj.push_back(substr[0].eqNode(substr[1])); @@ -632,18 +802,29 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 )) Node assert = nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj)); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, str.<=( x, y ) = ltp retNode = ltp; } + return retNode; +} +Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts) +{ + size_t prev_asserts = asserts.size(); + // call the static reduce routine + Node retNode = reduce(t, asserts, d_sc); if( t!=retNode ){ Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl; - if(!new_nodes.empty()) { - Trace("strings-preprocess") << " ... new nodes (" << (new_nodes.size()-prev_new_nodes) << "):" << std::endl; - for(unsigned int i=prev_new_nodes; i<new_nodes.size(); ++i) { - Trace("strings-preprocess") << " " << new_nodes[i] << std::endl; + if (!asserts.empty()) + { + Trace("strings-preprocess") + << " ... new nodes (" << (asserts.size() - prev_asserts) + << "):" << std::endl; + for (size_t i = prev_asserts; i < asserts.size(); ++i) + { + Trace("strings-preprocess") << " " << asserts[i] << std::endl; } } d_statistics.d_reductions << t.getKind(); @@ -656,14 +837,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return retNode; } -Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, std::map< Node, Node >& visited ){ +Node StringsPreprocess::simplifyRec(Node t, + std::vector<Node>& asserts, + std::map<Node, Node>& visited) +{ std::map< Node, Node >::iterator it = visited.find(t); if( it!=visited.end() ){ return it->second; }else{ Node retNode = t; if( t.getNumChildren()==0 ){ - retNode = simplify( t, new_nodes ); + retNode = simplify(t, asserts); }else if( t.getKind()!=kind::FORALL ){ bool changed = false; std::vector< Node > cc; @@ -671,7 +855,7 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st cc.push_back( t.getOperator() ); } for(unsigned i=0; i<t.getNumChildren(); i++) { - Node s = simplifyRec( t[i], new_nodes, visited ); + Node s = simplifyRec(t[i], asserts, visited); cc.push_back( s ); if( s!=t[i] ) { changed = true; @@ -681,24 +865,27 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st if( changed ){ tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); } - retNode = simplify( tmp, new_nodes ); + retNode = simplify(tmp, asserts); } visited[t] = retNode; return retNode; } } -Node StringsPreprocess::processAssertion( Node n, std::vector< Node > &new_nodes ) { +Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts) +{ std::map< Node, Node > visited; - std::vector< Node > new_nodes_curr; - Node ret = simplifyRec( n, new_nodes_curr, visited ); - while( !new_nodes_curr.empty() ){ - Node curr = new_nodes_curr.back(); - new_nodes_curr.pop_back(); - std::vector< Node > new_nodes_tmp; - curr = simplifyRec( curr, new_nodes_tmp, visited ); - new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() ); - new_nodes.push_back( curr ); + std::vector<Node> asserts_curr; + Node ret = simplifyRec(n, asserts_curr, visited); + while (!asserts_curr.empty()) + { + Node curr = asserts_curr.back(); + asserts_curr.pop_back(); + std::vector<Node> asserts_tmp; + curr = simplifyRec(curr, asserts_tmp, visited); + asserts_curr.insert( + asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end()); + asserts.push_back(curr); } return ret; } @@ -708,18 +895,22 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ for( unsigned i=0; i<vec_node.size(); i++ ){ Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl; //preprocess until fixed point - std::vector< Node > new_nodes; - std::vector< Node > new_nodes_curr; - new_nodes_curr.push_back( vec_node[i] ); - while( !new_nodes_curr.empty() ){ - Node curr = new_nodes_curr.back(); - new_nodes_curr.pop_back(); - std::vector< Node > new_nodes_tmp; - curr = simplifyRec( curr, new_nodes_tmp, visited ); - new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() ); - new_nodes.push_back( curr ); + std::vector<Node> asserts; + std::vector<Node> asserts_curr; + asserts_curr.push_back(vec_node[i]); + while (!asserts_curr.empty()) + { + Node curr = asserts_curr.back(); + asserts_curr.pop_back(); + std::vector<Node> asserts_tmp; + curr = simplifyRec(curr, asserts_tmp, visited); + asserts_curr.insert( + asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end()); + asserts.push_back(curr); } - Node res = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + Node res = asserts.size() == 1 + ? asserts[0] + : NodeManager::currentNM()->mkNode(kind::AND, asserts); if( res!=vec_node[i] ){ res = Rewriter::rewrite( res ); PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); ); |