From 2c05402119dba7e90e24621c5768514ab2f5042c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 21 Nov 2018 14:44:44 -0600 Subject: [PATCH] Support string replace all (#2704) --- src/parser/cvc/Cvc.g | 3 + src/parser/smt2/smt2.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 2 + src/theory/datatypes/datatypes_sygus.cpp | 4 +- src/theory/strings/kinds | 2 + src/theory/strings/skolem_cache.cpp | 34 ++++-- src/theory/strings/skolem_cache.h | 19 ++++ src/theory/strings/theory_strings.cpp | 9 +- .../strings/theory_strings_preprocess.cpp | 78 +++++++++++++- .../strings/theory_strings_rewriter.cpp | 101 +++++++++++++++--- src/theory/strings/theory_strings_rewriter.h | 12 +++ test/regress/CMakeLists.txt | 5 + .../regress0/strings/replaceall-eval.smt2 | 10 ++ .../regress1/strings/replaceall-len.smt2 | 10 ++ .../regress1/strings/replaceall-replace.smt2 | 13 +++ .../strings/replaceall-diffrange.smt2 | 11 ++ .../regress2/strings/replaceall-len-c.smt2 | 8 ++ 17 files changed, 296 insertions(+), 26 deletions(-) create mode 100644 test/regress/regress0/strings/replaceall-eval.smt2 create mode 100644 test/regress/regress1/strings/replaceall-len.smt2 create mode 100644 test/regress/regress1/strings/replaceall-replace.smt2 create mode 100644 test/regress/regress2/strings/replaceall-diffrange.smt2 create mode 100644 test/regress/regress2/strings/replaceall-len-c.smt2 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3eddf438f..29bc84510 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -222,6 +222,7 @@ tokens { STRING_CHARAT_TOK = 'CHARAT'; STRING_INDEXOF_TOK = 'INDEXOF'; STRING_REPLACE_TOK = 'REPLACE'; + STRING_REPLACE_ALL_TOK = 'REPLACE_ALL'; STRING_PREFIXOF_TOK = 'PREFIXOF'; STRING_SUFFIXOF_TOK = 'SUFFIXOF'; STRING_STOI_TOK = 'STRING_TO_INTEGER'; @@ -2028,6 +2029,8 @@ stringTerm[CVC4::Expr& f] { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); } | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN { f = MK_EXPR(CVC4::kind::STRING_STRREPL, f, f2, f3); } + | STRING_REPLACE_ALL_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_STRREPLALL, f, f2, f3); } | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::STRING_PREFIX, f, f2); } | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2fd61aabc..d52dd948b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -129,6 +129,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_CHARAT, "str.at" ); addOperator(kind::STRING_STRIDOF, "str.indexof" ); addOperator(kind::STRING_STRREPL, "str.replace" ); + addOperator(kind::STRING_STRREPLALL, "str.replaceall"); addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); // at the moment, we only use this syntax for smt2.6.1 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b71e9d4c4..259f23afc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -601,6 +601,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::STRING_STRCTN: case kind::STRING_STRIDOF: case kind::STRING_STRREPL: + case kind::STRING_STRREPLALL: case kind::STRING_PREFIX: case kind::STRING_SUFFIX: case kind::STRING_LEQ: @@ -1143,6 +1144,7 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_CHARAT: return "str.at" ; case kind::STRING_STRIDOF: return "str.indexof" ; case kind::STRING_STRREPL: return "str.replace" ; + case kind::STRING_STRREPLALL: return "str.replaceall"; case kind::STRING_PREFIX: return "str.prefixof" ; case kind::STRING_SUFFIX: return "str.suffixof" ; case kind::STRING_LEQ: return "str.<="; diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 4c7dcec9a..2fee4f48d 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -759,12 +759,12 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, deq_child[1].push_back(1); } } - if (nk == ITE || nk == STRING_STRREPL) + if (nk == ITE || nk == STRING_STRREPL || nk == STRING_STRREPLALL) { deq_child[0].push_back(1); deq_child[1].push_back(2); } - if (nk == STRING_STRREPL) + if (nk == STRING_STRREPL || nk == STRING_STRREPLALL) { deq_child[0].push_back(0); deq_child[1].push_back(1); diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 7fb2d26c6..df6085422 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -22,6 +22,7 @@ operator STRING_LT 2 "string less than" operator STRING_LEQ 2 "string less than or equal" operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" +operator STRING_STRREPLALL 3 "string replace all" operator STRING_PREFIX 2 "string prefixof" operator STRING_SUFFIX 2 "string suffixof" operator STRING_ITOS 1 "integer to string" @@ -93,6 +94,7 @@ typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule +typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 2b0cc8a1b..7725b1b0d 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -20,31 +20,51 @@ namespace CVC4 { namespace theory { namespace strings { -SkolemCache::SkolemCache() {} +SkolemCache::SkolemCache() +{ + d_strType = NodeManager::currentNM()->stringType(); +} Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c) +{ + return mkTypedSkolemCached(d_strType, a, b, id, c); +} + +Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c) +{ + return mkSkolemCached(a, Node::null(), id, c); +} + +Node SkolemCache::mkTypedSkolemCached( + TypeNode tn, Node a, Node b, SkolemId id, const char* c) { a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); std::map::iterator it = d_skolemCache[a][b].find(id); if (it == d_skolemCache[a][b].end()) { - Node sk = mkSkolem(c); + Node sk = mkTypedSkolem(tn, c); d_skolemCache[a][b][id] = sk; return sk; } return it->second; } - -Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c) +Node SkolemCache::mkTypedSkolemCached(TypeNode tn, + Node a, + SkolemId id, + const char* c) { - return mkSkolemCached(a, Node::null(), id, c); + return mkTypedSkolemCached(tn, a, Node::null(), id, c); } Node SkolemCache::mkSkolem(const char* c) { - NodeManager* nm = NodeManager::currentNM(); - Node n = nm->mkSkolem(c, nm->stringType(), "string skolem"); + return mkTypedSkolem(d_strType, c); +} + +Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c) +{ + Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem"); d_allSkolems.insert(n); return n; } diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 1cd4d7de8..d0eabd4c2 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -100,6 +100,16 @@ class SkolemCache // b > 0 => // exists k. a = a' ++ k ^ len( k ) = ite( len(a)>b, len(a)-b, 0 ) SK_SUFFIX_REM, + // --------------- integer skolems + // exists k. ( b occurs k times in a ) + SK_NUM_OCCUR, + // --------------- function skolems + // For function k: Int -> Int + // exists k. + // forall 0 <= x <= n, + // k(x) is the end index of the x^th occurrence of b in a + // where n is the number of occurrences of b in a, and k(0)=0. + SK_OCCUR_INDEX, }; /** * Returns a skolem of type string that is cached for (a,b,id) and has @@ -111,12 +121,21 @@ class SkolemCache * name c. */ Node mkSkolemCached(Node a, SkolemId id, const char* c); + /** Same as above, but the skolem to construct has a custom type tn */ + Node mkTypedSkolemCached( + TypeNode tn, Node a, Node b, SkolemId id, const char* c); + /** Same as mkTypedSkolemCached above for (a,[null],id) */ + Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c); /** Returns a (uncached) skolem of type string with name c */ Node mkSkolem(const char* c); + /** Same as above, but for custom type tn */ + Node mkTypedSkolem(TypeNode tn, const char* c); /** Returns true if n is a skolem allocated by this class */ bool isSkolem(Node n) const; private: + /** string type */ + TypeNode d_strType; /** map from node pairs and identifiers to skolems */ std::map > > d_skolemCache; /** the set of all skolems we have generated */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 883683f52..e8b753768 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -144,6 +144,7 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_ITOS); getExtTheory()->addFunctionKind(kind::STRING_STOI); getExtTheory()->addFunctionKind(kind::STRING_STRREPL); + getExtTheory()->addFunctionKind(kind::STRING_STRREPLALL); getExtTheory()->addFunctionKind(kind::STRING_STRCTN); getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); getExtTheory()->addFunctionKind(kind::STRING_LEQ); @@ -162,6 +163,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_STOI); d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF); d_equalityEngine.addFunctionKind(kind::STRING_STRREPL); + d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL); } d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); @@ -503,7 +505,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) NodeManager* nm = NodeManager::currentNM(); Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL - || k == STRING_LEQ); + || k == STRING_STRREPLALL || k == STRING_LEQ); std::vector new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); @@ -817,9 +819,8 @@ void TheoryStrings::preRegisterTerm(TNode n) { Kind k = n.getKind(); if( !options::stringExp() ){ if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS - || k == kind::STRING_STOI - || k == kind::STRING_STRREPL - || k == kind::STRING_STRCTN + || k == kind::STRING_STOI || k == kind::STRING_STRREPL + || k == kind::STRING_STRREPLALL || k == kind::STRING_STRCTN || k == STRING_LEQ) { std::stringstream ss; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a1b37e6fb..d095d6801 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -410,6 +410,82 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // Thus, replace( x, y, z ) = rpw. retNode = rpw; + } + else if (t.getKind() == kind::STRING_STRREPLALL) + { + // processing term: replaceall( x, y, z ) + Node x = t[0]; + Node y = t[1]; + Node z = t[2]; + Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw"); + + Node numOcc = d_sc->mkTypedSkolemCached( + nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc"); + std::vector 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( + ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf"); + + 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 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(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)); + + Node i = nm->mkBoundVar(nm->integerType()); + Node bvli = nm->mkNode(BOUND_VAR_LIST, i); + Node bound = + nm->mkNode(AND, nm->mkNode(GEQ, i, d_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 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))); + + std::vector flem; + flem.push_back(ii.eqNode(d_neg_one).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)))); + + Node q = nm->mkNode( + FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem))); + lem.push_back(q); + + // assert: + // IF y="" + // THEN: rpaw = x + // ELSE: + // numOcc >= 0 ^ + // rpaw = Us(0) ^ Us(numOcc) = substr(x, Uf(numOcc), len(x)) ^ + // Uf(0) = 0 ^ indexof( x, y, Uf(numOcc) ) = -1 ^ + // forall i. 0 <= i < numOcc => + // ii != -1 ^ + // Us( i ) = str.substr( x, Uf(i), ii - Uf(i) ) ++ z ++ Us(i+1) ^ + // Uf( i+1 ) = ii + len(y) + // where ii == indexof( x, y, Uf(i) ) + + // Conceptually, numOcc is the number of occurrences of y in x, Uf( i ) is + // the index to begin searching in x for y after the i^th occurrence of y in + // x, and Us( i ) is the result of processing the remainder after processing + // the i^th occurrence of y in x. + Node assert = nm->mkNode( + ITE, y.eqNode(d_empty_str), rpaw.eqNode(x), nm->mkNode(AND, lem)); + new_nodes.push_back(assert); + + // Thus, replaceall( x, y, z ) = rpaw + retNode = rpaw; } else if( t.getKind() == kind::STRING_STRCTN ){ Node x = t[0]; Node s = t[1]; @@ -474,7 +550,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj)); new_nodes.push_back(assert); - // Thus, str.<=( x, y ) = p_lt + // Thus, str.<=( x, y ) = ltp retNode = ltp; } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e94a23c87..b7821d562 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1392,9 +1392,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == kind::STRING_LENGTH) { + Kind nk0 = node[0].getKind(); if( node[0].isConst() ){ retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst().size() ) ); - }else if( node[0].getKind() == kind::STRING_CONCAT ){ + } + else if (nk0 == kind::STRING_CONCAT) + { Node tmpNode = node[0]; if(tmpNode.isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst().size() ) ); @@ -1410,7 +1413,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - else if (node[0].getKind() == STRING_STRREPL) + else if (nk0 == STRING_STRREPL || nk0 == STRING_STRREPLALL) { Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1])); Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2])); @@ -1453,6 +1456,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteReplace( node ); } + else if (nk == kind::STRING_STRREPLALL) + { + retNode = rewriteReplaceAll(node); + } else if (nk == kind::STRING_PREFIX || nk == kind::STRING_SUFFIX) { retNode = rewritePrefixSuffix(node); @@ -2437,16 +2444,6 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { Assert(node.getKind() == kind::STRING_STRREPL); NodeManager* nm = NodeManager::currentNM(); - if (node[1] == node[2]) - { - return returnRewrite(node, node[0], "rpl-id"); - } - - if (node[0] == node[1]) - { - return returnRewrite(node, node[2], "rpl-replace"); - } - if (node[1].isConst() && node[1].getConst().isEmptyString()) { Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]); @@ -2497,6 +2494,14 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { } } + // rewrites that apply to both replace and replaceall + Node rri = rewriteReplaceInternal(node); + if (!rri.isNull()) + { + // printing of the rewrite managed by the call above + return rri; + } + if (node[0] == node[2]) { // ( len( y )>=len(x) ) => str.replace( x, y, x ) ---> x @@ -2938,6 +2943,78 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return node; } +Node TheoryStringsRewriter::rewriteReplaceAll(Node node) +{ + Assert(node.getKind() == STRING_STRREPLALL); + NodeManager* nm = NodeManager::currentNM(); + + if (node[0].isConst() && node[1].isConst()) + { + std::vector children; + String s = node[0].getConst(); + String t = node[1].getConst(); + if (s.isEmptyString() || t.isEmptyString()) + { + return returnRewrite(node, node[0], "replall-empty-find"); + } + std::size_t index = 0; + std::size_t curr = 0; + do + { + curr = s.find(t, index); + if (curr != std::string::npos) + { + if (curr > index) + { + children.push_back(nm->mkConst(s.substr(index, curr - index))); + } + children.push_back(node[2]); + index = curr + t.size(); + } + else + { + children.push_back(nm->mkConst(s.substr(index, s.size() - index))); + } + } while (curr != std::string::npos && curr < s.size()); + // constant evaluation + Node res = mkConcat(STRING_CONCAT, children); + return returnRewrite(node, res, "replall-const"); + } + + // rewrites that apply to both replace and replaceall + Node rri = rewriteReplaceInternal(node); + if (!rri.isNull()) + { + // printing of the rewrite managed by the call above + return rri; + } + + Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; + return node; +} + +Node TheoryStringsRewriter::rewriteReplaceInternal(Node node) +{ + Kind nk = node.getKind(); + Assert(nk == STRING_STRREPL || nk == STRING_STRREPLALL); + + if (node[1] == node[2]) + { + return returnRewrite(node, node[0], "rpl-id"); + } + + if (node[0] == node[1]) + { + // only holds for replaceall if non-empty + if (nk == STRING_STRREPL || checkEntailNonEmpty(node[1])) + { + return returnRewrite(node, node[2], "rpl-replace"); + } + } + + return Node::null(); +} + Node TheoryStringsRewriter::rewriteStringLeq(Node n) { Assert(n.getKind() == kind::STRING_LEQ); diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 2e356f8f7..69d6ff68e 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -187,6 +187,18 @@ class TheoryStringsRewriter { * Returns the rewritten form of node. */ static Node rewriteReplace(Node node); + /** rewrite replace all + * This is the entry point for post-rewriting terms n of the form + * str.replaceall( s, t, r ) + * Returns the rewritten form of node. + */ + static Node rewriteReplaceAll(Node node); + /** rewrite replace internal + * + * This method implements rewrite rules that apply to both str.replace and + * str.replaceall. If it returns a non-null ret, then node rewrites to ret. + */ + static Node rewriteReplaceInternal(Node node); /** rewrite string less than or equal * This is the entry point for post-rewriting terms n of the form * str.<=( t, s ) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6736d712b..a1d5a35aa 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -825,6 +825,7 @@ set(regress_0_tests regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 regress0/strings/repl-rewrites2.smt2 + regress0/strings/replaceall-eval.smt2 regress0/strings/rewrites-re-concat.smt2 regress0/strings/rewrites-v2.smt2 regress0/strings/std2.6.1.smt2 @@ -1544,6 +1545,8 @@ set(regress_1_tests regress1/strings/reloop.smt2 regress1/strings/repl-empty-sem.smt2 regress1/strings/repl-soundness-sem.smt2 + regress1/strings/replaceall-len.smt2 + regress1/strings/replaceall-replace.smt2 regress1/strings/rew-020618.smt2 regress1/strings/stoi-400million.smt2 regress1/strings/str-code-sat.smt2 @@ -1729,6 +1732,8 @@ set(regress_2_tests regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 regress2/strings/repl-repl.smt2 + regress2/strings/replaceall-diffrange.smt2 + regress2/strings/replaceall-len-c.smt2 regress2/sygus/MPwL_d1s3.sy regress2/sygus/array_sum_dd.sy regress2/sygus/cegisunif-depth1-bv.sy diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2 new file mode 100644 index 000000000..924515901 --- /dev/null +++ b/test/regress/regress0/strings/replaceall-eval.smt2 @@ -0,0 +1,10 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) + +(assert (= x (str.replaceall "AABAABBC" "B" "def"))) +(assert (= y (str.replaceall "AABAABBC" "AB" "BA"))) + +(check-sat) diff --git a/test/regress/regress1/strings/replaceall-len.smt2 b/test/regress/regress1/strings/replaceall-len.smt2 new file mode 100644 index 000000000..448d8e98f --- /dev/null +++ b/test/regress/regress1/strings/replaceall-len.smt2 @@ -0,0 +1,10 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(set-option :strings-fmf true) +(set-option :produce-models true) +(declare-fun x () String) +(assert (= (str.len (str.replaceall x "B" "CC")) (+ (str.len x) 2))) +(assert (> (str.len x) 2)) +(check-sat) diff --git a/test/regress/regress1/strings/replaceall-replace.smt2 b/test/regress/regress1/strings/replaceall-replace.smt2 new file mode 100644 index 000000000..5bf5b5b16 --- /dev/null +++ b/test/regress/regress1/strings/replaceall-replace.smt2 @@ -0,0 +1,13 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(set-option :strings-fmf true) +(set-option :produce-models true) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(assert (not (= x ""))) +(assert (not (= y ""))) +(assert (not (= (str.replace x y z) (str.replaceall x y z)))) +(check-sat) diff --git a/test/regress/regress2/strings/replaceall-diffrange.smt2 b/test/regress/regress2/strings/replaceall-diffrange.smt2 new file mode 100644 index 000000000..5d1ef57bf --- /dev/null +++ b/test/regress/regress2/strings/replaceall-diffrange.smt2 @@ -0,0 +1,11 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(set-option :strings-fmf true) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(assert (= (str.len (str.replaceall x y z)) (+ (str.len (str.replaceall x y w)) 3))) +(check-sat) diff --git a/test/regress/regress2/strings/replaceall-len-c.smt2 b/test/regress/regress2/strings/replaceall-len-c.smt2 new file mode 100644 index 000000000..336ec10e4 --- /dev/null +++ b/test/regress/regress2/strings/replaceall-len-c.smt2 @@ -0,0 +1,8 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(set-option :strings-fmf true) +(declare-fun x () String) +(assert (= (str.len (str.replaceall "ABBABAAB" x "C")) 5)) +(check-sat) -- 2.30.2