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

add deterministic behavior

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-29 12:24:03 -07:00
parent 7dae39c24b
commit a1918c4630
4 changed files with 61 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

76
src/ast/rewriter/bv2int_translator.cpp
View file

@ -221,9 +221,11 @@ void bv2int_translator::translate_bv(app* e) {
auto N = bv_size(e);
auto A = rational::power_of_two(sz - n);
auto B = rational::power_of_two(n);
auto hi = mul(r, a.mk_int(A));
// TODO: non-deterministic parameter evaluation
auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A);
expr_ref hi(m);
expr_ref div(m);
hi = mul(r, a.mk_int(A));
div = a.mk_idiv(umod(e, 0), a.mk_int(B));
expr* lo = amod(e, div, A);
r = add(hi, lo);
}
return r;
@ -365,8 +367,8 @@ void bv2int_translator::translate_bv(app* e) {
rational N = bv_size(e);
expr* x = umod(e, 0), * y = umod(e, 1);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
// TODO: non-deterministic parameter evaluation
r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0));
expr* min_uno = a.mk_int(-1);
expr* r = m.mk_ite(signx, min_uno, a.mk_int(0));
IF_VERBOSE(4, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
@ -431,12 +433,14 @@ void bv2int_translator::translate_bv(app* e) {
ctx.push(push_back_vector(m_bv2int));
r = umod(e->get_arg(0), 0);
break;
case OP_BCOMP:
case OP_BCOMP: {
bv_expr = e->get_arg(0);
// TODO: non-deterministic parameter evaluation
// TODO: non-deterministic parameter evaluation
r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
expr* lhs = umod(bv_expr, 0);
expr* rhs = umod(bv_expr, 1);
expr* eq = m.mk_eq(lhs, rhs);
r = m.mk_ite(eq, a.mk_int(1), a.mk_int(0));
break;
}
case OP_BSMOD_I:
case OP_BSMOD: {
expr* x = umod(e, 0), * y = umod(e, 1);
@ -451,10 +455,14 @@ void bv2int_translator::translate_bv(app* e) {
// x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u
r = a.mk_uminus(u);
r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
// TODO: non-deterministic parameter evaluation
r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
expr* pos_neg = m.mk_and(m.mk_not(signx), signy);
expr* neg_pos = m.mk_and(signx, m.mk_not(signy));
expr* pos_pos = m.mk_and(m.mk_not(signx), m.mk_not(signy));
expr_ref add_u_y(m);
add_u_y = add(u, y);
r = m.mk_ite(pos_neg, add_u_y, r);
r = m.mk_ite(neg_pos, a.mk_sub(y, u), r);
r = m.mk_ite(pos_pos, u, r);
r = if_eq(u, 0, a.mk_int(0), r);
r = if_eq(y, 0, x, r);
break;
@ -477,8 +485,8 @@ void bv2int_translator::translate_bv(app* e) {
y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(x, y);
r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
// TODO: non-deterministic parameter evaluation
r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
expr* zero_case = m.mk_ite(signx, a.mk_int(1), a.mk_int(-1));
r = if_eq(y, 0, zero_case, r);
break;
}
case OP_BSREM_I:
@ -572,22 +580,24 @@ void bv2int_translator::translate_basic(app* e) {
rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) ||
is_bounded(arg(0), N) || is_bounded(arg(1), N)) {
// TODO: non-deterministic parameter evaluation
set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
expr* lhs = umod(bv_expr, 0);
expr* rhs = umod(bv_expr, 1);
expr* eq = m.mk_eq(lhs, rhs);
set_translated(e, eq);
}
else {
// TODO: non-deterministic parameter evaluation
m_args[0] = a.mk_sub(arg(0), arg(1));
// TODO: non-deterministic parameter evaluation
set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
expr* diff = a.mk_sub(arg(0), arg(1));
m_args[0] = diff;
expr* lhs = umod(bv_expr, 0);
expr* rhs = a.mk_int(0);
expr* eq = m.mk_eq(lhs, rhs);
set_translated(e, eq);
}
}
else
// TODO: non-deterministic parameter evaluation
set_translated(e, m.mk_eq(arg(0), arg(1)));
}
else if (m.is_ite(e))
// TODO: non-deterministic parameter evaluation
set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
else if (m_is_plugin)
set_translated(e, e);
@ -671,9 +681,11 @@ expr_ref bv2int_translator::add(expr* x, expr* y) {
expr* bv2int_translator::amod(expr* bv_expr, expr* x, rational const& N) {
rational v;
expr* r = nullptr, * c = nullptr, * t = nullptr, * e = nullptr;
if (m.is_ite(x, c, t, e))
// TODO: non-deterministic parameter evaluation
r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
if (m.is_ite(x, c, t, e)) {
expr* t_val = amod(bv_expr, t, N);
expr* e_val = amod(bv_expr, e, N);
r = m.mk_ite(c, t_val, e_val);
}
else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
r = x;
else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
@ -693,11 +705,13 @@ void bv2int_translator::translate_eq(expr* e) {
SASSERT(bv.is_bv(x));
if (!is_translated(e)) {
ensure_translated(x);
ensure_translated(y);
m_args.reset();
m_args.push_back(a.mk_sub(translated(x), translated(y)));
// TODO: non-deterministic parameter evaluation
set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
ensure_translated(y);
m_args.reset();
m_args.push_back(a.mk_sub(translated(x), translated(y)));
expr* lhs = umod(x, 0);
expr* rhs = a.mk_int(0);
expr* eq = m.mk_eq(lhs, rhs);
set_translated(e, eq);
}
m_preds.push_back(e);
TRACE(bv, tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n");

8
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -74,9 +74,11 @@ struct enum2bv_rewriter::imp {
if (is_unate(s)) {
expr_ref one(m_bv.mk_numeral(rational::one(), 1), m);
for (unsigned i = 0; i + 2 < domain_size; ++i) {
// TODO: non-deterministic parameter evaluation
bounds.push_back(m.mk_implies(m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x)),
m.mk_eq(one, m_bv.mk_extract(i, i, x))));
expr* hi_bit = m_bv.mk_extract(i + 1, i + 1, x);
expr* lo_bit = m_bv.mk_extract(i, i, x);
expr* eq_hi = m.mk_eq(one, hi_bit);
expr* eq_lo = m.mk_eq(one, lo_bit);
bounds.push_back(m.mk_implies(eq_hi, eq_lo));
}
}
else {

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

@ -494,8 +494,10 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
}
if (m_util.is_ninf(arg1)) {
// -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN)
// TODO: non-deterministic parameter evaluation
result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2));
expr* eq_neg_inf = m().mk_eq(arg2, arg1);
expr* neq = m().mk_not(eq_neg_inf);
expr* not_nan = mk_neq_nan(arg2);
result = m().mk_and(neq, not_nan);
return BR_REWRITE3;
}
if (m_util.is_ninf(arg2)) {
@ -510,8 +512,10 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
}
if (m_util.is_pinf(arg2)) {
// arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN)
// TODO: non-deterministic parameter evaluation
result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1));
expr* eq_pos_inf = m().mk_eq(arg1, arg2);
expr* neq = m().mk_not(eq_pos_inf);
expr* not_nan = mk_neq_nan(arg1);
result = m().mk_and(neq, not_nan);
return BR_REWRITE3;
}

5
src/muz/rel/check_relation.cpp
View file

@ -533,8 +533,9 @@ namespace datalog {
unsigned c1 = m_cols[0];
for (unsigned i = 1; i < m_cols.size(); ++i) {
unsigned c2 = m_cols[i];
// TODO: non-deterministic parameter evaluation
conds.push_back(m.mk_eq(m.mk_var(c1, sig[c1]), m.mk_var(c2, sig[c2])));
expr* v1 = m.mk_var(c1, sig[c1]);
expr* v2 = m.mk_var(c2, sig[c2]);
conds.push_back(m.mk_eq(v1, v2));
}
cond = mk_and(m, conds.size(), conds.data());
r.consistent_formula();