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

parameter eval order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-07 09:17:12 -07:00 • committed by Nikolaj Bjorner
parent 748b004e0d
commit f8fb0351af
1 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4393,9 +4393,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m());
expr_ref len_a(str().mk_length(a), m());
expr_ref len_tl(m_autil.mk_sub(len_a, len_hd), m());
result = m().mk_and(m_autil.mk_ge(len_a, len_hd),
re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd),
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
auto ge_len = m_autil.mk_ge(len_a, len_hd);
auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd);
auto suffix = re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl);
result = m().mk_and(ge_len, prefix, suffix);
return BR_REWRITE_FULL;
}
if (get_re_head_tail_reversed(b, hd, tl)) {
@ -4404,10 +4405,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
expr_ref len_a(str().mk_length(a), m());
expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m());
expr* s = nullptr;
result = m().mk_and(m_autil.mk_ge(len_a, len_tl),
re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd),
(re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) :
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)));
auto ge_len = m_autil.mk_ge(len_a, len_tl);
auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd);
auto tail_seq = str().mk_substr(a, len_hd, len_tl);
auto tail = (re().is_to_re(tl, s) ? m().mk_eq(s, tail_seq) : re().mk_in_re(tail_seq, tl));
result = m().mk_and(ge_len, prefix, tail);
return BR_REWRITE_FULL;
}