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';
{ 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
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
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:
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.<=";
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);
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"
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
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<SkolemId, Node>::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;
}
// 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
* 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<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
/** the set of all skolems we have generated */
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);
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 ) );
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<Node> new_nodes;
Node res = d_preproc.simplify(n, new_nodes);
Assert(res != 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;
// 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<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(
+ 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<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(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<Node> 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];
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;
}
}
else if (nk == kind::STRING_LENGTH)
{
+ Kind nk0 = node[0].getKind();
if( node[0].isConst() ){
retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().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<String>().size() ) );
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]));
{
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);
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<String>().isEmptyString())
{
Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]);
}
}
+ // 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
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<Node> children;
+ String s = node[0].getConst<String>();
+ String t = node[1].getConst<String>();
+ 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);
* 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 )
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
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
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
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
projects / cvc5.git / commitdiff