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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-19 08:23:27 -08:00
parent 5962ca2a62 73da4dda07
commit bff10527d1
5 changed files with 87 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -321,13 +321,17 @@ 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 (rem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
// (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, r3, sz) &&
(r3 = m_util.norm(r3, sz, is_signed), r3.is_minus_one()) &&
m_util.is_bv_sremi(a4, a5, a6) && is_numeral(a6, r3, sz) &&
a1 == a5 /* && r1 + r3 - rational::one() < power(rational(2), sz) */) {
result = m_util.mk_sle(a1, m_util.mk_numeral(r3 + r1 - rational::one(), sz));
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;
}

15
src/smt/theory_seq.cpp
View file

@ -517,12 +517,13 @@ bool theory_seq::check_length_coherence() {
bool theory_seq::fixed_length() {
obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
bool found = false;
for (; it != end; ++it) {
if (fixed_length(*it)) {
return true;
found = true;
}
}
return false;
return found;
}
bool theory_seq::fixed_length(expr* e) {
@ -530,7 +531,10 @@ bool theory_seq::fixed_length(expr* e) {
if (!(is_var(e) && lower_bound(e, lo) && upper_bound(e, hi) && lo == hi && lo.is_unsigned() && lo.is_pos())) {
return false;
}
if (m_fixed.contains(e)) {
if (is_skolem(m_tail, e) || is_skolem(m_seq_first, e) ||
is_skolem(m_indexof_left, e) || is_skolem(m_indexof_right, e) ||
is_skolem(m_contains_left, e) || is_skolem(m_contains_right, e) ||
m_fixed.contains(e)) {
return false;
}
@ -539,10 +543,6 @@ bool theory_seq::fixed_length(expr* e) {
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_fixed, e));
m_fixed.insert(e);
if (is_skolem(m_tail, e) || is_skolem(m_pre, e) || is_skolem(m_post, e) || is_skolem(m_seq_first, e)) {
return false;
}
unsigned _lo = lo.get_unsigned();
expr_ref seq(e, m), head(m), tail(m);
expr_ref_vector elems(m);
@ -553,7 +553,6 @@ bool theory_seq::fixed_length(expr* e) {
seq = tail;
}
seq = mk_concat(elems.size(), elems.c_ptr());
std::cout << "Fixed " << mk_pp(e, m) << " " << lo << " " << get_context().get_scope_level() << "\n";
TRACE("seq", tout << "Fixed: " << mk_pp(e, m) << " " << lo << "\n";);
add_axiom(~mk_eq(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true), false), mk_seq_eq(seq, e));
if (!ctx.at_base_level()) {

72
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -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); }
@ -49,6 +51,7 @@ struct interval {
SASSERT(sz == b.sz);
return l == b.l && h == b.h;
}
bool operator!=(const interval& b) const { return !(*this == b); }
bool implies(const interval& b) const {
if (b.is_full())
@ -112,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()) {
@ -151,34 +159,40 @@ 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;
}
@ -195,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;
}
@ -203,36 +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 == b) {
// no improvement in range; do nothing
} else if (intr.l == intr.h) {
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;
}

27
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -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) {

2
src/tactic/core/ctx_simplify_tactic.h
View file

@ -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;