mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

add eval1 functionality for replace_all

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-29 04:36:55 -08:00
parent ab43d2dcf1
commit 6d3cfb63da
1 changed files with 24 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ast/sls/sls_seq_plugin.cpp
View file

@ -457,12 +457,35 @@ namespace sls {
ev.val1.svalue = r.replace(s, t);
return ev.val1.svalue;
}
case OP_SEQ_REPLACE_ALL: {
expr* x, * y, * z;
VERIFY(seq.str.is_replace_all(e, x, y, z));
zstring s1 = strval0(x);
zstring s2 = strval0(y);
zstring c = strval0(z);
if (s1.length() < s2.length())
ev.val1.svalue = s1;
else {
zstring r;
for (unsigned i = 0; i < s1.length(); ++i) {
if (s1.length() >= s2.length() + i &&
s2 == s1.extract(i, s2.length())) {
r += c;
i += s2.length() - 1;
}
else
r += zstring(s1[i]);
}
ev.val1.svalue = r;
}
return ev.val1.svalue;
}
case OP_SEQ_NTH:
case OP_SEQ_NTH_I:
case OP_SEQ_NTH_U:
case OP_SEQ_REPLACE_RE_ALL:
case OP_SEQ_REPLACE_RE:
case OP_SEQ_REPLACE_ALL:
case OP_SEQ_MAP:
case OP_SEQ_MAPI:
case OP_SEQ_FOLDL: