mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

prepare for stronger rewrites

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-02 15:51:49 -07:00
parent 6e4a059c75
commit 4067c84611
1 changed files with 19 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -691,15 +691,12 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
return BR_REWRITE3; return BR_REWRITE3;
} }
#if 0 #if 0
expr* s = nullptr, *offs = nullptr, *l = nullptr; if (m().is_ite(a, c, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
// len(extract(s, offs, len(s) - offs)) = max(0, len(s) - offs) result = m().mk_ite(c, m_util.str.mk_length(t), m_util.str.mk_length(e));
// return BR_REWRITE3;
if (m_util.str.is_extract(a, s, offs, l) && is_suffix(s, offs, l)) {
result = m_autil.mk_sub(m_util.str.mk_length(s), offs);
result = m().mk_ite(m_autil.mk_ge(result, zero()), result, zero());
return BR_REWRITE_FULL;
} }
#endif #endif
return BR_FAILED; return BR_FAILED;
} }
@ -774,6 +771,21 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
bool lengthPos = m_util.str.is_length(b) || m_autil.is_add(b); bool lengthPos = m_util.str.is_length(b) || m_autil.is_add(b);
sort* a_sort = m().get_sort(a); sort* a_sort = m().get_sort(a);
expr* cond = nullptr, *t = nullptr, *e = nullptr;
#if 0
if (m().is_ite(a, cond, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
result = m().mk_ite(cond, m_util.str.mk_substr(t, b, c), m_util.str.mk_substr(e, b, c));
return BR_REWRITE3;
}
if (m().is_ite(b, cond, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
result = m().mk_ite(cond, m_util.str.mk_substr(a, t, c), m_util.str.mk_substr(a, e, c));
return BR_REWRITE3;
}
if (m().is_ite(c, cond, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
result = m().mk_ite(cond, m_util.str.mk_substr(a, b, t), m_util.str.mk_substr(a, b, e));
return BR_REWRITE3;
}
#endif
sign sg; sign sg;
if (sign_is_determined(c, sg) && sg == sign_neg) { if (sign_is_determined(c, sg) && sg == sign_neg) {
result = m_util.str.mk_empty(a_sort); result = m_util.str.mk_empty(a_sort);