mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix encoding bugs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-14 19:30:21 -08:00
parent 54ee098cfd
commit ce1acd8c41
1 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/sat/smt/intblast_solver.cpp
View file

@ -468,6 +468,7 @@ namespace intblast {
sorts.push_back(a.mk_int()); sorts.push_back(a.mk_int());
} }
else else
sorts.push_back(s); sorts.push_back(s);
} }
b = translated(b); b = translated(b);
@ -701,17 +702,17 @@ namespace intblast {
// //
// ashr(x, y) // ashr(x, y)
// if y = k & x >= 0 -> x / 2^k // if y = k & x >= 0 -> x / 2^k
// if y = k & x < 0 -> - (x / 2^k) // if y = k & x < 0 -> (x / 2^k) - 1 + 2^{N-k}
// //
rational N = rational::power_of_two(bv.get_bv_size(e)); unsigned sz = bv.get_bv_size(e);
expr* x = umod(e, 0); rational N = bv_size(e);
expr* y = umod(e, 1); expr* x = umod(e, 0), *y = umod(e, 1);
expr* signbit = a.mk_ge(x, a.mk_int(N / 2)); expr* signx = a.mk_ge(x, a.mk_int(N / 2));
r = m.mk_ite(signbit, a.mk_int(N - 1), a.mk_int(0)); r = m.mk_ite(signx, a.mk_int(N - 1), a.mk_int(0));
for (unsigned i = 0; i < bv.get_bv_size(e); ++i) { for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
m.mk_ite(signbit, a.mk_uminus(d), d), m.mk_ite(signx, a.mk_add(d, a.mk_int(N - rational::power_of_two(sz-i))), d),
r); r);
} }
break; break;
@ -793,12 +794,13 @@ namespace intblast {
case OP_BSREM: { case OP_BSREM: {
// y = 0 -> x // y = 0 -> x
// else x - sdiv(x, y) * y // else x - sdiv(x, y) * y
bv_expr = e; expr* x = umod(e, 0), * y = umod(e, 1);
expr* x = umod(bv_expr, 0), * y = umod(bv_expr, 1); rational N = bv_size(e);
rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
expr* signx = a.mk_ge(x, a.mk_int(N / 2)); expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2)); expr* signy = a.mk_ge(y, a.mk_int(N / 2));
expr* d = a.mk_idiv(x, y); expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(absx, absy);
d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = a.mk_sub(x, a.mk_mul(d, y)); r = a.mk_sub(x, a.mk_mul(d, y));
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);