mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

add (disabled) experiment to use quot-rem instead of division circuit

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-13 15:20:43 +02:00
parent 8a30128933
commit 2449ba93c5
2 changed files with 50 additions and 0 deletions

47
src/smt/theory_bv.cpp
View file

@ -885,6 +885,7 @@ namespace smt {
find_wpos(v);
}
bool theory_bv::internalize_term_core(app * term) {
SASSERT(term->get_family_id() == get_family_id());
TRACE("bv", tout << "internalizing term: " << mk_bounded_pp(term, m) << "\n";);
@ -898,6 +899,7 @@ namespace smt {
case OP_BMUL: internalize_mul(term); return true;
case OP_BSDIV_I: internalize_sdiv(term); return true;
case OP_BUDIV_I: internalize_udiv(term); return true;
// case OP_BUDIV_I: internalize_udiv_quot_rem(term); return true;
case OP_BSREM_I: internalize_srem(term); return true;
case OP_BUREM_I: internalize_urem(term); return true;
case OP_BSMOD_I: internalize_smod(term); return true;
@ -1392,6 +1394,13 @@ namespace smt {
ctx.mark_as_relevant(n->get_arg(0));
assert_int2bv_axiom(n);
}
#if 0
else if (m_util.is_bv_udivi(n)) {
ctx.mark_as_relevant(n->get_arg(0));
ctx.mark_as_relevant(n->get_arg(1));
assert_udiv_quot_rem_axiom(n);
}
#endif
else if (ctx.e_internalized(n)) {
enode * e = ctx.get_enode(n);
theory_var v = e->get_th_var(get_id());
@ -1985,5 +1994,43 @@ namespace smt {
return true;
}
#if 0
void theory_bv::internalize_udiv_quot_rem(app* n) {
process_args(n);
mk_enode(n);
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v);
if (!ctx.relevancy())
assert_udiv_quot_rem_axiom(n);
}
void theory_bv::assert_udiv_quot_rem_axiom(app * q) {
// Axioms for quotient/remainder:
// a = b*q + r
// no-mul-overflow(b,q)
// no-add-overflow(bq, r)
// b != 0 => r < b
// b = 0 => q = -1
expr* a, *b;
VERIFY(m_util.is_bv_udivi(q, a, b));
sort* srt = q->get_sort();
func_decl_ref rf(m.mk_func_decl(symbol("rem"), srt, srt, srt), m);
expr_ref r(m.mk_app(rf, a, b), m);
expr_ref bq(m_util.mk_bv_mul(b, q), m);
expr_ref bqr(m_util.mk_bv_add(bq, r), m);
literal eq = mk_literal(m.mk_eq(a, bqr));
literal obq = mk_literal(m_util.mk_bvumul_no_ovfl(b, q));
literal obqr = mk_literal(m_util.mk_ule(r, bqr));
literal b0 = mk_literal(m.mk_eq(b, m_util.mk_numeral(rational::zero(), srt)));
ctx.mk_th_axiom(get_id(), 1, &eq);
ctx.mk_th_axiom(get_id(), 1, &obq);
ctx.mk_th_axiom(get_id(), 1, &obqr);
ctx.mk_th_axiom(get_id(), b0, ~mk_literal(m_util.mk_ule(b, r)));
ctx.mk_th_axiom(get_id(), ~b0, mk_literal(m.mk_eq(q, m_util.mk_numeral(rational(-1), srt))));
}
#endif
};

3
src/smt/theory_bv.h
View file

@ -188,6 +188,7 @@ namespace smt {
void internalize_urem(app * n);
void internalize_srem(app * n);
void internalize_smod(app * n);
void internalize_udiv_quot_rem(app* n);
void internalize_shl(app * n);
void internalize_lshr(app * n);
void internalize_ashr(app * n);
@ -227,6 +228,8 @@ namespace smt {
void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
void assert_int2bv_axiom(app* n);
void assert_bv2int_axiom(app* n);
void assert_udiv_quot_rem_axiom(app * n);
protected:
theory_var mk_var(enode * n) override;