From e2d714a0839fb80d9a40e9b6fdd8a6fe325a1664 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Mar 2018 20:36:17 -0600 Subject: [PATCH] Update semantics for string indexof and replace (#1630) --- src/theory/datatypes/datatypes_sygus.cpp | 2 +- .../strings/theory_strings_preprocess.cpp | 182 ++++++++++++------ .../strings/theory_strings_rewriter.cpp | 112 +++++------ src/theory/strings/theory_strings_rewriter.h | 42 +++- test/regress/regress0/strings/idof-sem.smt2 | 4 +- .../regress0/strings/repl-rewrites2.smt2 | 5 +- test/regress/regress1/strings/Makefile.am | 4 +- .../regress1/strings/double-replace.smt2 | 3 +- .../regress1/strings/repl-empty-sem.smt2 | 4 +- .../regress1/strings/repl-soundness-sem.smt2 | 4 +- test/regress/regress1/strings/rew-020618.smt2 | 2 +- .../regress1/strings/string-unsound-sem.smt2 | 12 ++ test/regress/regress2/strings/Makefile.am | 3 +- .../strings/cmu-disagree-0707-dd.smt2 | 0 14 files changed, 240 insertions(+), 139 deletions(-) create mode 100644 test/regress/regress1/strings/string-unsound-sem.smt2 rename test/regress/{regress1 => regress2}/strings/cmu-disagree-0707-dd.smt2 (100%) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 6f533bfe0..b8185e9c8 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -843,7 +843,7 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, Node pbv_e = its->second.evaluate(bvr, pt_index); Assert(bv_e != pbv_e); Trace("sygus-rr-debug") << "; unsound: where they evaluate to " - << pbv_e << " and " << bv_e << std::endl; + << bv_e << " and " << pbv_e << std::endl; } else { diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1a61cb449..d412eaa33 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -72,6 +72,7 @@ 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 retNode = t; + NodeManager *nm = NodeManager::currentNM(); if( t.getKind() == kind::STRING_SUBSTR ) { Node skt; @@ -105,52 +106,87 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node lemma = NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ); new_nodes.push_back( lemma ); retNode = skt; - } else if( t.getKind() == kind::STRING_STRIDOF ) { - Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" ); - Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" ); + } + else if (t.getKind() == kind::STRING_STRIDOF) + { + // processing term: indexof( x, y, n ) + Node skk; if( options::stringUfReduct() ){ skk = getUfAppForNode( kind::STRING_STRIDOF, t ); }else{ - skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); + skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof"); } - Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); - //TODO: simplify this (only applies when idof != -1) - Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) ); - new_nodes.push_back( eq ); - - //learn range of idof? - Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); - Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone ); + + Node negone = nm->mkConst(::CVC4::Rational(-1)); + Node krange = nm->mkNode(kind::GEQ, skk, negone); + // assert: indexof( x, y, n ) >= -1 new_nodes.push_back( krange ); - krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk); + krange = nm->mkNode(kind::GEQ, nm->mkNode(kind::STRING_LENGTH, t[0]), skk); + // assert: len( x ) >= indexof( x, y, z ) new_nodes.push_back( krange ); - // s2 = "" - Node c1 = t[1].eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - //~contain(t234, s2) - Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, st, t[1] ).negate(); - //left - Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3 ); - //t3 = s2 - Node c4 = t[1].eqNode( sk3 ); - //~contain(t2, s2) - Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, - NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2, - NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, t[1], d_zero, - NodeManager::currentNM()->mkNode(kind::MINUS, - NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]), - NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))), - t[1] ).negate(); - //k=str.len(s2) - Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, t[2], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 )) ); - //right - Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, c1.negate() ); - Node cond = skk.eqNode( negone ); - Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right ); + // substr( x, n, len( x ) - n ) + Node st = nm->mkNode( + kind::STRING_SUBSTR, + t[0], + t[2], + nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, t[0]), t[2])); + Node io2 = nm->mkSkolem("io2", nm->stringType(), "created for indexof"); + Node io4 = nm->mkSkolem("io4", nm->stringType(), "created for indexof"); + + // ~contains( substr( x, n, len( x ) - n ), y ) + Node c11 = nm->mkNode(kind::STRING_STRCTN, st, t[1]).negate(); + // n > len( x ) + Node c12 = + nm->mkNode(kind::GT, t[2], nm->mkNode(kind::STRING_LENGTH, t[0])); + // 0 > n + Node c13 = nm->mkNode(kind::GT, d_zero, t[2]); + Node cond1 = nm->mkNode(kind::OR, c11, c12, c13); + // skk = -1 + Node cc1 = skk.eqNode(negone); + + // y = "" + Node cond2 = t[1].eqNode(nm->mkConst(CVC4::String(""))); + // skk = n + Node cc2 = skk.eqNode(t[2]); + + // substr( x, n, len( x ) - n ) = str.++( io2, y, io4 ) + Node c31 = st.eqNode(nm->mkNode(kind::STRING_CONCAT, io2, t[1], io4)); + // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) + Node c32 = + nm->mkNode( + kind::STRING_STRCTN, + nm->mkNode( + kind::STRING_CONCAT, + io2, + nm->mkNode(kind::STRING_SUBSTR, + t[1], + d_zero, + nm->mkNode(kind::MINUS, + nm->mkNode(kind::STRING_LENGTH, t[1]), + d_one))), + t[1]) + .negate(); + // skk = n + len( io2 ) + Node c33 = skk.eqNode( + nm->mkNode(kind::PLUS, t[2], nm->mkNode(kind::STRING_LENGTH, io2))); + Node cc3 = nm->mkNode(kind::AND, c31, c32, c33); + + // assert: + // IF: ~contains( substr( x, n, len( x ) - n ), y ) OR n > len(x) OR 0 > n + // THEN: skk = -1 + // ELIF: y = "" + // THEN: skk = n + // ELSE: substr( x, n, len( x ) - n ) = str.++( io2, y, io4 ) ^ + // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) ^ + // skk = n + len( io2 ) + // for fresh io2, io4. + Node rr = nm->mkNode( + kind::ITE, cond1, cc1, nm->mkNode(kind::ITE, cond2, cc2, cc3)); new_nodes.push_back( rr ); + + // Thus, indexof( x, y, n ) = skk. retNode = skk; } else if( t.getKind() == kind::STRING_ITOS ) { //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, @@ -363,28 +399,64 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3); new_nodes.push_back( conc ); retNode = pret; - } else if( t.getKind() == kind::STRING_STRREPL ) { + } + else if (t.getKind() == kind::STRING_STRREPL) + { + // processing term: replace( x, y, z ) Node x = t[0]; Node y = t[1]; Node z = t[2]; - Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" ); - Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" ); - Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); - cond = NodeManager::currentNM()->mkNode( kind::AND, cond, NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) ); - Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); - Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); - Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, - NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1, - NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, y, d_zero, - NodeManager::currentNM()->mkNode(kind::MINUS, - NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), - NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate(); - Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3), - skw.eqNode(x) ); + TypeNode tn = t[0].getType(); + Node rp1 = nm->mkSkolem("rp1", tn, "created for replace"); + Node rp2 = nm->mkSkolem("rp2", tn, "created for replace"); + Node rpw = nm->mkSkolem("rpw", tn, "created for replace"); + + // y = "" + Node cond1 = y.eqNode(nm->mkConst(CVC4::String(""))); + // rpw = str.++( z, x ) + Node c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x)); + + // contains( x, y ) + Node cond2 = nm->mkNode(kind::STRING_STRCTN, x, y); + // x = str.++( rp1, y, rp2 ) + Node c21 = x.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, y, rp2)); + // rpw = str.++( rp1, z, rp2 ) + Node c22 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, z, rp2)); + // ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y ) + Node c23 = + nm->mkNode(kind::STRING_STRCTN, + nm->mkNode( + kind::STRING_CONCAT, + rp1, + nm->mkNode(kind::STRING_SUBSTR, + y, + d_zero, + nm->mkNode(kind::MINUS, + nm->mkNode(kind::STRING_LENGTH, y), + d_one))), + y) + .negate(); + + // assert: + // IF y="" + // THEN: rpw = str.++( z, x ) + // ELIF: contains( x, y ) + // THEN: x = str.++( rp1, y, rp2 ) ^ + // rpw = str.++( rp1, z, rp2 ) ^ + // ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y ), + // ELSE: rpw = x + // for fresh rp1, rp2, rpw + Node rr = nm->mkNode(kind::ITE, + cond1, + c1, + nm->mkNode(kind::ITE, + cond2, + nm->mkNode(kind::AND, c21, c22, c23), + rpw.eqNode(x))); new_nodes.push_back( rr ); - retNode = skw; + + // Thus, replace( x, y, z ) = rpw. + retNode = rpw; } else if( t.getKind() == kind::STRING_STRCTN ){ Node x = t[0]; Node s = t[1]; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 1555b0aa0..e66861579 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1827,16 +1827,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { return returnRewrite(node, negone, "idof-neg"); } - if (node[1].isConst()) - { - if (node[1].getConst().size() == 0) - { - // str.indexof( x, "", z ) --> -1 - Node negone = nm->mkConst(Rational(-1)); - return returnRewrite(node, negone, "idof-empty"); - } - } - // evaluation and simple cases std::vector children0; getConcat(node[0], children0); @@ -1884,16 +1874,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { { fstr = nm->mkNode(kind::STRING_SUBSTR, node[0], node[2], len0); fstr = Rewriter::rewrite(fstr); - if (fstr.isConst()) - { - CVC4::String fs = fstr.getConst(); - if (fs.size() == 0) - { - // substr( x, z, len(x) ) --> "" implies str.indexof( x, y, z ) --> -1 - Node negone = nm->mkConst(Rational(-1)); - return returnRewrite(node, negone, "idof-base-len"); - } - } } Node cmp_con = nm->mkNode(kind::STRING_STRCTN, fstr, node[1]); @@ -1960,25 +1940,22 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { Node TheoryStringsRewriter::rewriteReplace( Node node ) { Assert(node.getKind() == kind::STRING_STRREPL); - if( node[1]==node[2] ){ + NodeManager* nm = NodeManager::currentNM(); + + if (node[1] == node[2]) + { return returnRewrite(node, node[0], "rpl-id"); } - if (node[0].isConst()) + + if (node[0] == node[1]) { - CVC4::String s = node[0].getConst(); - if (s.isEmptyString()) - { - return returnRewrite(node, node[0], "rpl-empty"); - } - if (node[0] == node[2] && s.size() == 1) - { - // str.replace( "A", x, "A" ) -> "A" - return returnRewrite(node, node[0], "rpl-char-id"); - } + return returnRewrite(node, node[2], "rpl-replace"); } + if (node[1].isConst() && node[1].getConst().isEmptyString()) { - return returnRewrite(node, node[0], "rpl-rpl-empty"); + Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]); + return returnRewrite(node, ret, "rpl-rpl-empty"); } std::vector children0; @@ -2047,26 +2024,13 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { if (cmp_conr.getConst()) { - // currently by the semantics of replace, if the second argument is - // empty, then we return the first argument. - // hence, we test whether the second argument must be non-empty here. - // if it definitely non-empty, we can use rules that successfully replace - // node[1]->node[2] among those below. - Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]); - Node zero = NodeManager::currentNM()->mkConst(CVC4::Rational(0)); - bool is_non_empty = checkEntailArith(l1, zero, true); - - if (node[0] == node[1] && is_non_empty) - { - return returnRewrite(node, node[2], "rpl-replace"); - } // component-wise containment std::vector cb; std::vector ce; int cc = componentContains(children0, children1, cb, ce, true, 1); if (cc != -1) { - if (cc == 0 && children0[0] == children1[0] && is_non_empty) + if (cc == 0 && children0[0] == children1[0]) { // definitely a prefix, can do the replace // for example, @@ -2106,24 +2070,27 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { if (cmp_conr != cmp_con) { - // pull endpoints that can be stripped - // for example, - // str.replace( str.++( "b", x, "b" ), "a", y ) ---> - // str.++( "b", str.replace( x, "a", y ), "b" ) - std::vector cb; - std::vector ce; - if (stripConstantEndpoints(children0, children1, cb, ce)) + if (checkEntailNonEmpty(node[1])) { - std::vector cc; - cc.insert(cc.end(), cb.begin(), cb.end()); - cc.push_back(NodeManager::currentNM()->mkNode( - kind::STRING_STRREPL, - mkConcat(kind::STRING_CONCAT, children0), - node[1], - node[2])); - cc.insert(cc.end(), ce.begin(), ce.end()); - Node ret = mkConcat(kind::STRING_CONCAT, cc); - return returnRewrite(node, ret, "rpl-pull-endpt"); + // pull endpoints that can be stripped + // for example, + // str.replace( str.++( "b", x, "b" ), "a", y ) ---> + // str.++( "b", str.replace( x, "a", y ), "b" ) + std::vector cb; + std::vector ce; + if (stripConstantEndpoints(children0, children1, cb, ce)) + { + std::vector cc; + cc.insert(cc.end(), cb.begin(), cb.end()); + cc.push_back(NodeManager::currentNM()->mkNode( + kind::STRING_STRREPL, + mkConcat(kind::STRING_CONCAT, children0), + node[1], + node[2])); + cc.insert(cc.end(), ce.begin(), ce.end()); + Node ret = mkConcat(kind::STRING_CONCAT, cc); + return returnRewrite(node, ret, "rpl-pull-endpt"); + } } } @@ -2661,13 +2628,13 @@ bool TheoryStringsRewriter::componentContainsBase( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n2[0]); if (dir == 1) { - // To be suffix, start + length must be greater than + // To be a suffix, start + length must be greater than // or equal to the length of the string. success = checkEntailArith(end_pos, len_n2s); } else if (dir == -1) { - // To be prefix, must literally start at 0, since + // To be a prefix, must literally start at 0, since // if we knew it started at <0, it should be rewritten to "", // if we knew it started at 0, then n2[1] should be rewritten to // 0. @@ -2678,6 +2645,12 @@ bool TheoryStringsRewriter::componentContainsBase( { if (computeRemainder) { + // we can only compute the remainder if start_pos and end_pos + // are known to be non-negative. + if (!checkEntailArith(start_pos) || !checkEntailArith(end_pos)) + { + return false; + } if (dir != 1) { n1rb = NodeManager::currentNM()->mkNode( @@ -2883,6 +2856,13 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector& n1, return changed; } +bool TheoryStringsRewriter::checkEntailNonEmpty(Node a) +{ + Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a); + len = Rewriter::rewrite(len); + return checkEntailArith(len, true); +} + bool TheoryStringsRewriter::checkEntailArithEq(Node a, Node b) { if (a == b) diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index e0d265334..217546c71 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -91,19 +91,24 @@ private: * Context-Dependent Rewriting", CAV 2017. */ static Node rewriteContains(Node node); + /** rewrite indexof + * This is the entry point for post-rewriting terms n of the form + * str.indexof( s, t, n ) + * Returns the rewritten form of node. + */ static Node rewriteIndexof(Node node); /** rewrite replace * This is the entry point for post-rewriting terms n of the form * str.replace( s, t, r ) - * Returns the rewritten form of n. + * Returns the rewritten form of node. */ - static Node rewriteReplace(Node n); + static Node rewriteReplace(Node node); /** rewrite prefix/suffix * This is the entry point for post-rewriting terms n of the form * str.prefixof( s, t ) / str.suffixof( s, t ) - * Returns the rewritten form of n. + * Returns the rewritten form of node. */ - static Node rewritePrefixSuffix(Node n); + static Node rewritePrefixSuffix(Node node); /** gets the "vector form" of term n, adds it to c. * For example: @@ -269,6 +274,29 @@ private: * componentContainsBase(y, str.substr(y,0,5), n1rb, n1re, -1, true) * returns true, * n1re is set to str.substr(y,5,str.len(y)). + * + * + * Notice that this function may return false when it cannot compute a + * remainder when it otherwise would have returned true. For example: + * + * componentContainsBase(y, str.substr(y,x,z), n1rb, n1re, 0, false) + * returns true. + * + * Hence, we know that str.substr(y,x,z) is contained in y. However: + * + * componentContainsBase(y, str.substr(y,x,z), n1rb, n1re, 0, true) + * returns false. + * + * The reason is since computeRemainder=true, it must be that + * y = str.++( n1rb, str.substr(y,x,z), n1re ) + * for some n1rb, n1re. However, to construct such n1rb, n1re would require + * e.g. the terms: + * y = str.++( ite( x+z < 0 OR x < 0, "", str.substr(y,0,x) ), + * str.substr(y,x,z), + * ite( x+z < 0 OR x < 0, y, str.substr(y,x+z,len(y)) ) ) + * + * Since we do not wish to introduce ITE terms in the rewriter, we instead + * return false, indicating that we cannot compute the remainder. */ static bool componentContainsBase( Node n1, Node n2, Node& n1rb, Node& n1re, int dir, bool computeRemainder); @@ -305,6 +333,12 @@ private: std::vector& nb, std::vector& ne, int dir = 0); + /** entail non-empty + * + * Checks whether string a is entailed to be non-empty. Is equivalent to + * the call checkArithEntail( len( a ), true ). + */ + static bool checkEntailNonEmpty(Node a); /** check arithmetic entailment equal * Returns true if it is always the case that a = b. */ diff --git a/test/regress/regress0/strings/idof-sem.smt2 b/test/regress/regress0/strings/idof-sem.smt2 index 90dcc83a0..0de8f6a67 100644 --- a/test/regress/regress0/strings/idof-sem.smt2 +++ b/test/regress/regress0/strings/idof-sem.smt2 @@ -1,6 +1,6 @@ (set-logic SLIA) (set-option :strings-exp true) -(set-info :status unsat) +(set-info :status sat) (declare-fun x () String) (assert (not (= (str.indexof x "" 0) (- 1)))) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/strings/repl-rewrites2.smt2 b/test/regress/regress0/strings/repl-rewrites2.smt2 index 42699bc8b..e56a8ea44 100644 --- a/test/regress/regress0/strings/repl-rewrites2.smt2 +++ b/test/regress/regress0/strings/repl-rewrites2.smt2 @@ -5,10 +5,11 @@ (declare-fun x () String) (declare-fun y () String) (assert (or -(not (= (str.replace "" "" "c") "")) +(not (= (str.replace "" "" "c") "c")) (not (= (str.replace (str.++ "abc" y) "b" x) (str.++ "a" x "c" y))) (not (= (str.replace "" "abc" "de") "")) (not (= (str.replace "ab" "ab" "de") "de")) -(not (= (str.replace "ab" "" "de") "ab")) +(not (= (str.replace "ab" "" "de") "deab")) +(not (= (str.replace "abb" "b" "de") "adeb")) )) (check-sat) diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am index 493cd5b6d..f6326e0c6 100644 --- a/test/regress/regress1/strings/Makefile.am +++ b/test/regress/regress1/strings/Makefile.am @@ -25,7 +25,6 @@ TESTS = \ bug768.smt2 \ bug799-min.smt2 \ chapman150408.smt2 \ - cmu-disagree-0707-dd.smt2 \ cmu-inc-nlpp-071516.smt2 \ cmu-substr-rw.smt2 \ crash-1019.smt2 \ @@ -73,7 +72,8 @@ TESTS = \ str002.smt2 \ str007.smt2 \ rew-020618.smt2 \ - double-replace.smt2 + double-replace.smt2 \ + string-unsound-sem.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/strings/double-replace.smt2 b/test/regress/regress1/strings/double-replace.smt2 index 0800592d6..bfbc3afc1 100644 --- a/test/regress/regress1/strings/double-replace.smt2 +++ b/test/regress/regress1/strings/double-replace.smt2 @@ -1,7 +1,8 @@ (set-logic SLIA) +(set-option :strings-fmf true) (set-option :strings-exp true) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (assert (not (= (str.replace (str.replace x y x) x y) x))) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/strings/repl-empty-sem.smt2 b/test/regress/regress1/strings/repl-empty-sem.smt2 index 61f70bc23..56d4f1b86 100644 --- a/test/regress/regress1/strings/repl-empty-sem.smt2 +++ b/test/regress/regress1/strings/repl-empty-sem.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --strings-exp -; EXPECT: unsat +; EXPECT: sat (set-logic ALL) -(set-info :status unsat) +(set-info :status sat) (declare-fun x () String) (declare-fun z () String) (assert (= (str.len z) 0)) diff --git a/test/regress/regress1/strings/repl-soundness-sem.smt2 b/test/regress/regress1/strings/repl-soundness-sem.smt2 index d56d7945f..f65b3b56a 100644 --- a/test/regress/regress1/strings/repl-soundness-sem.smt2 +++ b/test/regress/regress1/strings/repl-soundness-sem.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --strings-exp -; EXPECT: sat +; EXPECT: unsat (set-logic ALL) -(set-info :status sat) +(set-info :status unsat) (declare-fun x () String) (declare-fun y () String) (assert (and diff --git a/test/regress/regress1/strings/rew-020618.smt2 b/test/regress/regress1/strings/rew-020618.smt2 index 5fb58a272..95dbf4d29 100644 --- a/test/regress/regress1/strings/rew-020618.smt2 +++ b/test/regress/regress1/strings/rew-020618.smt2 @@ -9,7 +9,7 @@ (= (str.++ s s) "A") (not (str.contains s "")) (str.contains "" (str.++ s "A")) -(not (= (str.replace "A" s "A") "A")) +(not (= (str.replace "A" "" "A") "AA")) (not (= (str.prefixof s "A") (str.suffixof s "A"))) (not (str.prefixof s s)) (not (str.prefixof "" s)) diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2 new file mode 100644 index 000000000..771d8d4b0 --- /dev/null +++ b/test/regress/regress1/strings/string-unsound-sem.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () Int) +(assert (and +(not (= (str.replace "A" (int.to.str z) x) (str.++ "A" (str.replace "" (int.to.str z) x)))) +(not (= (str.replace x (str.at x z) "") (str.++ (str.replace (str.++ (str.substr x 0 z) (str.substr x z 1)) (str.substr x z 1) "") (str.substr x (+ 1 z) (str.len x))))) +) +) +(check-sat) diff --git a/test/regress/regress2/strings/Makefile.am b/test/regress/regress2/strings/Makefile.am index 9b397699c..4e6f3aa56 100644 --- a/test/regress/regress2/strings/Makefile.am +++ b/test/regress/regress2/strings/Makefile.am @@ -19,7 +19,8 @@ endif TESTS = \ cmu-dis-0707-3.smt2 \ cmu-prereg-fmf.smt2 \ - cmu-repl-len-nterm.smt2 + cmu-repl-len-nterm.smt2 \ + cmu-disagree-0707-dd.smt2 EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 similarity index 100% rename from test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 rename to test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 -- 2.30.2