mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

added derivative support for (str.to_re (str.from_int ...)) (#5431)

Browse source
This commit is contained in:
Margus Veanes 2021-07-25 09:51:48 -07:00 • committed by GitHub
parent 2fa156eaf4
commit 4fd1e6d32c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 20 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/rewriter/seq_rewriter.cpp
View file

@ -3339,6 +3339,26 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
//while mk_empty() = [], because deriv(epsilon) = [] = nothing
return mk_empty();
}
else if (str().is_itos(r1, r2))
{
//here r1 = (str.from_int r2) and r2 is non-ground
//or else the expression would have been simplified earlier
//so r1 must be nonempty and must consists of decimal digits
//'0' = char(48) <= elem <= char(57) = '9'
m_br.mk_and(u().mk_le(m_util.mk_char(48), ele), u().mk_le(ele, m_util.mk_char(57)), result);
if (m().is_false(result))
return mk_empty();
hd = str().mk_nth_i(r1, m_autil.mk_int(0));
m_br.mk_and(result, m().mk_eq(hd, ele), result); // result := result & ele = (hd r1)
if (m().is_false(result))
return mk_empty();
tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)));
//if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
result = re_and(result, re().mk_to_re(tl));
return result;
}
#if 0
else {
hd = str().mk_nth_i(r1, m_autil.mk_int(0));