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

fixing build

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-07-30 12:33:32 -07:00
parent 69b4a819a6
commit e0a9848e01
2 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/arith_rewriter.cpp
View file

@ -624,14 +624,14 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
switch (kind) { switch (kind) {
case LE: case LE:
result = m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)); result = m_util.mk_lt(t, m_util.mk_numeral(a2+1, false));
return BR_DONE; return BR_REWRITE1;
case GE: case GE:
result = m_util.mk_ge(t, m_util.mk_numeral(a2, false)); result = m_util.mk_ge(t, m_util.mk_numeral(a2, false));
return BR_REWRITE1; return BR_REWRITE1;
case EQ: case EQ:
result = m_util.mk_ge(t, m_util.mk_numeral(a2, false)); result = m_util.mk_ge(t, m_util.mk_numeral(a2, false));
result = m().mk_and(m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)), result); result = m().mk_and(m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)), result);
return BR_DONE; return BR_REWRITE3;
} }
} }
if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) { if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {

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

@ -824,6 +824,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
result = m_autil.mk_add(es.size(), es.c_ptr()); result = m_autil.mk_add(es.size(), es.c_ptr());
return BR_REWRITE2; return BR_REWRITE2;
} }
#if 0
expr* s = nullptr, *offset = nullptr, *length = nullptr; expr* s = nullptr, *offset = nullptr, *length = nullptr;
if (str().is_extract(a, s, offset, length)) { if (str().is_extract(a, s, offset, length)) {
expr_ref len_s(str().mk_length(s), m()); expr_ref len_s(str().mk_length(s), m());
@ -837,11 +838,12 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
result = m().mk_ite(m_autil.mk_gt(m_autil.mk_add(offset, length), len_s), result = m().mk_ite(m_autil.mk_gt(m_autil.mk_add(offset, length), len_s),
m_autil.mk_sub(len_s, offset), m_autil.mk_sub(len_s, offset),
result); result);
result = m().mk_ite(m().mk_or(m_autil.mk_ge(offset, len_s), m_autil.mk_le(length, zero), m_autil.mk_lt(offset, zero)), result = m().mk_ite(m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_le(length, zero), m_autil.mk_lt(offset, zero)),
zero, zero,
result); result);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
#endif
return BR_FAILED; return BR_FAILED;
} }
@ -3810,7 +3812,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
} }
bool changed = false; bool changed = false;
if (reduce_eq_empty(l, r, result)) if (reduce_eq_empty(l, r, result))
return BR_REWRITE3; return BR_REWRITE_FULL;
if (!reduce_eq(l, r, new_eqs, changed)) { if (!reduce_eq(l, r, new_eqs, changed)) {
result = m().mk_false(); result = m().mk_false();
@ -4220,7 +4222,7 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
fmls.push_back(m_autil.mk_lt(offset, m_autil.mk_int(0))); fmls.push_back(m_autil.mk_lt(offset, m_autil.mk_int(0)));
fmls.push_back(m().mk_eq(s, l)); fmls.push_back(m().mk_eq(s, l));
fmls.push_back(m_autil.mk_lt(len, m_autil.mk_int(0))); fmls.push_back(m_autil.mk_lt(len, m_autil.mk_int(0)));
fmls.push_back(m_autil.mk_ge(offset, len_s)); fmls.push_back(m_autil.mk_le(len_s, offset));
result = m().mk_or(fmls); result = m().mk_or(fmls);
return true; return true;
} }