summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp182
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp112
-rw-r--r--src/theory/strings/theory_strings_rewriter.h42
-rw-r--r--test/regress/regress0/strings/idof-sem.smt24
-rw-r--r--test/regress/regress0/strings/repl-rewrites2.smt25
-rw-r--r--test/regress/regress1/strings/Makefile.am4
-rw-r--r--test/regress/regress1/strings/double-replace.smt23
-rw-r--r--test/regress/regress1/strings/repl-empty-sem.smt24
-rw-r--r--test/regress/regress1/strings/repl-soundness-sem.smt24
-rw-r--r--test/regress/regress1/strings/rew-020618.smt22
-rw-r--r--test/regress/regress1/strings/string-unsound-sem.smt212
-rw-r--r--test/regress/regress2/strings/Makefile.am3
-rw-r--r--test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 (renamed from test/regress/regress1/strings/cmu-disagree-0707-dd.smt2)0
14 files changed, 240 insertions, 139 deletions
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<String>().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<Node> 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<String>();
- 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<String>();
- 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<String>().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<Node> children0;
@@ -2047,26 +2024,13 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
{
if (cmp_conr.getConst<bool>())
{
- // 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<Node> cb;
std::vector<Node> 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<Node> cb;
- std::vector<Node> ce;
- if (stripConstantEndpoints(children0, children1, cb, ce))
+ if (checkEntailNonEmpty(node[1]))
{
- std::vector<Node> 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<Node> cb;
+ std::vector<Node> ce;
+ if (stripConstantEndpoints(children0, children1, cb, ce))
+ {
+ std::vector<Node> 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<Node>& 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<Node>& nb,
std::vector<Node>& 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
index c44dfa396..c44dfa396 100644
--- a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2
+++ b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback