Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
return returnRewrite(node, ret, "idof-def-ctn");
}
+
+ // Strip components from the beginning that are guaranteed not to match
+ if (stripConstantEndpoints(children0, children1, nb, ne, 1))
+ {
+ // str.indexof(str.++("AB", x, "C"), "C", 0) --->
+ // 2 + str.indexof(str.++(x, "C"), "C", 0)
+ Node ret =
+ nm->mkNode(kind::PLUS,
+ nm->mkNode(kind::STRING_LENGTH,
+ mkConcat(kind::STRING_CONCAT, nb)),
+ nm->mkNode(kind::STRING_STRIDOF,
+ mkConcat(kind::STRING_CONCAT, children0),
+ node[1],
+ node[2]));
+ return returnRewrite(node, ret, "idof-strip-cnst-endpts");
+ }
}
// strip symbolic length
// str.contains( str.++( "c", x ), str.++( "cd", y ) )
overlap = r == 0 ? s.overlap(t) : t.overlap(s);
}
+ else
+ {
+ // if we are looking at a substring, we can remove the component
+ // if there is no overlap
+ // e.g. str.contains( str.++( str.substr( "c", i, j ), x), "a" )
+ // --> str.contains( x, "a" )
+ removeComponent = ((r == 0 ? s.overlap(t) : t.overlap(s)) == 0);
+ }
}
else if (sss.empty()) // only if not substr
{
Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
Node aaad = d_nm->mkConst(::CVC4::String("AAAD"));
Node b = d_nm->mkConst(::CVC4::String("B"));
+ Node c = d_nm->mkConst(::CVC4::String("C"));
+ Node ccc = d_nm->mkConst(::CVC4::String("CCC"));
Node x = d_nm->mkVar("x", strType);
Node y = d_nm->mkVar("y", strType);
Node negOne = d_nm->mkConst(Rational(-1));
+ Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
Node two = d_nm->mkConst(Rational(2));
Node three = d_nm->mkConst(Rational(3));
Node i = d_nm->mkVar("i", intType);
+ Node j = d_nm->mkVar("j", intType);
// Same normal form for:
//
a,
i);
sameNormalForm(idof_substr, negOne);
+
+ {
+ // Same normal form for:
+ //
+ // (str.indexof (str.++ "B" (str.substr "CCC" i j) x "A") "A" 0)
+ //
+ // (+ 1 (str.len (str.substr "CCC" i j))
+ // (str.indexof (str.++ "A" x y) "A" 0))
+ Node lhs = d_nm->mkNode(
+ kind::STRING_STRIDOF,
+ d_nm->mkNode(kind::STRING_CONCAT,
+ b,
+ d_nm->mkNode(kind::STRING_SUBSTR, ccc, i, j),
+ x,
+ a),
+ a,
+ zero);
+ Node rhs = d_nm->mkNode(
+ kind::PLUS,
+ one,
+ d_nm->mkNode(kind::STRING_LENGTH,
+ d_nm->mkNode(kind::STRING_SUBSTR, ccc, i, j)),
+ d_nm->mkNode(kind::STRING_STRIDOF,
+ d_nm->mkNode(kind::STRING_CONCAT, x, a),
+ a,
+ zero));
+ sameNormalForm(lhs, rhs);
+ }
+
+ {
+ // Same normal form for:
+ //
+ // (str.indexof (str.++ "B" "C" "A" x y) "A" 0)
+ //
+ // (+ 2 (str.indexof (str.++ "A" x y) "A" 0))
+ Node lhs = d_nm->mkNode(kind::STRING_STRIDOF,
+ d_nm->mkNode(kind::STRING_CONCAT, b, c, a, x, y),
+ a,
+ zero);
+ Node rhs =
+ d_nm->mkNode(kind::PLUS,
+ two,
+ d_nm->mkNode(kind::STRING_STRIDOF,
+ d_nm->mkNode(kind::STRING_CONCAT, a, x, y),
+ a,
+ zero));
+ sameNormalForm(lhs, rhs);
+ }
}
void testRewriteReplace()
Node empty = d_nm->mkConst(::CVC4::String(""));
Node a = d_nm->mkConst(::CVC4::String("A"));
+ Node ab = d_nm->mkConst(::CVC4::String("AB"));
Node b = d_nm->mkConst(::CVC4::String("B"));
Node c = d_nm->mkConst(::CVC4::String("C"));
Node abc = d_nm->mkConst(::CVC4::String("ABC"));
Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
Node z = d_nm->mkVar("z", strType);
Node n = d_nm->mkVar("n", intType);
+ Node m = d_nm->mkVar("m", intType);
Node one = d_nm->mkConst(Rational(1));
Node two = d_nm->mkConst(Rational(2));
Node three = d_nm->mkConst(Rational(3));
rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc);
differentNormalForms(lhs, rhs);
}
+
+ {
+ // Same normal form for:
+ //
+ // (str.contains (str.++ (str.substr "DEF" n m) x) "AB")
+ //
+ // (str.contains x "AB")
+ lhs = d_nm->mkNode(
+ kind::STRING_STRCTN,
+ d_nm->mkNode(kind::STRING_CONCAT,
+ d_nm->mkNode(kind::STRING_SUBSTR, def, n, m),
+ x),
+ ab);
+ rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ab);
+ sameNormalForm(lhs, rhs);
+ }
}
void testInferEqsFromContains()