mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

fix quot-rem axioms: cannot be rewritten because it looses information

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 19:28:53 -08:00
parent 211aff4cba
commit 33c43a474d
1 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/sat/smt/polysat_internalize.cpp
View file

@ -528,8 +528,6 @@ namespace polysat {
return; return;
} }
pdd r = var2pdd(rn->get_th_var(get_id()));
pdd q = var2pdd(qn->get_th_var(get_id()));
// Axioms for quotient/remainder // Axioms for quotient/remainder
// //
@ -540,18 +538,19 @@ namespace polysat {
// b = 0 ==> q = -1 // b = 0 ==> q = -1
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it. // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
// Maybe we need something like an op_constraint for better propagation. // Maybe we need something like an op_constraint for better propagation.
add_axiom("quot-rem", { m_core.eq(b * q + r - a) }, false);
add_axiom("quot-rem", { ~m_core.umul_ovfl(b, q) }, false); add_axiom("quot-rem", { eq_internalize(bv.mk_bv_add(bv.mk_bv_mul(y, quot), rem), x)}, false);
add_axiom("quot-rem", { mk_literal(bv.mk_bvumul_no_ovfl(quot, y)) }, false);
// r <= b*q+r // r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 } // { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1 // b*q <= -r-1
add_axiom("quot-rem", { m_core.ule(b * q, -r - 1) }, false); auto minus_one = bv.mk_numeral(rational::power_of_two(sz) - 1, sz);
auto one = bv.mk_numeral(1, sz);
auto c_eq = m_core.eq(b); auto zero = bv.mk_numeral(0, sz);
if (!c_eq.is_always_true()) add_axiom("quot-rem", { mk_literal(bv.mk_ule(bv.mk_bv_mul(y, quot), bv.mk_bv_sub(minus_one, rem))) }, false);
add_axiom("quot-rem", { c_eq, ~m_core.ule(b, r) }, false); auto c_eq = eq_internalize(y, zero);
if (!c_eq.is_always_false()) add_axiom("quot-rem", { c_eq, ~mk_literal(bv.mk_ule(y, rem)) }, false);
add_axiom("quot-rem", { ~c_eq, m_core.eq(q + 1) }, false); add_axiom("quot-rem", { ~c_eq, eq_internalize(bv.mk_bv_add(quot, one), zero) }, false);
} }
void solver::internalize_sign_extend(app* e) { void solver::internalize_sign_extend(app* e) {