diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp new file mode 100644 index 000000000..9d3ca8c76 --- /dev/null +++ b/src/ast/rewriter/bv_bounds.cpp @@ -0,0 +1,667 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + bv_bounds.cpp + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: +--*/ +#include"bv_bounds.h" +#include"ast_smt2_pp.h" + +bv_bounds::~bv_bounds() { + reset(); +} + +bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool negated, vector& nis) { + TRACE("bv_bounds", tout << "record0 " << mk_ismt2_pp(v, m_m) << ":" << (negated ? "~[" : "[") << lo << ";" << hi << "]" << std::endl;); + const unsigned bv_sz = m_bv_util.get_bv_size(v); + const numeral& zero = numeral::zero(); + const numeral& one = numeral::one(); + SASSERT(zero <= lo); + SASSERT(lo <= hi); + SASSERT(hi < numeral::power_of_two(bv_sz)); + numeral vmax, vmin; + const bool has_upper = m_unsigned_uppers.find(v, vmax); + const bool has_lower = m_unsigned_lowers.find(v, vmin); + if (!has_lower) vmin = numeral::zero(); + if (!has_upper) vmax = (numeral::power_of_two(bv_sz) - one); + bool lo_min = lo <= vmin; + bool hi_max = hi >= vmax; + if (negated) { + if (lo_min && hi_max) return UNSAT; + if (lo > vmax) return CONVERTED; + if (hi < vmin) return CONVERTED; + if (lo_min) { + negated = false; lo = hi + one; hi = vmax; + lo_min = lo <= vmin; + hi_max = true; + } else if (hi_max) { + negated = false; hi = lo - one; lo = vmin; + hi_max = hi >= vmax; + lo_min = true; + } + SASSERT(zero <= lo); + SASSERT(lo <= hi); + SASSERT(hi < numeral::power_of_two(bv_sz)); + } + if (lo_min) lo = vmin; + if (hi_max) hi = vmax; + TRACE("bv_bounds", tout << "record1 " << mk_ismt2_pp(v, m_m) << ":" << (negated ? "~[" : "[") << lo << ";" << hi << "]" << std::endl;); + if (lo > hi) return negated ? CONVERTED : UNSAT; + if (lo_min && hi_max) return negated ? UNSAT : CONVERTED; + nis.resize(nis.size() + 1); + nis.back().v = v; + nis.back().lo = lo; + nis.back().hi = hi; + nis.back().negated = negated; + return CONVERTED; +} + +bool bv_bounds::is_uleq(expr * e, expr * & v, numeral & c) { + // To detect the following rewrite from bv_rewriter: + // m().mk_and( + // m().mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)), + // m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b))); + expr * eq; + expr * eql; + expr * eqr; + expr * ule; + expr * ulel; + expr * uler; + numeral eqr_val, uleqr_val; + unsigned eqr_sz, uleqr_sz; + if (!m_m.is_and(e, eq, ule)) return false; + if (!m_m.is_eq(eq, eql, eqr)) return false; + if (!m_bv_util.is_bv_ule(ule, ulel, uler)) return false; + if (!m_bv_util.is_extract(eql)) return false; + expr * const eql0 = to_app(eql)->get_arg(0); + const unsigned eql0_sz = m_bv_util.get_bv_size(eql0); + if (!m_bv_util.get_extract_high(eql) == (eql0_sz - 1)) return false; + if (!m_bv_util.is_numeral(eqr, eqr_val, eqr_sz)) return false; + if (!eqr_val.is_zero()) return false; + if (!m_bv_util.is_extract(ulel)) return false; + expr * const ulel0 = to_app(ulel)->get_arg(0); + if (ulel0 != eql0) return false; + if ((m_bv_util.get_extract_high(ulel) + 1) != m_bv_util.get_extract_low(eql)) return false; + if (!m_bv_util.get_extract_low(ulel) == 0) return false; + if (!m_bv_util.is_numeral(uler, uleqr_val, uleqr_sz)) return false; + SASSERT(m_bv_util.get_bv_size(ulel0) == uleqr_sz + eqr_sz); + v = ulel0; + c = uleqr_val; + return true; +} + +bv_bounds::conv_res bv_bounds::convert(expr * e, vector& nis, bool negated) { + TRACE("bv_bounds", tout << "new constraint: " << (negated ? "~" : "" ) << mk_ismt2_pp(e, m_m) << std::endl;); + + if (m_m.is_not(e)) { + negated = !negated; + e = to_app(e)->get_arg(0); + } + + expr *lhs, *rhs; + numeral val, val1; + unsigned bv_sz1; + + if (0) { + if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) { + return record(to_app(lhs), val, val, negated, nis); + } + + if (m_m.is_eq(e, lhs, rhs) && to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz1)) { + return record(to_app(rhs), val, val, negated, nis); + } + } + + if (is_uleq(e, lhs, val) && to_bound(lhs)) { + return record(to_app(lhs), numeral::zero(), val, negated, nis); + } + + if (1) { + numeral rhs_val; + unsigned rhs_sz; + if (m_m.is_eq(e, lhs, rhs) + && m_bv_util.is_numeral(rhs, rhs_val, rhs_sz) + && rhs_val.is_zero() + && m_bv_util.is_extract(lhs)) { + expr * const lhs0 = to_app(lhs)->get_arg(0); + const unsigned lhs0_sz = m_bv_util.get_bv_size(lhs0); + if (m_bv_util.get_extract_high(lhs)+1 == lhs0_sz) { + const numeral u = numeral::power_of_two(m_bv_util.get_extract_low(lhs)) - numeral::one(); + return record(to_app(lhs0), numeral::zero(), u, negated, nis); + } + } + } + + if (m_bv_util.is_bv_ule(e, lhs, rhs)) { + unsigned bv_sz = m_bv_util.get_bv_size(lhs); + // unsigned inequality with one variable and a constant + if (to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz)) // v <= val + return record(to_app(lhs), numeral::zero(), val, negated, nis); + if (to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz)) // val <= v + return record(to_app(rhs), val, numeral::power_of_two(bv_sz) - numeral::one(), negated, nis); + + // unsigned inequality with one variable, constant, and addition + expr *t1, *t2; + if (m_bv_util.is_bv_add(lhs, t1, t2) + && m_bv_util.is_numeral(t1, val, bv_sz) + && to_bound(t2) + && t2 == rhs) { // val + v <= v + if (val.is_zero()) return negated ? UNSAT : CONVERTED; + SASSERT(val.is_pos()); + const numeral mod = numeral::power_of_two(bv_sz); + return record(to_app(rhs), mod - val, mod - numeral::one(), negated, nis); + } + + if (m_bv_util.is_bv_add(rhs, t1, t2) + && m_bv_util.is_numeral(t1, val, bv_sz) + && to_bound(t2) + && m_bv_util.is_numeral(lhs, val1, bv_sz1)) { // val1 <= val + v + SASSERT(bv_sz1 == bv_sz); + const numeral mod = numeral::power_of_two(bv_sz); + if (val1.is_zero()) return negated ? UNSAT : CONVERTED; + if (val1 < val) { + const numeral nl = mod - val; + const numeral nh = mod + val1 - val - numeral::one(); + return nl <= nh ? record(to_app(t2), nl, nh, !negated, nis) : (negated ? UNSAT : CONVERTED); + } + else { + const numeral l = val1 - val; + const numeral h = mod - val - numeral::one(); + return l <= h ? record(to_app(t2), l, h, negated, nis) : (negated ? CONVERTED : UNSAT); + } + } + + if (m_bv_util.is_bv_add(lhs, t1, t2) + && m_bv_util.is_numeral(t1, val, bv_sz) + && to_bound(t2) + && m_bv_util.is_numeral(rhs, val1, bv_sz1)) { // val + v <= val1 + SASSERT(bv_sz1 == bv_sz); + if (!val.is_pos() || !val1.is_pos()) return UNDEF; + const numeral mod = numeral::power_of_two(bv_sz); + if (val <= val1) { + const numeral nl = val1 - val + numeral::one(); + const numeral nh = mod - val - numeral::one(); + return nl <= nh ? record(to_app(t2), nl, nh, !negated, nis) : (negated ? UNSAT : CONVERTED); + } + else { + const numeral l = mod - val; + const numeral h = l + val1; + return record(to_app(t2), l, h, negated, nis); + } + } + + // v + c1 <= v + c2 + app * v1(NULL), *v2(NULL); + numeral val1, val2; + if (is_constant_add(bv_sz, lhs, v1, val1) + && is_constant_add(bv_sz, rhs, v2, val2) + && v1 == v2) { + if (val1 == val2) return negated ? UNSAT : CONVERTED; + const numeral mod = numeral::power_of_two(bv_sz); + if (val1 < val2) { + SASSERT(val1 < (mod - numeral::one())); + SASSERT(val2 > numeral::zero()); + return record(v1, mod - val2, mod - val1 - numeral::one(), !negated, nis); + } + else { + SASSERT(val1 > val2); + SASSERT(val2 < (mod - numeral::one())); + SASSERT(val1 > numeral::zero()); + return record(v1, mod - val1, mod - val2 - numeral::one(), negated, nis); + } + } + } + + if (m_bv_util.is_bv_sle(e, lhs, rhs)) { + unsigned bv_sz = m_bv_util.get_bv_size(lhs); + // signed inequality with one variable and a constant + if (to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz)) { // v <= val + val = m_bv_util.norm(val, bv_sz, true); + return convert_signed(to_app(lhs), -numeral::power_of_two(bv_sz - 1), val, negated, nis); + } + if (to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz)) { // val <= v + val = m_bv_util.norm(val, bv_sz, true); + return convert_signed(to_app(rhs), val, numeral::power_of_two(bv_sz - 1) - numeral::one(), negated, nis); + } + } + + return UNDEF; +} + +void bv_bounds::reset() { + intervals_map::iterator it = m_negative_intervals.begin(); + const intervals_map::iterator end = m_negative_intervals.end(); + for (; it != end; ++it) dealloc(it->m_value); +} + +br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result) { + const family_id fid = f->get_family_id(); + if (!m_m.is_bool(f->get_range())) return BR_FAILED; + const decl_kind k = f->get_decl_kind(); + if ((k != OP_OR && k != OP_AND) || num > limit) return BR_FAILED; + const bool negated = k == OP_OR; + vector nis; + vector lengths; + vector ignore; + unsigned nis_head = 0; + for (unsigned i = 0; i < num && m_okay; ++i) { + expr * const curr = args[i]; + const conv_res cr = convert(curr, nis, negated); + ignore.push_back(cr == UNDEF); + switch (cr) { + case UNDEF: continue; + case UNSAT: m_okay = false; break; + case CONVERTED: + { + for (unsigned i = nis_head; i < nis.size(); ++i) { + const ninterval& ni = nis[i]; + m_okay = m_okay && add_bound_unsigned(ni.v, ni.lo, ni.hi, ni.negated); + } + lengths.push_back(nis.size()); + nis_head = nis.size(); + break; + } + default: UNREACHABLE(); + } + } + if (!m_okay || !is_sat()) { + result = negated ? m_m.mk_true() : m_m.mk_false(); + return BR_DONE; + } + nis_head = 0; + unsigned count = 0; + expr_ref_vector nargs(m_m); + bool has_singls = false; + for (unsigned i = 0; i < num && m_okay; ++i) { + TRACE("bv_bounds", tout << "check red: " << mk_ismt2_pp(args[i], m_m) << std::endl;); + if (ignore[i]) { + TRACE("bv_bounds", tout << "unprocessed" << std::endl;); + nargs.push_back(args[i]); + continue; + } + SASSERT(nis_head <= lengths[count]); + const bool redundant = nis_head == lengths[count]; + bool is_singl = false; + if (nis_head < lengths[count]) { + app * const v = nis[nis_head].v; + numeral th, tl; + const unsigned bv_sz = m_bv_util.get_bv_size(v); + const bool has_upper = m_unsigned_uppers.find(v, th); + const bool has_lower = m_unsigned_lowers.find(v, tl); + const numeral& one = numeral::one(); + if (!has_lower) tl = numeral::zero(); + if (!has_upper) th = (numeral::power_of_two(bv_sz) - one); + TRACE("bv_bounds", tout << "bounds: " << mk_ismt2_pp(v, m_m) << "[" << tl << "-" << th << "]" << std::endl;); + is_singl = tl == th; + nis_head = lengths[count]; + } + if (!redundant && !is_singl) nargs.push_back(args[i]); + has_singls |= is_singl; + CTRACE("bv_bounds", redundant, tout << "redundant: " << mk_ismt2_pp(args[i], m_m) << std::endl;); + ++count; + } + + if (nargs.size() == num && !has_singls) return BR_FAILED; + + expr_ref eq(m_m); + for (bv_bounds::bound_map::iterator i = m_singletons.begin(); i != m_singletons.end(); ++i) { + app * const v = i->m_key; + const rational val = i->m_value; + eq = m_m.mk_eq(v, bvu().mk_numeral(val, v->get_decl()->get_range())); + if (negated) eq = m_m.mk_not(eq); + nargs.push_back(eq); + } + + switch (nargs.size()) { + case 0: result = negated ? m_m.mk_false() : m_m.mk_true(); return BR_DONE; + case 1: result = nargs.get(0); return BR_DONE; + default: result = negated ? m_m.mk_or(nargs.size(), nargs.c_ptr()) + : m_m.mk_and(nargs.size(), nargs.c_ptr()); + return BR_DONE; + } +} + +bool bv_bounds::add_constraint(expr* e) { + TRACE("bv_bounds", tout << "new constraint" << mk_ismt2_pp(e, m_m) << std::endl;); + if (!m_okay) return false; + + bool negated = false; + if (m_m.is_not(e)) { + negated = true; + e = to_app(e)->get_arg(0); + } + + expr *lhs, *rhs; + numeral val, val1; + unsigned bv_sz1; + + if (0) { + if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) { + return add_bound_unsigned(to_app(lhs), val, val, negated); + } + + if (m_m.is_eq(e, lhs, rhs) && to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz1)) { + return add_bound_unsigned(to_app(rhs), val, val, negated); + } + } + + + if (m_bv_util.is_bv_ule(e, lhs, rhs)) { + unsigned bv_sz = m_bv_util.get_bv_size(lhs); + // unsigned inequality with one variable and a constant + if (to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz)) // v <= val + return add_bound_unsigned(to_app(lhs), numeral::zero(), val, negated); + if (to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz)) // val <= v + return add_bound_unsigned(to_app(rhs), val, numeral::power_of_two(bv_sz) - numeral::one(), negated); + + // unsigned inequality with one variable, constant, and addition + expr *t1, *t2; + if (m_bv_util.is_bv_add(lhs, t1, t2) + && m_bv_util.is_numeral(t1, val, bv_sz) + && to_bound(t2) + && t2 == rhs) { // val + v <= v + if (!val.is_pos()) return m_okay; + const numeral mod = numeral::power_of_two(bv_sz); + return add_bound_unsigned(to_app(rhs), mod - val, mod - numeral::one(), negated); + } + + if (m_bv_util.is_bv_add(rhs, t1, t2) + && m_bv_util.is_numeral(t1, val, bv_sz) + && to_bound(t2) + && m_bv_util.is_numeral(lhs, val1, bv_sz1)) { // val1 <= val + v + SASSERT(bv_sz1 == bv_sz); + if (!val.is_pos() || !val1.is_pos()) return m_okay; + const numeral mod = numeral::power_of_two(bv_sz); + if (val1 < val) { + const numeral nl = mod - val; + const numeral nh = mod + val1 - val - numeral::one(); + return nl <= nh ? add_bound_unsigned(to_app(t2), nl, nh, !negated) : m_okay; + } + else { + const numeral l = val1 - val; + const numeral h = mod - val - numeral::one(); + return l <= h ? add_bound_unsigned(to_app(t2), l, h, negated) : m_okay; + } + } + + if (m_bv_util.is_bv_add(lhs, t1, t2) + && m_bv_util.is_numeral(t1, val, bv_sz) + && to_bound(t2) + && m_bv_util.is_numeral(rhs, val1, bv_sz1)) { // val + v <= val1 + SASSERT(bv_sz1 == bv_sz); + if (!val.is_pos() || !val1.is_pos()) return m_okay; + const numeral mod = numeral::power_of_two(bv_sz); + if (val <= val1) { + const numeral nl = val1 - val + numeral::one(); + const numeral nh = mod - val - numeral::one(); + return nl <= nh ? add_bound_unsigned(to_app(t2), nl, nh, !negated) : m_okay; + } + else { + const numeral l = mod - val; + const numeral h = l + val1; + return add_bound_unsigned(to_app(t2), l, h, negated); + } + } + + // v + c1 <= v + c2 + app * v1(NULL), *v2(NULL); + numeral val1, val2; + if (is_constant_add(bv_sz, lhs, v1, val1) + && is_constant_add(bv_sz, rhs, v2, val2) + && v1 == v2) { + if (val1 == val2) return m_okay; + const numeral mod = numeral::power_of_two(bv_sz); + if (val1 < val2) { + SASSERT(val1 < (mod - numeral::one())); + SASSERT(val2 > numeral::zero()); + return add_bound_unsigned(v1, mod - val2, mod - val1 - numeral::one(), !negated); + } + else { + SASSERT(val1 > val2); + SASSERT(val2 < (mod - numeral::one())); + SASSERT(val1 > numeral::zero()); + return add_bound_unsigned(v1, mod - val1, mod - val2 - numeral::one(), negated); + } + } + } + + if (m_bv_util.is_bv_sle(e, lhs, rhs)) { + unsigned bv_sz = m_bv_util.get_bv_size(lhs); + // signed inequality with one variable and a constant + if (to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz)) { // v <= val + val = m_bv_util.norm(val, bv_sz, true); + return add_bound_signed(to_app(lhs), -numeral::power_of_two(bv_sz - 1), val, negated); + } + if (to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz)) { // val <= v + val = m_bv_util.norm(val, bv_sz, true); + return add_bound_signed(to_app(rhs), val, numeral::power_of_two(bv_sz - 1) - numeral::one(), negated); + } + } + + return m_okay; +} + +bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) { + TRACE("bv_bounds", tout << "bound_unsigned " << mk_ismt2_pp(v, m_m) << ": " << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;); + const unsigned bv_sz = m_bv_util.get_bv_size(v); + const numeral& zero = numeral::zero(); + const numeral& one = numeral::one(); + SASSERT(zero <= a); + SASSERT(a <= b); + SASSERT(b < numeral::power_of_two(bv_sz)); + const bool a_min = a == zero; + const bool b_max = b == (numeral::power_of_two(bv_sz) - one); + if (negate) { + if (a_min && b_max) return m_okay = false; + if (a_min) return bound_lo(v, b + one); + if (b_max) return bound_up(v, a - one); + return add_neg_bound(v, a, b); + } + else { + if (!a_min) m_okay &= bound_lo(v, a); + if (!b_max) m_okay &= bound_up(v, b); + return m_okay; + } +} + +bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, bool negate, vector& nis) { + TRACE("bv_bounds", tout << "convert_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;); + const unsigned bv_sz = m_bv_util.get_bv_size(v); + SASSERT(a <= b); + const numeral& zero = numeral::zero(); + const numeral& one = numeral::one(); + const bool a_neg = a < zero; + const bool b_neg = b < zero; + if (!a_neg && !b_neg) return record(v, a, b, negate, nis); + const numeral mod = numeral::power_of_two(bv_sz); + if (a_neg && b_neg) return record(v, mod + a, mod + b, negate, nis); + SASSERT(a_neg && !b_neg); + if (negate) { + const conv_res r1 = record(v, mod + a, mod - one, true, nis); + const conv_res r2 = record(v, zero, b, true, nis); + return r1 == UNSAT || r2 == UNSAT ? UNSAT : CONVERTED; + } + else { + const numeral l = b + one; + const numeral u = mod + a - one; + return l <= u ? record(v, l, u, true, nis) : CONVERTED; + } +} + +bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) { + TRACE("bv_bounds", tout << "bound_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~" : " ") << a << ";" << b << std::endl;); + const unsigned bv_sz = m_bv_util.get_bv_size(v); + SASSERT(a <= b); + const numeral& zero = numeral::zero(); + const numeral& one = numeral::one(); + const bool a_neg = a < zero; + const bool b_neg = b < zero; + if (!a_neg && !b_neg) return add_bound_unsigned(v, a, b, negate); + const numeral mod = numeral::power_of_two(bv_sz); + if (a_neg && b_neg) return add_bound_unsigned(v, mod + a, mod + b, negate); + SASSERT(a_neg && !b_neg); + if (negate) { + return add_bound_unsigned(v, mod + a, mod - one, true) + && add_bound_unsigned(v, zero, b, true); + } + else { + const numeral l = b + one; + const numeral u = mod + a - one; + return (l <= u) ? add_bound_unsigned(v, l, u, true) : m_okay; + } +} + +bool bv_bounds::bound_lo(app * v, numeral l) { + SASSERT(in_range(v, l)); + TRACE("bv_bounds", tout << "lower " << mk_ismt2_pp(v, m_m) << ":" << l << std::endl;); + // l <= v + bound_map::obj_map_entry * const entry = m_unsigned_lowers.insert_if_not_there2(v, l); + if (!(entry->get_data().m_value < l)) return m_okay; + // improve bound + entry->get_data().m_value = l; + return m_okay; +} + +bool bv_bounds::bound_up(app * v, numeral u) { + SASSERT(in_range(v, u)); + TRACE("bv_bounds", tout << "upper " << mk_ismt2_pp(v, m_m) << ":" << u << std::endl;); + // v <= u + bound_map::obj_map_entry * const entry = m_unsigned_uppers.insert_if_not_there2(v, u); + if (!(u < entry->get_data().m_value)) return m_okay; + // improve bound + entry->get_data().m_value = u; + return m_okay; +} + +bool bv_bounds::add_neg_bound(app * v, numeral a, numeral b) { + TRACE("bv_bounds", tout << "negative bound " << mk_ismt2_pp(v, m_m) << ":" << a << ";" << b << std::endl;); + bv_bounds::interval negative_interval(a, b); + SASSERT(m_bv_util.is_bv(v)); + SASSERT(a >= numeral::zero()); + SASSERT(b < numeral::power_of_two(m_bv_util.get_bv_size(v))); + SASSERT(a <= b); + + intervals_map::obj_map_entry * const e = m_negative_intervals.find_core(v); + intervals * ivs(NULL); + if (e == 0) { + ivs = alloc(intervals); + m_negative_intervals.insert(v, ivs); + } + else { + ivs = e->get_data().get_value(); + } + ivs->push_back(negative_interval); + return m_okay; +} + + +bool bv_bounds::is_sat() { + if (!m_okay) return false; + obj_hashtable seen; + obj_hashtable::entry *dummy; + + for (bound_map::iterator i = m_unsigned_lowers.begin(); i != m_unsigned_lowers.end(); ++i) { + app * const v = i->m_key; + if (!seen.insert_if_not_there_core(v, dummy)) continue; + if (!is_sat(v)) return false; + } + + for (bound_map::iterator i = m_unsigned_uppers.begin(); i != m_unsigned_uppers.end(); ++i) { + app * const v = i->m_key; + if (!seen.insert_if_not_there_core(v, dummy)) continue; + if (!is_sat(v)) return false; + } + + for (intervals_map::iterator i = m_negative_intervals.begin(); i != m_negative_intervals.end(); ++i) { + app * const v = i->m_key; + if (!seen.insert_if_not_there_core(v, dummy)) continue; + if (!is_sat(v)) return false; + } + + return true; +} + +struct interval_comp_t { + bool operator() (bv_bounds::interval i, bv_bounds::interval j) { + return (i.first < j.first); + } +} interval_comp; + + +void bv_bounds::record_singleton(app * v, numeral& singleton_value) { + TRACE("bv_bounds", tout << "singleton:" << mk_ismt2_pp(v, m_m) << ":" << singleton_value << std::endl;); + SASSERT(!m_singletons.find(v, singleton_value)); + m_singletons.insert(v, singleton_value); +} + +bool bv_bounds::is_sat(app * v) { + TRACE("bv_bounds", tout << "is_sat " << mk_ismt2_pp(v, m_m) << std::endl;); + const bool rv = is_sat_core(v); + TRACE("bv_bounds", tout << "is_sat " << mk_ismt2_pp(v, m_m) << "\nres: " << rv << std::endl;); + return rv; +} + +bool bv_bounds::is_sat_core(app * v) { + SASSERT(m_bv_util.is_bv(v)); + if (!m_okay) return false; + func_decl * const d = v->get_decl(); + unsigned const bv_sz = m_bv_util.get_bv_size(v); + numeral lower, upper; + const bool has_upper = m_unsigned_uppers.find(v, upper); + const bool has_lower = m_unsigned_lowers.find(v, lower); + if (has_upper && has_lower && lower > upper) return false; + const numeral& one = numeral::one(); + if (!has_lower) lower = numeral::zero(); + if (!has_upper) upper = (numeral::power_of_two(bv_sz) - one); + TRACE("bv_bounds", tout << "is_sat bound:" << lower << "-" << upper << std::endl;); + intervals * negative_intervals(NULL); + const bool has_neg_intervals = m_negative_intervals.find(v, negative_intervals); + bool is_sat(false); + numeral new_lo = lower; + numeral new_hi = lower - one; + numeral ptr = lower; + if (has_neg_intervals) { + SASSERT(negative_intervals != NULL); + std::sort(negative_intervals->begin(), negative_intervals->end(), interval_comp); + intervals::const_iterator e = negative_intervals->end(); + for (intervals::const_iterator i = negative_intervals->begin(); i != e; ++i) { + const numeral negative_lower = i->first; + const numeral negative_upper = i->second; + if (ptr > negative_upper) continue; + if (ptr < negative_lower) { + if (!is_sat) new_lo = ptr; + new_hi = negative_lower - one; + if (new_hi > upper) new_hi = upper; + is_sat = true; + } + TRACE("bv_bounds", tout << "is_sat new_lo, new_hi:" << new_lo << "-" << new_hi << std::endl;); + ptr = negative_upper + one; + TRACE("bv_bounds", tout << "is_sat ptr, new_hi:" << ptr << "-" << new_hi << std::endl;); + if (ptr > upper) break; + } + } + + if (ptr <= upper) { + if (!is_sat) new_lo = ptr; + new_hi = upper; + is_sat = true; + } + if (new_hi < upper) bound_up(v, new_hi); + if (new_lo > lower) bound_lo(v, new_lo); + TRACE("bv_bounds", tout << "is_sat new_lo, new_hi:" << new_lo << "-" << new_hi << std::endl;); + + const bool is_singleton = is_sat && new_hi == new_lo; + if (is_singleton) record_singleton(v, new_lo); + + return is_sat; +} diff --git a/src/ast/rewriter/bv_bounds.h b/src/ast/rewriter/bv_bounds.h new file mode 100644 index 000000000..eeefc2c11 --- /dev/null +++ b/src/ast/rewriter/bv_bounds.h @@ -0,0 +1,130 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + bv_bounds.h + + Abstract: + + A class used to determine bounds on bit-vector variables. + The satisfiability procedure is polynomial. + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: + --*/ +#ifndef BV_BOUNDS_H_23754 +#define BV_BOUNDS_H_23754 +#include"ast.h" +#include"bv_decl_plugin.h" +#include"rewriter_types.h" + +/* \brief A class to analyze constraints on bit vectors. + + The objective is to identify inconsistencies in polynomial time. + All bounds/intervals are closed. Methods that add new constraints + return false if inconsistency has already been reached. + Typical usage is to call repeatedly add_constraint(e) and call is_sat() in the end. + */ +class bv_bounds { +public: + typedef rational numeral; + typedef std::pair interval; + typedef obj_map bound_map; + bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {}; + ~bv_bounds(); +public: // bounds addition methods + br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result); + + /** \brief Add a constraint to the system. + + The added constraints are to be considered by is_sat. + Currently, only special types of inequalities are supported, e.g. v <= v+1. + Other constraints are ignored. + Returns false if the system became trivially unsatisfiable + **/ + bool add_constraint(expr* e); + + bool bound_up(app * v, numeral u); // v <= u + bool bound_lo(app * v, numeral l); // l <= v + inline bool add_neg_bound(app * v, numeral a, numeral b); // not (a<=v<=b) + bool add_bound_signed(app * v, numeral a, numeral b, bool negate); + bool add_bound_unsigned(app * v, numeral a, numeral b, bool negate); +public: + bool is_sat(); ///< Determine if the set of considered constraints is satisfiable. + bool is_okay(); + const bound_map& singletons() { return m_singletons; } + bv_util& bvu() { return m_bv_util; } + void reset(); +protected: + struct ninterval { + //ninterval(app * v, numeral lo, numeral hi, bool negated) : v(v), lo(lo), hi(hi), negated(negated) {} + app * v; + numeral lo, hi; + bool negated; + }; + enum conv_res { CONVERTED, UNSAT, UNDEF }; + conv_res convert(expr * e, vector& nis, bool negated); + conv_res record(app * v, numeral lo, numeral hi, bool negated, vector& nis); + conv_res convert_signed(app * v, numeral a, numeral b, bool negate, vector& nis); + + typedef vector intervals; + typedef obj_map intervals_map; + ast_manager& m_m; + bound_map m_unsigned_lowers; + bound_map m_unsigned_uppers; + intervals_map m_negative_intervals; + bound_map m_singletons; + bv_util m_bv_util; + bool m_okay; + bool is_sat(app * v); + bool is_sat_core(app * v); + inline bool in_range(app *v, numeral l); + inline bool is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val); + void record_singleton(app * v, numeral& singleton_value); + inline bool to_bound(const expr * e) const; + bool is_uleq(expr * e, expr * & v, numeral & c); +}; + + +inline bool bv_bounds::is_okay() { return m_okay; } + +inline bool bv_bounds::to_bound(const expr * e) const { + return is_app(e) && m_bv_util.is_bv(e) + && !m_bv_util.is_bv_add(e) + && !m_bv_util.is_numeral(e); +} + +inline bool bv_bounds::in_range(app *v, bv_bounds::numeral n) { + const unsigned bv_sz = m_bv_util.get_bv_size(v); + const bv_bounds::numeral zero(0); + const bv_bounds::numeral mod(rational::power_of_two(bv_sz)); + return (zero <= n) && (n < mod); +} + +inline bool bv_bounds::is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val) { + SASSERT(e && !v); + SASSERT(m_bv_util.get_bv_size(e) == bv_sz); + expr *lhs(NULL), *rhs(NULL); + if (!m_bv_util.is_bv_add(e, lhs, rhs)) { + v = to_app(e); + val = rational(0); + return true; + } + if (to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz)) { + v = to_app(lhs); + return true; + } + if (to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz)) { + v = to_app(rhs); + return true; + } + return false; +} + + +#endif /* BV_BOUNDS_H_23754 */ diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 07e97364e..dcb5ba681 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -29,12 +29,18 @@ void bv_rewriter::updt_local_params(params_ref const & _p) { m_mul2concat = p.mul2concat(); m_bit2bool = p.bit2bool(); m_trailing = p.bv_trailing(); + m_urem_simpl = p.bv_urem_simpl(); m_blast_eq_value = p.blast_eq_value(); m_split_concat_eq = p.split_concat_eq(); m_udiv2mul = p.udiv2mul(); m_bvnot2arith = p.bvnot2arith(); + m_bvnot_simpl = p.bv_not_simpl(); m_bv_sort_ac = p.bv_sort_ac(); m_mkbv2num = _p.get_bool("mkbv2num", false); + m_extract_prop = p.bv_extract_prop(); + m_ite2id = p.bv_ite2id(); + m_le_extra = p.bv_le_extra(); + set_sort_sums(p.bv_sort_ac()); } void bv_rewriter::updt_params(params_ref const & p) { @@ -234,6 +240,198 @@ br_status bv_rewriter::mk_slt(expr * a, expr * b, expr_ref & result) { return BR_REWRITE2; } +// short-circuited concat +expr * bv_rewriter::concat(unsigned num_args, expr * const * args) { + SASSERT(num_args); + switch (num_args) { + case 0: return m_util.mk_concat(num_args, args); + case 1: return args[0]; + default: return m_util.mk_concat(num_args, args); + } +} + +// finds a commonality in sums, e.g. 2 + x + y and 5 + x + y +bool bv_rewriter::are_eq_upto_num(expr * _a, expr * _b, + expr_ref& common, + numeral& a0_val, numeral& b0_val) { + const bool aadd = m_util.is_bv_add(_a); + const bool badd = m_util.is_bv_add(_b); + const bool has_num_a = aadd && to_app(_a)->get_num_args() && is_numeral(to_app(_a)->get_arg(0)); + const bool has_num_b = badd && to_app(_b)->get_num_args() && is_numeral(to_app(_b)->get_arg(0)); + a0_val = numeral::zero(); + b0_val = numeral::zero(); + if (!aadd && !badd) { + if (_a == _b) { + common = _a; + return true; + } else { + return false; + } + } + if (!aadd && badd) { + if (to_app(_a)->get_num_args() != 2 || !has_num_a || to_app(_a)->get_arg(0) != _b) + return false; + common = _b; + return true; + } + if (aadd && !badd) { + if (to_app(_b)->get_num_args() != 2 || !has_num_b || to_app(_b)->get_arg(0) != _a) + return false; + common = _a; + return true; + } + SASSERT(aadd && badd); + app * const a = to_app(_a); + app * const b = to_app(_b); + const unsigned numa = a->get_num_args(); + const unsigned numb = b->get_num_args(); + if (!numa || !numb) return false; + if ((numa - (has_num_a ? 1 : 0)) != (numb - (has_num_b ? 1 : 0))) return false; + unsigned ai = has_num_a ? 1 : 0; + unsigned bi = has_num_b ? 1 : 0; + while (ai < numa) { + if (a->get_arg(ai) != b->get_arg(bi)) return false; + ++ai; + ++bi; + } + a0_val = numeral::zero(); + b0_val = numeral::zero(); + const unsigned sz = m_util.get_bv_size(a); + unsigned a0_sz(sz), b0_sz(sz); + if (has_num_a) is_numeral(a->get_arg(0), a0_val, a0_sz); + if (has_num_b) is_numeral(b->get_arg(0), b0_val, b0_sz); + SASSERT(a0_sz == m_util.get_bv_size(a) && b0_sz == m_util.get_bv_size(a)); + if (has_num_a && numa > 2) { + common = m().mk_app(m_util.get_fid(), add_decl_kind(), numa - 1, a->get_args() + 1); + } + else { + common = has_num_a ? a->get_arg(1) : a; + } + return true; +} + +// simplifies expressions as (bvuleq (X + c1) (X + c2)) for some common expression X and numerals c1, c2 +br_status bv_rewriter::rw_leq_overflow(bool is_signed, expr * a, expr * b, expr_ref & result) { + if (is_signed) return BR_FAILED; + expr_ref common(m()); + numeral a0_val, b0_val; + if (!are_eq_upto_num(a, b, common, a0_val, b0_val)) return BR_FAILED; + SASSERT(a0_val.is_nonneg() && b0_val.is_nonneg()); + const unsigned sz = m_util.get_bv_size(a); + if (a0_val == b0_val) { + result = m().mk_true(); + return BR_DONE; + } + if (a0_val < b0_val) { + result = m_util.mk_ule(m_util.mk_numeral(b0_val - a0_val, sz), b); + return BR_REWRITE2; + } + SASSERT(a0_val > b0_val); + SASSERT(!a0_val.is_zero()); + const numeral lower = rational::power_of_two(sz) - a0_val; + const numeral upper = rational::power_of_two(sz) - b0_val - numeral::one(); + if (lower == upper) { + result = m().mk_eq(common, mk_numeral(lower, sz)); + } + else if (b0_val.is_zero()) { + result = m_util.mk_ule(mk_numeral(lower, sz), common); + } + else { + SASSERT(lower.is_pos()); + result = m().mk_and(m_util.mk_ule(mk_numeral(lower, sz), common), + m_util.mk_ule(common, mk_numeral(upper, sz))); + } + return BR_REWRITE2; +} + +// simplification for leq comparison between two concatenations +br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr_ref & result) { + if (!m_util.is_concat(_a) || !m_util.is_concat(_b)) + return BR_FAILED; + const app * const a = to_app(_a); + const app * const b = to_app(_b); + const unsigned numa = a->get_num_args(); + const unsigned numb = b->get_num_args(); + const unsigned num_min = std::min(numa, numb); + + if (numa && numb) { // first arg numeral + numeral af, bf; + unsigned af_sz, bf_sz; + if ( is_numeral(a->get_arg(0), af, af_sz) + && is_numeral(b->get_arg(0), bf, bf_sz) ) { + const unsigned sz_min = std::min(af_sz, bf_sz); + const numeral hi_af = m_util.norm(af_sz > sz_min ? div(af, rational::power_of_two(af_sz - sz_min)) : af, + sz_min, is_signed); + const numeral hi_bf = m_util.norm(bf_sz > sz_min ? div(bf, rational::power_of_two(bf_sz - sz_min)) : bf, + sz_min, is_signed); + if (hi_af != hi_bf) { + result = hi_af < hi_bf ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + expr_ref new_a(m()); + expr_ref new_b(m()); + if (af_sz > sz_min) { + ptr_buffer new_args; + new_args.push_back(mk_numeral(af, af_sz - sz_min)); + for (unsigned i = 1; i < numa; ++i) new_args.push_back(a->get_arg(i)); + new_a = concat(new_args.size(), new_args.c_ptr()); + } else { + new_a = concat(numa - 1, a->get_args() + 1); + } + if (bf_sz > sz_min) { + ptr_buffer new_args; + new_args.push_back(mk_numeral(bf, bf_sz - sz_min)); + for (unsigned i = 1; i < numb; ++i) new_args.push_back(b->get_arg(i)); + new_b = concat(new_args.size(), new_args.c_ptr()); + } else { + new_b = concat(numb - 1, b->get_args() + 1); + } + result = m_util.mk_ule(new_a, new_b); + return BR_REWRITE2; + } + } + + { // common prefix + unsigned common = 0; + while (common < num_min && m().are_equal(a->get_arg(common), b->get_arg(common))) ++common; + SASSERT((common == numa) == (common == numb)); + if (common == numa) { + SASSERT(0); // shouldn't get here as both sides are equal + result = m().mk_true(); + return BR_DONE; + } + if (common > 0) { + result = m_util.mk_ule(concat(numa - common, a->get_args() + common), + concat(numb - common, b->get_args() + common)); + return BR_REWRITE2; + } + } + + { // common postfix + unsigned new_numa = a->get_num_args(); + unsigned new_numb = b->get_num_args(); + while (new_numa && new_numb) { + expr * const last_a = a->get_arg(new_numa - 1); + expr * const last_b = b->get_arg(new_numb - 1); + if (!m().are_equal(last_a, last_b)) break; + new_numa--; + new_numb--; + } + if (new_numa == 0) { + SASSERT(0); // shouldn't get here as both sides are equal + result = m().mk_true(); + return BR_DONE; + } + if (new_numa != numa) { + result = is_signed ? m_util.mk_sle(concat(new_numa, a->get_args()), concat(new_numb, b->get_args())) + : m_util.mk_ule(concat(new_numa, a->get_args()), concat(new_numb, b->get_args())); + return BR_REWRITE2; + } + } + + return BR_FAILED; +} + br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref & result) { numeral r1, r2, r3; @@ -309,6 +507,24 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref return BR_REWRITE2; } + if (m_le_extra) { + const br_status cst = rw_leq_concats(is_signed, a, b, result); + if (cst != BR_FAILED) { + TRACE("le_extra", tout << (is_signed ? "bv_sle\n" : "bv_ule\n") + << mk_ismt2_pp(a, m(), 2) << "\n" << mk_ismt2_pp(b, m(), 2) << "\n--->\n"<< mk_ismt2_pp(result, m(), 2) << "\n";); + return cst; + } + } + + if (m_le_extra) { + const br_status cst = rw_leq_overflow(is_signed, a, b, result); + if (cst != BR_FAILED) { + TRACE("le_extra", tout << (is_signed ? "bv_sle\n" : "bv_ule\n") + << mk_ismt2_pp(a, m(), 2) << "\n" << mk_ismt2_pp(b, m(), 2) << "\n--->\n"<< mk_ismt2_pp(result, m(), 2) << "\n";); + return cst; + } + } + #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))) { // @@ -366,6 +582,89 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref return BR_FAILED; } +// attempt to chop off bits that are above the position high for bv_mul and bv_add, +// returns how many bits were chopped off +// e.g. (bvadd(concat #b11 p) #x1)) with high=1, returns 2 and sets result = p + #b01 +// the sz of results is the sz of arg minus the return value +unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & result) { + if (!m_util.is_bv_add(arg) && !m_util.is_bv_mul(arg)) + return 0; + const unsigned sz = m_util.get_bv_size(arg); + const unsigned to_remove = high + 1 < sz ? sz - high - 1 : 0; + if (to_remove == 0) + return 0; // high goes to the top, nothing to do + const app * const a = to_app(arg); + const unsigned num = a->get_num_args(); + bool all_numerals = true; + unsigned removable = to_remove; + numeral val; + unsigned curr_first_sz = -1; + // calculate how much can be removed + for (unsigned i = 0; i < num; i++) { + expr * const curr = a->get_arg(i); + const bool curr_is_conc = m_util.is_concat(curr); + if (curr_is_conc && to_app(curr)->get_num_args() == 0) continue; + expr * const curr_first = curr_is_conc ? to_app(curr)->get_arg(0) : curr; + if (!all_numerals) { + if (removable != m_util.get_bv_size(curr_first)) + return 0; + continue; + } + if (is_numeral(curr_first, val, curr_first_sz)) { + removable = std::min(removable, curr_first_sz); + } else { + all_numerals = false; + curr_first_sz = m_util.get_bv_size(curr_first); + if (curr_first_sz > removable) return 0; + removable = curr_first_sz; + } + if (removable == 0) return 0; + } + // perform removal + SASSERT(removable <= to_remove); + const unsigned new_sz = sz - removable; + ptr_buffer new_args; + ptr_buffer new_concat_args; + for (unsigned i = 0; i < num; i++) { + expr * const curr = a->get_arg(i); + const bool curr_is_conc = m_util.is_concat(curr); + if (curr_is_conc && to_app(curr)->get_num_args() == 0) continue; + expr * const curr_first = curr_is_conc ? to_app(curr)->get_arg(0) : curr; + expr * new_first = NULL; + if (is_numeral(curr_first, val, curr_first_sz)) { + SASSERT(curr_first_sz >= removable); + const unsigned new_num_sz = curr_first_sz - removable; + new_first = new_num_sz ? mk_numeral(val, new_num_sz) : NULL; + } + expr * new_arg = NULL; + if (curr_is_conc) { + const unsigned conc_num = to_app(curr)->get_num_args(); + if (new_first) { + new_concat_args.reset(); + new_concat_args.push_back(new_first); + for (unsigned j = 1; j < conc_num; ++j) + new_concat_args.push_back(to_app(curr)->get_arg(j)); + new_arg = m_util.mk_concat(new_concat_args.size(), new_concat_args.c_ptr()); + } else { + // remove first element of concat + expr * const * const old_conc_args = to_app(curr)->get_args(); + switch (conc_num) { + case 0: UNREACHABLE(); break; + case 1: new_arg = NULL; break; + case 2: new_arg = to_app(curr)->get_arg(1); break; + default: new_arg = m_util.mk_concat(conc_num - 1, old_conc_args + 1); + } + } + } else { + new_arg = new_first; + } + if (new_arg) new_args.push_back(new_arg); + } + result = m().mk_app(get_fid(), a->get_decl()->get_decl_kind(), new_args.size(), new_args.c_ptr()); + SASSERT(m_util.is_bv(result)); + return removable; +} + br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ref & result) { unsigned sz = get_bv_size(arg); SASSERT(sz > 0); @@ -469,6 +768,17 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ return BR_REWRITE2; } + if (m_extract_prop && (high >= low)) { + expr_ref ep_res(m()); + const unsigned ep_rm = propagate_extract(high, arg, ep_res); + if (ep_rm != 0) { + result = m_mk_extract(high, low, ep_res); + TRACE("extract_prop", tout << mk_ismt2_pp(arg, m()) << "\n[" << high <<"," << low << "]\n" << ep_rm << "---->\n" + << mk_ismt2_pp(result.get(), m()) << "\n";); + return BR_REWRITE2; + } + } + if (m().is_ite(arg)) { result = m().mk_ite(to_app(arg)->get_arg(0), m_mk_extract(high, low, to_app(arg)->get_arg(1)), @@ -842,6 +1152,22 @@ bool bv_rewriter::is_minus_one_core(expr * arg) const { return false; } +bool bv_rewriter::is_negatable(expr * arg, expr_ref& x) { + numeral r; + unsigned bv_size; + if (is_numeral(arg, r, bv_size)) { + r = bitwise_not(bv_size, r); + x = mk_numeral(r, bv_size); + return true; + } + if (m_util.is_bv_not(arg)) { + SASSERT(to_app(arg)->get_num_args() == 1); + x = to_app(arg)->get_arg(0); + return true; + } + return false; +} + bool bv_rewriter::is_x_minus_one(expr * arg, expr * & x) { if (is_add(arg) && to_app(arg)->get_num_args() == 2) { if (is_minus_one_core(to_app(arg)->get_arg(0))) { @@ -1046,6 +1372,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { return BR_FAILED; } + br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_ref & result) { expr_ref_buffer new_args(m()); numeral v1; @@ -1534,6 +1861,35 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) { return BR_REWRITE1; } + if (m_bvnot_simpl) { + expr *s(0), *t(0); + if (m_util.is_bv_mul(arg, s, t)) { + // ~(-1 * x) --> (x - 1) + bv_size = m_util.get_bv_size(s); + if (m_util.is_allone(s)) { + rational minus_one = (rational::power_of_two(bv_size) - rational::one()); + result = m_util.mk_bv_add(m_util.mk_numeral(minus_one, bv_size), t); + return BR_REWRITE1; + } + if (m_util.is_allone(t)) { + rational minus_one = (rational::power_of_two(bv_size) - rational::one()); + result = m_util.mk_bv_add(m_util.mk_numeral(minus_one, bv_size), s); + return BR_REWRITE1; + } + } + if (m_util.is_bv_add(arg, s, t)) { + expr_ref ns(m()); + expr_ref nt(m()); + // ~(x + y) --> (~x + ~y + 1) when x and y are easy to negate + if (is_negatable(t, nt) && is_negatable(s, ns)) { + bv_size = m_util.get_bv_size(s); + expr * nargs[3] = { m_util.mk_numeral(rational::one(), bv_size), ns.get(), nt.get() }; + result = m().mk_app(m_util.get_fid(), OP_BADD, 3, nargs); + return BR_REWRITE1; + } + } + } + return BR_FAILED; } @@ -2076,6 +2432,16 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { return BR_FAILED; } +bool bv_rewriter::is_urem_any(expr * e, expr * & dividend, expr * & divisor) { + if (!m_util.is_bv_urem(e) && !m_util.is_bv_uremi(e)) + return false; + const app * const a = to_app(e); + SASSERT(a->get_num_args() == 2); + dividend = a->get_arg(0); + divisor = a->get_arg(1); + return true; +} + br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (lhs == rhs) { result = m().mk_true(); @@ -2127,6 +2493,25 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { return st; } + if (m_urem_simpl) { + expr * dividend; + expr * divisor; + numeral divisor_val, rhs_val; + unsigned divisor_sz, rhs_sz; + if (is_urem_any(lhs, dividend, divisor) + && is_numeral(rhs, rhs_val, rhs_sz) + && is_numeral(divisor, divisor_val, divisor_sz)) { + if (rhs_val >= divisor_val) {//(= (bvurem x c1) c2) where c2 >= c1 + result = m().mk_false(); + return BR_DONE; + } + if ((divisor_val + rhs_val) >= rational::power_of_two(divisor_sz)) {//(= (bvurem x c1) c2) where c1+c2 >= 2^width + result = m().mk_eq(dividend, rhs); + return BR_REWRITE2; + } + } + } + expr_ref new_lhs(m()); expr_ref new_rhs(m()); @@ -2194,6 +2579,55 @@ br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & res return BR_FAILED; } +br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { + TRACE("bv_ite", tout << "mk_ite_core:\n" << mk_ismt2_pp(c, m()) << "?\n" + << mk_ismt2_pp(t, m()) << "\n:" << mk_ismt2_pp(e, m()) << "\n";); + if (m().are_equal(t, e)) { + result = e; + return BR_REWRITE1; + } + if (m().is_not(c)) { + result = m().mk_ite(to_app(c)->get_arg(0), e, t); + return BR_REWRITE1; + } + + if (m_ite2id && m().is_eq(c) && is_bv(t) && is_bv(e)) { + // detect when ite is actually some simple function based on the pattern (lhs=rhs) ? t : e + expr * lhs = to_app(c)->get_arg(0); + expr * rhs = to_app(c)->get_arg(1); + + if (is_bv(rhs)) { + if (is_numeral(lhs)) + std::swap(lhs, rhs); + + if ( (m().are_equal(lhs, t) && m().are_equal(rhs, e)) + || (m().are_equal(lhs, e) && m().are_equal(rhs, t))) { + // (a = b ? a : b) is b. (a = b ? b : a) is a + result = e; + return BR_REWRITE1; + } + + const unsigned sz = m_util.get_bv_size(rhs); + if (sz == 1) { // detect (lhs = N) ? C : D, where N, C, D are 1 bit numberals + numeral rhs_n, e_n, t_n; + unsigned rhs_sz, e_sz, t_sz; + if (is_numeral(rhs, rhs_n, rhs_sz) + && is_numeral(t, t_n, t_sz) && is_numeral(e, e_n, e_sz)) { + if (t_sz == 1) { + SASSERT(rhs_sz == sz && e_sz == sz && t_sz == sz); + SASSERT(!m().are_equal(t, e)); + result = m().are_equal(rhs, t) ? lhs : m_util.mk_bv_not(lhs); + return BR_REWRITE1; + } + } + } + } + + + } + return BR_FAILED; +} + br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); unsigned bv_sz; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index a8db05013..5d47fb99d 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -56,11 +56,16 @@ class bv_rewriter : public poly_rewriter { bool m_bit2bool; bool m_blast_eq_value; bool m_mkbv2num; + bool m_ite2id; bool m_split_concat_eq; bool m_udiv2mul; bool m_bvnot2arith; bool m_bv_sort_ac; bool m_trailing; + bool m_extract_prop; + bool m_bvnot_simpl; + bool m_le_extra; + bool m_urem_simpl; bool is_zero_bit(expr * x, unsigned idx); @@ -70,13 +75,19 @@ class bv_rewriter : public poly_rewriter { br_status mk_sle(expr * a, expr * b, expr_ref & result); br_status mk_sge(expr * a, expr * b, expr_ref & result); br_status mk_slt(expr * a, expr * b, expr_ref & result); + br_status rw_leq_concats(bool is_signed, expr * a, expr * b, expr_ref & result); + bool are_eq_upto_num(expr * a, expr * b, expr_ref& common, numeral& a0_val, numeral& b0_val); + br_status rw_leq_overflow(bool is_signed, expr * _a, expr * _b, expr_ref & result); br_status mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref & result); + br_status fuse_concat(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_concat(unsigned num_args, expr * const * args, expr_ref & result); + unsigned propagate_extract(unsigned high, expr * arg, expr_ref & result); br_status mk_extract(unsigned high, unsigned low, expr * arg, expr_ref & result); br_status mk_repeat(unsigned n, expr * arg, expr_ref & result); br_status mk_zero_extend(unsigned n, expr * arg, expr_ref & result); br_status mk_sign_extend(unsigned n, expr * arg, expr_ref & result); + bool is_negatable(expr * arg, expr_ref& x); br_status mk_bv_not(expr * arg, expr_ref & result); br_status mk_bv_or(unsigned num, expr * const * args, expr_ref & result); br_status mk_bv_xor(unsigned num, expr * const * args, expr_ref & result); @@ -139,6 +150,7 @@ class bv_rewriter : public poly_rewriter { void updt_local_params(params_ref const & p); + expr * concat(unsigned num_args, expr * const * args); public: bv_rewriter(ast_manager & m, params_ref const & p = params_ref()): poly_rewriter(m, p), @@ -167,7 +179,9 @@ public: result = m().mk_app(f, num_args, args); } + bool is_urem_any(expr * e, expr * & dividend, expr * & divisor); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul); bool hi_div0() const { return m_hi_div0; } diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg index 0f0163fb1..984a48b37 100644 --- a/src/ast/rewriter/bv_rewriter_params.pyg +++ b/src/ast/rewriter/bv_rewriter_params.pyg @@ -10,5 +10,10 @@ def_module_params(module_name='rewriter', ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"), ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"), ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"), - ("bv_trailing", BOOL, False, "lean removal of trailing zeros") + ("bv_trailing", BOOL, False, "lean removal of trailing zeros"), + ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"), + ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"), + ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"), + ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications"), + ("bv_urem_simpl", BOOL, False, "additional simplification for bvurem") )) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index 31e9121ec..f0b96a91f 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -36,11 +36,14 @@ struct bv_trailing::imp { : m_mk_extract(mk_extract) , m_util(mk_extract.bvutil()) , m(mk_extract.m()) { + TRACE("bv-trailing", tout << "ctor\n";); + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) m_count_cache[i] = NULL; } virtual ~imp() { + TRACE("bv-trailing", tout << "dtor\n";); reset_cache(0); } @@ -337,6 +340,7 @@ struct bv_trailing::imp { if (depth == 0) return; if (m_count_cache[depth] == NULL) m_count_cache[depth] = alloc(map); + SASSERT(!m_count_cache[depth]->contains(e)); m.inc_ref(e); m_count_cache[depth]->insert(e, std::make_pair(min, max)); TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); @@ -359,11 +363,13 @@ struct bv_trailing::imp { return true; } - void reset_cache(unsigned condition) { + void reset_cache(const unsigned condition) { SASSERT(m_count_cache[0] == NULL); for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) { if (m_count_cache[i] == NULL) continue; - if (m_count_cache[i]->size() < condition) continue; + TRACE("bv-trailing", tout << "may reset cache " << i << " " << condition << "\n";); + if (condition && m_count_cache[i]->size() < condition) continue; + TRACE("bv-trailing", tout << "reset cache " << i << "\n";); map::iterator it = m_count_cache[i]->begin(); map::iterator end = m_count_cache[i]->end(); for (; it != end; ++it) m.dec_ref(it->m_key); diff --git a/src/ast/rewriter/rewriter_params.pyg b/src/ast/rewriter/rewriter_params.pyg index 3a8ed5d5e..5bd17f556 100644 --- a/src/ast/rewriter/rewriter_params.pyg +++ b/src/ast/rewriter/rewriter_params.pyg @@ -7,5 +7,6 @@ def_module_params('rewriter', ("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."), ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."), ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."), + ("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."), ("cache_all", BOOL, False, "cache all intermediate results."))) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index ff6a10274..0c57ea609 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -189,6 +189,14 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (st != BR_FAILED) return st; } + if (k == OP_ITE) { + SASSERT(num == 3); + family_id s_fid = m().get_sort(args[1])->get_family_id(); + if (s_fid == m_bv_rw.get_fid()) + st = m_bv_rw.mk_ite_core(args[0], args[1], args[2], result); + if (st != BR_FAILED) + return st; + } return m_b_rw.mk_app_core(f, num, args, result); } if (fid == m_a_rw.get_fid()) diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp new file mode 100644 index 000000000..c3f32aaaf --- /dev/null +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -0,0 +1,245 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + bv_bound_chk_tactic.cpp + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: +--*/ +#include"bv_bound_chk_tactic.h" +#include"ast.h" +#include"rewriter.h" +#include"rewriter_def.h" +#include"bv_bounds.h" +#include"rewriter_params.hpp" +#include"bool_rewriter.h" +#include"cooperate.h" + +struct bv_bound_chk_stats { + unsigned m_unsats; + unsigned m_singletons; + unsigned m_reduces; + bv_bound_chk_stats() : m_unsats(0), m_singletons(0), m_reduces(0) {}; +}; + +struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg { + ast_manager & m_m; + unsigned m_bv_ineq_consistency_test_max; + bool_rewriter m_b_rw; + unsigned long long m_max_steps; + unsigned long long m_max_memory; // in bytes + bv_bound_chk_stats& m_stats; + + + bv_bound_chk_rewriter_cfg(ast_manager & m, bv_bound_chk_stats& stats) + : m_m(m), m_b_rw(m), m_stats(stats) {} + + ~bv_bound_chk_rewriter_cfg() {} + + void updt_params(params_ref const & _p) { + rewriter_params p(_p); + m_bv_ineq_consistency_test_max = p.bv_ineq_consistency_test_max(); + m_max_memory = p.max_memory(); + m_max_steps = p.max_steps(); + + } + + ast_manager & m() const { return m_m; } + + bool rewrite_patterns() const { return false; } + + bool flat_assoc(func_decl * f) const { return true; } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + const br_status st = reduce_app_core(f, num, args, result, result_pr); + CTRACE("bv_bound_chk_step", st != BR_FAILED, + tout << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; + tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";); + return st; + } + + br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result_pr = 0; + const family_id fid = f->get_family_id(); + if (fid != m_b_rw.get_fid()) return BR_FAILED; + const decl_kind k = f->get_decl_kind(); + bv_bounds bvb(m()); + const br_status rv = bvb.rewrite(m_bv_ineq_consistency_test_max, f, num, args, result); + if (rv != BR_FAILED && (m_m.is_false(result) || m_m.is_true(result))) m_stats.m_unsats++; + else if (rv != BR_FAILED && bvb.singletons().size()) m_stats.m_singletons++; + else if (rv != BR_FAILED && is_app(result) && to_app(result)->get_num_args() < num) m_stats.m_reduces++; + return rv; + } + + bool max_steps_exceeded(unsigned long long num_steps) const { + cooperate("bv-bound-chk"); + if (num_steps > m_max_steps) + return true; + if (memory::get_allocation_size() > m_max_memory) + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + return false; + } + + void reset_statistics() { + m_stats.m_unsats = 0; + m_stats.m_singletons = 0; + m_stats.m_reduces = 0; + } + + void collect_statistics(statistics & st) const { + st.update("unsat bv bounds", m_stats.m_unsats); + st.update("bv singletons", m_stats.m_singletons); + st.update("bv reduces", m_stats.m_reduces); + } +}; + +struct bv_bound_chk_rewriter : public rewriter_tpl { + bv_bound_chk_rewriter_cfg m_cfg; + + bv_bound_chk_rewriter(ast_manager & m, params_ref const & p, bv_bound_chk_stats& stats) + : rewriter_tpl(m, false, m_cfg) + , m_cfg(m, stats) + { + updt_params(p); + } + + virtual ~bv_bound_chk_rewriter() {} + + void updt_params(params_ref const & _p) { + m_cfg.updt_params(_p); + } + + void collect_statistics(statistics & st) const { + m_cfg.collect_statistics(st); + } + + + void reset_statistics() { + m_cfg.reset_statistics(); + } + +}; + +class bv_bound_chk_tactic : public tactic { + class imp; + imp * m_imp; + params_ref m_params; + bv_bound_chk_stats m_stats; +public: + bv_bound_chk_tactic(ast_manager & m, params_ref const & p); + virtual ~bv_bound_chk_tactic(); + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core); + virtual tactic * translate(ast_manager & m); + virtual void updt_params(params_ref const & p); + void cleanup(); + void collect_statistics(statistics & st) const; + void reset_statistics(); +}; + +class bv_bound_chk_tactic::imp { + bv_bound_chk_rewriter m_rw; +public: + imp(ast_manager & m, params_ref const & p, bv_bound_chk_stats& stats) + : m_rw(m, p, stats) { } + + virtual ~imp() { } + + ast_manager& m() { return m_rw.m(); } + + void operator()(goal_ref const & g) { + SASSERT(g->is_well_sorted()); + tactic_report report("bv-bound-chk", *g); + ast_manager& m(g->m()); + expr_ref new_curr(m); + const unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + if (g->inconsistent()) break; + expr * curr = g->form(idx); + m_rw(curr, new_curr); + g->update(idx, new_curr); + } + m_rw.m_cfg.cleanup(); + } + + virtual void updt_params(params_ref const & p) { + m_rw.updt_params(p); + } + + void collect_statistics(statistics & st) const { + m_rw.collect_statistics(st); + } + + void reset_statistics() { + m_rw.reset_statistics(); + } +}; + +bv_bound_chk_tactic::bv_bound_chk_tactic(ast_manager & m, params_ref const & p) +: m_params(p) +{ + m_imp = alloc(imp, m, p, m_stats); +} + + +bv_bound_chk_tactic::~bv_bound_chk_tactic() { + dealloc(m_imp); +} + +void bv_bound_chk_tactic::operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + fail_if_proof_generation("bv-bound-chk", g); + fail_if_unsat_core_generation("bv-bound-chk", g); + TRACE("bv-bound-chk", g->display(tout << "before:"); tout << std::endl;); + mc = 0; pc = 0; core = 0; result.reset(); + m_imp->operator()(g); + g->inc_depth(); + result.push_back(g.get()); + TRACE("bv-bound-chk", g->display(tout << "after:");); + SASSERT(g->is_well_sorted()); +} + +tactic * bv_bound_chk_tactic::translate(ast_manager & m) { + return alloc(bv_bound_chk_tactic, m, m_params); +} + + +void bv_bound_chk_tactic::updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); +} + +void bv_bound_chk_tactic::cleanup() { + imp * d = alloc(imp, m_imp->m(), m_params, m_stats); + std::swap(d, m_imp); + dealloc(d); +} + +void bv_bound_chk_tactic::collect_statistics(statistics & st) const { + m_imp->collect_statistics(st); +} + +void bv_bound_chk_tactic::reset_statistics() { + m_imp->reset_statistics(); +} + + +tactic* mk_bv_bound_chk_tactic(ast_manager & m, params_ref const & p) { + return alloc(bv_bound_chk_tactic, m, p); +} diff --git a/src/tactic/bv/bv_bound_chk_tactic.h b/src/tactic/bv/bv_bound_chk_tactic.h new file mode 100644 index 000000000..f134d42ab --- /dev/null +++ b/src/tactic/bv/bv_bound_chk_tactic.h @@ -0,0 +1,30 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + bv_bound_chk_tactic.h + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: + --*/ +#ifndef BV_BOUND_CHK_TACTIC_H_ +#define BV_BOUND_CHK_TACTIC_H_ + +#include"tactical.h" +#include"params.h" +#include"ast.h" + +tactic* mk_bv_bound_chk_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("bv_bound_chk", "attempts to detect inconsistencies of bounds on bv expressions.", "mk_bv_bound_chk_tactic(m, p)") +*/ + +#endif /* BV_BOUND_CHK_TACTIC_H_*/ diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 3ee97308a..e0e1a60e4 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -39,6 +39,7 @@ Notes: #include"qfaufbv_tactic.h" #include"qfbv_tactic.h" #include"tactic2solver.h" +#include"bv_bound_chk_tactic.h" /////////////// class qfufbv_ackr_tactic : public tactic { @@ -149,6 +150,7 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { return and_then( mk_simplify_tactic(m), mk_propagate_values_tactic(m), + if_no_proofs(if_no_unsat_cores(mk_bv_bound_chk_tactic(m))), //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p), mk_solve_eqs_tactic(m), mk_elim_uncnstr_tactic(m),