mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
some simplifications based on #4178
This commit is contained in:
parent
269522127b
commit
f0d33ddddb
|
@ -36,6 +36,7 @@ static void sort_args(expr * & l1, expr * & l2, expr * & l3) {
|
|||
l1 = args[0]; l2 = args[1]; l3 = args[2];
|
||||
}
|
||||
|
||||
|
||||
void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) {
|
||||
TRACE("xor3", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id(););
|
||||
sort_args(l1, l2, l3);
|
||||
|
|
|
@ -44,6 +44,7 @@ public:
|
|||
void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); }
|
||||
void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); }
|
||||
void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); }
|
||||
void mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) { m_rw.mk_ge2(a, b, c, r); }
|
||||
void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); }
|
||||
void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); }
|
||||
void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); }
|
||||
|
|
|
@ -64,6 +64,7 @@ struct blaster_cfg {
|
|||
void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rewriter.mk_ite(c, t, e, r); }
|
||||
void mk_nand(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nand(a, b, r); }
|
||||
void mk_nor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nor(a, b, r); }
|
||||
void mk_ge2(expr * a, expr * b, expr * c, expr_ref& r) { m_rewriter.mk_ge2(a, b, c, r); }
|
||||
};
|
||||
|
||||
class blaster : public bit_blaster_tpl<blaster_cfg> {
|
||||
|
|
|
@ -70,6 +70,7 @@ public:
|
|||
void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { Cfg::mk_ite(c, t, e, r); }
|
||||
void mk_nand(expr * a, expr * b, expr_ref & r) { Cfg::mk_nand(a, b, r); }
|
||||
void mk_nor(expr * a, expr * b, expr_ref & r) { Cfg::mk_nor(a, b, r); }
|
||||
void mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) { Cfg::mk_ge2(a, b, c, r); }
|
||||
//
|
||||
|
||||
|
||||
|
|
|
@ -1101,23 +1101,17 @@ template<typename Cfg>
|
|||
template<bool Signed>
|
||||
void bit_blaster_tpl<Cfg>::mk_le(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) {
|
||||
SASSERT(sz > 0);
|
||||
expr_ref i1(m()), i2(m()), i3(m()), not_a(m());
|
||||
expr_ref not_a(m());
|
||||
mk_not(a_bits[0], not_a);
|
||||
mk_or(not_a, b_bits[0], out);
|
||||
for (unsigned idx = 1; idx < (Signed ? sz - 1 : sz); idx++) {
|
||||
mk_not(a_bits[idx], not_a);
|
||||
mk_and(not_a, b_bits[idx], i1);
|
||||
mk_and(not_a, out, i2);
|
||||
mk_and(b_bits[idx], out, i3);
|
||||
mk_or(i1, i2, i3, out);
|
||||
mk_ge2(not_a, b_bits[idx], out, out);
|
||||
}
|
||||
if (Signed) {
|
||||
expr_ref not_b(m());
|
||||
mk_not(b_bits[sz-1], not_b);
|
||||
mk_and(not_b, a_bits[sz-1], i1);
|
||||
mk_and(not_b, out, i2);
|
||||
mk_and(a_bits[sz-1], out, i3);
|
||||
mk_or(i1, i2, i3, out);
|
||||
mk_ge2(not_b, a_bits[sz-1], out, out);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -1031,4 +1031,22 @@ void bool_rewriter::mk_nor(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
mk_not(tmp, result);
|
||||
}
|
||||
|
||||
|
||||
void bool_rewriter::mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) {
|
||||
if (m().is_false(a)) mk_and(b, c, r);
|
||||
else if (m().is_false(b)) mk_and(a, c, r);
|
||||
else if (m().is_false(c)) mk_and(a, b, r);
|
||||
else if (m().is_true(a)) mk_or(b, c, r);
|
||||
else if (m().is_true(b)) mk_or(a, c, r);
|
||||
else if (m().is_true(c)) mk_or(a, b, r);
|
||||
else {
|
||||
expr_ref i1(m()), i2(m()), i3(m());
|
||||
mk_and(a, b, i1);
|
||||
mk_and(a, c, i2);
|
||||
mk_and(b, c, i3);
|
||||
mk_or(i1, i2, i3, r);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
template class rewriter_tpl<bool_rewriter_cfg>;
|
||||
|
|
|
@ -215,6 +215,7 @@ public:
|
|||
void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);
|
||||
void mk_nand(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_nor(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_ge2(expr* a, expr* b, expr* c, expr_ref& result);
|
||||
};
|
||||
|
||||
struct bool_rewriter_cfg : public default_rewriter_cfg {
|
||||
|
|
|
@ -510,6 +510,12 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
// (bvule c (+ c a)) -> (bvule a (2^n - c)) (could be generalized)
|
||||
if (!is_signed && is_num1 && m_util.is_bv_add(b, a1, a2) && is_numeral(a1, r2, sz) && r1 == r2) {
|
||||
result = m_util.mk_ule(a2, m_util.mk_numeral(-r1, sz));
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
if (m_le_extra) {
|
||||
const br_status cst = rw_leq_concats(is_signed, a, b, result);
|
||||
if (cst != BR_FAILED) {
|
||||
|
|
Loading…
Reference in a new issue