mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
73f93dbadb
|
@ -320,6 +320,21 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
}
|
||||
}
|
||||
|
||||
expr* a1, *a2, *a3, *a4, *a5, *a6;
|
||||
// (bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
|
||||
// (bvsle (+ x (* -1 (srem_i x c1))) c2)
|
||||
// pre: (and (> c1 0) (> c2 0) (= c2 % c1 0) (<= (+ c1 c2 -1) max_int))
|
||||
if (is_signed && is_num2 && m_util.is_bv_add(a, a1, a2) &&
|
||||
m_util.is_bv_mul(a2, a3, a4) && is_numeral(a3, r1, sz) &&
|
||||
m_util.norm(r1, sz, is_signed).is_minus_one() &&
|
||||
m_util.is_bv_sremi(a4, a5, a6) && is_numeral(a6, r1, sz) &&
|
||||
(r1 = m_util.norm(r1, sz, is_signed), r1.is_pos()) &&
|
||||
r2.is_pos() &&
|
||||
(r2 % r1).is_zero() && r1 + r2 - rational::one() < rational::power_of_two(sz-1)) {
|
||||
result = m_util.mk_sle(a1, m_util.mk_numeral(r1 + r2 - rational::one(), sz));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
#if 0
|
||||
if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) {
|
||||
//
|
||||
|
|
|
@ -32,14 +32,16 @@ struct interval {
|
|||
// l > h: [0, h] U [l, UMAX_INT]
|
||||
rational l, h;
|
||||
unsigned sz;
|
||||
bool tight;
|
||||
|
||||
explicit interval() : l(0), h(0), sz(0) {}
|
||||
interval(const rational& l, const rational& h, unsigned sz) : l(l), h(h), sz(sz) {
|
||||
explicit interval() : l(0), h(0), sz(0), tight(false) {}
|
||||
interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
|
||||
SASSERT(invariant());
|
||||
}
|
||||
|
||||
bool invariant() const {
|
||||
return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz);
|
||||
return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
|
||||
(!is_wrapped() || l != h+rational::one());
|
||||
}
|
||||
|
||||
bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
|
||||
|
@ -113,13 +115,18 @@ struct interval {
|
|||
return false;
|
||||
|
||||
// 0 .. l.. l' ... h ... h'
|
||||
result = interval(std::max(l, b.l), std::min(h, b.h), sz);
|
||||
result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/// return false if negation is empty
|
||||
bool negate(interval& result) const {
|
||||
if (!tight) {
|
||||
result = interval(rational::zero(), uMaxInt(sz), true);
|
||||
return true;
|
||||
}
|
||||
|
||||
if (is_full())
|
||||
return false;
|
||||
if (l.is_zero()) {
|
||||
|
@ -152,40 +159,43 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
|||
|
||||
if (m_bv.is_bv_ule(e, lhs, rhs)) {
|
||||
if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C
|
||||
b = interval(n, uMaxInt(sz), sz);
|
||||
if (m_bv.is_numeral(rhs))
|
||||
return false;
|
||||
b = interval(n, uMaxInt(sz), sz, true);
|
||||
v = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_bv.is_numeral(rhs, n, sz)) { // x ule C
|
||||
b = interval(rational::zero(), n, sz);
|
||||
b = interval(rational::zero(), n, sz, true);
|
||||
v = lhs;
|
||||
return true;
|
||||
}
|
||||
} else if (m_bv.is_bv_sle(e, lhs, rhs)) {
|
||||
if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C
|
||||
b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz);
|
||||
if (m_bv.is_numeral(rhs))
|
||||
return false;
|
||||
b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true);
|
||||
v = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_bv.is_numeral(rhs, n, sz)) { // x sle C
|
||||
b = interval(rational::power_of_two(sz-1), n, sz);
|
||||
b = interval(rational::power_of_two(sz-1), n, sz, true);
|
||||
v = lhs;
|
||||
return true;
|
||||
}
|
||||
} else if (m.is_eq(e, lhs, rhs)) {
|
||||
if (m_bv.is_numeral(lhs, n, sz)) {
|
||||
b = interval(n, n, sz);
|
||||
if (m_bv.is_numeral(rhs))
|
||||
return false;
|
||||
b = interval(n, n, sz, true);
|
||||
v = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_bv.is_numeral(rhs, n, sz)) {
|
||||
b = interval(n, n, sz);
|
||||
b = interval(n, n, sz, true);
|
||||
v = lhs;
|
||||
return true;
|
||||
}
|
||||
} else if (m.is_not(e, lhs)) {
|
||||
if (is_bound(lhs, v, b))
|
||||
return b.negate(b);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
@ -199,7 +209,7 @@ public:
|
|||
|
||||
virtual ~bv_bounds_simplifier() {}
|
||||
|
||||
virtual void assert_expr(expr * t, bool sign) {
|
||||
virtual bool assert_expr(expr * t, bool sign) {
|
||||
while (m.is_not(t, t)) {
|
||||
sign = !sign;
|
||||
}
|
||||
|
@ -207,34 +217,54 @@ public:
|
|||
interval b;
|
||||
expr* t1;
|
||||
if (is_bound(t, t1, b)) {
|
||||
SASSERT(!m_bv.is_numeral(t1));
|
||||
if (sign)
|
||||
VERIFY(b.negate(b));
|
||||
|
||||
push();
|
||||
TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
|
||||
interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value;
|
||||
VERIFY(r.intersect(b, r));
|
||||
return r.intersect(b, r);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual bool simplify(expr* t, expr_ref& result) {
|
||||
expr* t1;
|
||||
interval b, ctx, intr;
|
||||
result = 0;
|
||||
bool sign = false;
|
||||
|
||||
while (m.is_not(t, t)) {
|
||||
sign = !sign;
|
||||
}
|
||||
|
||||
if (!is_bound(t, t1, b))
|
||||
return false;
|
||||
|
||||
if (m_bound->find(t1, ctx)) {
|
||||
if (!b.intersect(ctx, intr)) {
|
||||
if (sign && b.tight) {
|
||||
sign = false;
|
||||
if (!b.negate(b)) {
|
||||
result = m.mk_false();
|
||||
} else if (intr.l == intr.h && intr != b) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
|
||||
} else if (ctx.implies(b)) {
|
||||
result = m.mk_true();
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
if (m_bound->find(t1, ctx)) {
|
||||
if (ctx.implies(b)) {
|
||||
result = m.mk_true();
|
||||
} else if (!b.intersect(ctx, intr)) {
|
||||
result = m.mk_false();
|
||||
} else if (intr.l == intr.h) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
|
||||
}
|
||||
} else if (b.is_full() && b.tight) {
|
||||
result = m.mk_true();
|
||||
}
|
||||
|
||||
CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
|
||||
if (sign && result != 0)
|
||||
result = m.mk_not(result);
|
||||
return result != 0;
|
||||
}
|
||||
|
||||
|
|
|
@ -34,7 +34,7 @@ class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier {
|
|||
public:
|
||||
ctx_propagate_assertions(ast_manager& m);
|
||||
virtual ~ctx_propagate_assertions() {}
|
||||
virtual void assert_expr(expr * t, bool sign);
|
||||
virtual bool assert_expr(expr * t, bool sign);
|
||||
virtual bool simplify(expr* t, expr_ref& result);
|
||||
virtual void push();
|
||||
virtual void pop(unsigned num_scopes);
|
||||
|
@ -45,7 +45,7 @@ public:
|
|||
|
||||
ctx_propagate_assertions::ctx_propagate_assertions(ast_manager& m): m(m), m_trail(m) {}
|
||||
|
||||
void ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
|
||||
bool ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
|
||||
|
||||
expr * p = t;
|
||||
while (m.is_not(t, t)) {
|
||||
|
@ -64,6 +64,7 @@ void ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
|
|||
else if (m.is_value(lhs))
|
||||
assert_eq_val(rhs, to_app(lhs), mk_scope);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void ctx_propagate_assertions::assert_eq_val(expr * t, app * val, bool mk_scope) {
|
||||
|
@ -307,8 +308,8 @@ struct ctx_simplify_tactic::imp {
|
|||
CASSERT("ctx_simplify_tactic", check_cache());
|
||||
}
|
||||
|
||||
void assert_expr(expr * t, bool sign) {
|
||||
m_simp->assert_expr(t, sign);
|
||||
bool assert_expr(expr * t, bool sign) {
|
||||
return m_simp->assert_expr(t, sign);
|
||||
}
|
||||
|
||||
bool is_cached(expr * t, expr_ref & r) {
|
||||
|
@ -370,6 +371,9 @@ struct ctx_simplify_tactic::imp {
|
|||
simplify(arg, new_arg);
|
||||
if (new_arg != arg)
|
||||
modified = true;
|
||||
if (i < num_args - 1 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
|
||||
new_arg = m.mk_false();
|
||||
|
||||
if ((OR && m.is_false(new_arg)) ||
|
||||
(!OR && m.is_true(new_arg))) {
|
||||
modified = true;
|
||||
|
@ -383,8 +387,6 @@ struct ctx_simplify_tactic::imp {
|
|||
return;
|
||||
}
|
||||
new_args.push_back(new_arg);
|
||||
if (i < num_args - 1)
|
||||
assert_expr(new_arg, OR);
|
||||
}
|
||||
pop(scope_level() - old_lvl);
|
||||
|
||||
|
@ -398,6 +400,9 @@ struct ctx_simplify_tactic::imp {
|
|||
simplify(arg, new_arg);
|
||||
if (new_arg != arg)
|
||||
modified = true;
|
||||
if (i > 0 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
|
||||
new_arg = m.mk_false();
|
||||
|
||||
if ((OR && m.is_false(new_arg)) ||
|
||||
(!OR && m.is_true(new_arg))) {
|
||||
modified = true;
|
||||
|
@ -411,8 +416,6 @@ struct ctx_simplify_tactic::imp {
|
|||
return;
|
||||
}
|
||||
new_new_args.push_back(new_arg);
|
||||
if (i > 0)
|
||||
assert_expr(new_arg, OR);
|
||||
}
|
||||
pop(scope_level() - old_lvl);
|
||||
|
||||
|
@ -448,10 +451,14 @@ struct ctx_simplify_tactic::imp {
|
|||
else {
|
||||
expr_ref new_t(m);
|
||||
expr_ref new_e(m);
|
||||
assert_expr(new_c, false);
|
||||
if (!assert_expr(new_c, false)) {
|
||||
simplify(e, r);
|
||||
cache(ite, r);
|
||||
return;
|
||||
}
|
||||
simplify(t, new_t);
|
||||
pop(scope_level() - old_lvl);
|
||||
assert_expr(new_c, true);
|
||||
VERIFY(assert_expr(new_c, true));
|
||||
simplify(e, new_e);
|
||||
pop(scope_level() - old_lvl);
|
||||
if (c == new_c && t == new_t && e == new_e) {
|
||||
|
|
|
@ -28,7 +28,7 @@ public:
|
|||
goal_num_occurs* m_occs;
|
||||
public:
|
||||
virtual ~simplifier() {}
|
||||
virtual void assert_expr(expr * t, bool sign) = 0;
|
||||
virtual bool assert_expr(expr * t, bool sign) = 0;
|
||||
virtual bool simplify(expr* t, expr_ref& result) = 0;
|
||||
virtual void push() = 0;
|
||||
virtual void pop(unsigned num_scopes) = 0;
|
||||
|
|
Loading…
Reference in a new issue