mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fixup bv operators

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-03 07:56:42 -08:00
parent 919ac515bc
commit 88269edd4b
3 changed files with 43 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/arith_decl_plugin.cpp
View file

@ -636,6 +636,10 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("/0",OP_DIV0));
op_names.push_back(builtin_name("div0",OP_IDIV0));
op_names.push_back(builtin_name("mod0",OP_MOD0));
op_names.push_back(builtin_name(bv_symbol(OP_ARITH_BAND).bare_str(), OP_ARITH_BAND));
op_names.push_back(builtin_name(bv_symbol(OP_ARITH_SHL).bare_str(), OP_ARITH_SHL));
op_names.push_back(builtin_name(bv_symbol(OP_ARITH_LSHR).bare_str(), OP_ARITH_LSHR));
op_names.push_back(builtin_name(bv_symbol(OP_ARITH_ASHR).bare_str(), OP_ARITH_ASHR));
}
}
@ -643,7 +647,7 @@ bool arith_decl_plugin::is_value(app * e) const {
return
is_app_of(e, m_family_id, OP_NUM) ||
is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) ||
is_app_of(e, m_family_id, OP_PI) ||
is_app_of(e, m_family_id, OP_PI) ||
is_app_of(e, m_family_id, OP_E);
}

12
src/ast/rewriter/arith_rewriter.cpp
View file

@ -1600,8 +1600,13 @@ br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr
N = rational::power_of_two(sz);
if (is_num_x)
x = mod(x, N);
if (is_num_y && y >= sz) {
result = m_util.mk_int(0);
return BR_DONE;
}
if (is_num_y)
y = mod(y, N);
if (is_num_x && x == 0) {
result = m_util.mk_int(0);
return BR_DONE;
@ -1619,6 +1624,13 @@ br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr
}
return BR_DONE;
}
if (is_num_y) {
result = m_util.mk_mod(arg1, m_util.mk_int(N));
//result = arg1; // unsound
result = m_util.mk_idiv(result, m_util.mk_int(rational::power_of_two(y.get_unsigned())));
return BR_DONE;
}
return BR_FAILED;
}

35
src/smt/theory_lra.cpp
View file

@ -2522,11 +2522,15 @@ public:
found_unsupported(n);
return true;
}
rational N = rational::power_of_two(sz);
rational N = rational::power_of_two(sz), r;
valx = mod(valx, N);
valy = mod(valy, N);
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
if (a.is_numeral(_x, r))
x = a.mk_int(mod(r, N));
if (a.is_numeral(_y, r))
y = a.mk_int(mod(r, N));
SASSERT(0 <= valn && valn < N);
// x mod 2^{i + 1} >= 2^i means the i'th bit is 1.
@ -2559,9 +2563,12 @@ public:
return true;
unsigned k = valy.get_unsigned();
sat::literal eq = th.mk_eq(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)), false);
ctx().mark_as_relevant(eq);
if (ctx().get_assignment(eq) == l_true)
return true;
ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq);
sat::literal y_eq_k = th.mk_eq(y, a.mk_int(k), false);
ctx().mark_as_relevant(y_eq_k);
ctx().mk_th_axiom(get_id(), ~y_eq_k, eq);
IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n");
return false;
}
@ -2571,10 +2578,12 @@ public:
return true;
unsigned k = valy.get_unsigned();
sat::literal eq = th.mk_eq(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))), false);
ctx().mark_as_relevant(eq);
if (ctx().get_assignment(eq) == l_true)
return true;
ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq);
IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n");
sat::literal y_eq_k = th.mk_eq(y, a.mk_int(k), false);
ctx().mark_as_relevant(y_eq_k);
ctx().mk_th_axiom(get_id(), ~y_eq_k, eq);
return false;
}
if (a.is_ashr(n)) {
@ -2590,6 +2599,7 @@ public:
// x < 0 & y = k -> n = (x div 2^k - 2^{N-k}) mod 2^N
xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
eq = th.mk_eq(n, a.mk_mod(a.mk_add(xdiv2k, a.mk_int(-rational::power_of_two(sz - k))), a.mk_int(N)), false);
ctx().mark_as_relevant(eq);
if (ctx().get_assignment(eq) == l_true)
return true;
break;
@ -2597,6 +2607,7 @@ public:
// x >= 0 & y = k -> n = x div 2^k
xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
eq = th.mk_eq(n, xdiv2k, false);
ctx().mark_as_relevant(eq);
if (ctx().get_assignment(eq) == l_true)
return true;
break;
@ -2604,7 +2615,9 @@ public:
ctx().mark_as_relevant(signx);
return false;
}
ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), ~signx, eq);
sat::literal y_eq_k = th.mk_eq(y, a.mk_int(k), false);
ctx().mark_as_relevant(y_eq_k);
ctx().mk_th_axiom(get_id(), ~y_eq_k, ~signx, eq);
return false;
}
return true;
@ -2622,9 +2635,13 @@ public:
unsigned sz = 0;
expr* _x = nullptr, * _y = nullptr;
VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
rational N = rational::power_of_two(sz);
rational N = rational::power_of_two(sz), r;
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
if (a.is_numeral(_x, r))
x = a.mk_int(mod(r, N));
if (a.is_numeral(_y, r))
y = a.mk_int(mod(r, N));
// 0 <= n < 2^sz
@ -2657,9 +2674,9 @@ public:
// y >= sz & x >= 2^{sz-1} => n = -1
// y = 0 => n = x
auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0))));
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1))));
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0))));
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1))));
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
}
else
UNREACHABLE();