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

fix param evaluation non-determinism

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-30 07:32:50 -07:00
parent a413783c1c
commit 77962ff3bb
4 changed files with 50 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast.cpp
View file

@ -2130,12 +2130,16 @@ expr* ast_manager::coerce_to(expr* e, sort* s) {
} }
if (s != se && s->get_family_id() == arith_family_id && is_bool(e)) { if (s != se && s->get_family_id() == arith_family_id && is_bool(e)) {
arith_util au(*this); arith_util au(*this);
if (s->get_decl_kind() == REAL_SORT) if (s->get_decl_kind() == REAL_SORT) {
// TODO: non-deterministic parameter evaluation expr_ref one(au.mk_real(1), *this);
return mk_ite(e, au.mk_real(1), au.mk_real(0)); expr_ref zero(au.mk_real(0), *this);
else return mk_ite(e, one.get(), zero.get());
// TODO: non-deterministic parameter evaluation }
return mk_ite(e, au.mk_int(1), au.mk_int(0)); else {
expr_ref one(au.mk_int(1), *this);
expr_ref zero(au.mk_int(0), *this);
return mk_ite(e, one.get(), zero.get());
}
} }
else { else {
return e; return e;

54
src/ast/ast_smt2_pp.cpp
View file

@ -592,21 +592,22 @@ class smt2_printer {
} }
format * pp_attribute(char const * attr, format * f) { format * pp_attribute(char const * attr, format * f) {
// TODO: non-deterministic parameter evaluation format * attr_fmt = mk_string(m(), attr);
return mk_compose(m(), format * indented = mk_indent(m(), static_cast<unsigned>(strlen(attr)), f);
mk_string(m(), attr), return mk_compose(m(), attr_fmt, indented);
mk_indent(m(), static_cast<unsigned>(strlen(attr)), f));
} }
format * pp_simple_attribute(char const * attr, int v) { format * pp_simple_attribute(char const * attr, int v) {
// TODO: non-deterministic parameter evaluation format * attr_fmt = mk_string(m(), attr);
return mk_compose(m(), mk_string(m(), attr), mk_int(m(), v)); format * int_fmt = mk_int(m(), v);
return mk_compose(m(), attr_fmt, int_fmt);
} }
format * pp_simple_attribute(char const * attr, symbol const & s) { format * pp_simple_attribute(char const * attr, symbol const & s) {
std::string str = ensure_quote(s); std::string str = ensure_quote(s);
// TODO: non-deterministic parameter evaluation format * attr_fmt = mk_string(m(), attr);
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str)); format * sym_fmt = mk_string(m(), str);
return mk_compose(m(), attr_fmt, sym_fmt);
} }
format * pp_labels(bool is_pos, buffer<symbol> const & names, format * f) { format * pp_labels(bool is_pos, buffer<symbol> const & names, format * f) {
@ -765,26 +766,31 @@ class smt2_printer {
SASSERT(it < end); SASSERT(it < end);
format * fname = m_env.pp_fdecl(t->get_decl(), len); format * fname = m_env.pp_fdecl(t->get_decl(), len);
if (len > MAX_INDENT) { if (len > MAX_INDENT) {
// TODO: non-deterministic parameter evaluation format * open_paren = mk_string(m(), "(");
f = mk_group(m(), mk_compose(m(), format * head = mk_compose(m(), open_paren, fname);
mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), format * indented_head = mk_indent(m(), 1, head);
// TODO: non-deterministic parameter evaluation format * arg_seq = mk_seq<format**, f2f>(m(), it, end, f2f());
mk_indent(m(), SMALL_INDENT, mk_compose(m(), format * close_paren = mk_string(m(), ")");
mk_seq<format**, f2f>(m(), it, end, f2f()), format * body = mk_compose(m(), arg_seq, close_paren);
mk_string(m(), ")"))))); format * indented_body = mk_indent(m(), SMALL_INDENT, body);
format * combined = mk_compose(m(), indented_head, indented_body);
f = mk_group(m(), combined);
} }
else { else {
format * first = *it; format * first = *it;
++it; ++it;
// TODO: non-deterministic parameter evaluation format * open_paren = mk_string(m(), "(");
f = mk_group(m(), mk_compose(m(), format * head = mk_compose(m(), open_paren, fname);
mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), format * indented_head = mk_indent(m(), 1, head);
// TODO: non-deterministic parameter evaluation format * space = mk_string(m(), " ");
mk_indent(m(), len + 2, mk_compose(m(), format * first_part = mk_compose(m(), space, first);
mk_string(m(), " "), format * rest_seq = mk_seq<format**, f2f>(m(), it, end, f2f());
first, format * with_rest = mk_compose(m(), first_part, rest_seq);
mk_seq<format**, f2f>(m(), it, end, f2f()), format * close_paren = mk_string(m(), ")");
mk_string(m(), ")"))))); format * body = mk_compose(m(), with_rest, close_paren);
format * indented_body = mk_indent(m(), len + 2, body);
format * combined = mk_compose(m(), indented_head, indented_body);
f = mk_group(m(), combined);
} }
} }
info f_info(0, 1, 1); info f_info(0, 1, 1);

7
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -459,9 +459,10 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta
auto fid = m_fpa_util.get_family_id(); auto fid = m_fpa_util.get_family_id();
auto k = is_decl_of(f, fid, OP_FPA_MIN) ? OP_FPA_MIN_I : OP_FPA_MAX_I; auto k = is_decl_of(f, fid, OP_FPA_MIN) ? OP_FPA_MIN_I : OP_FPA_MAX_I;
func_decl_ref min_max_i(m.mk_func_decl(fid, k, 0, nullptr, 2, pn_args), m); func_decl_ref min_max_i(m.mk_func_decl(fid, k, 0, nullptr, 2, pn_args), m);
// TODO: non-deterministic parameter evaluation expr_ref var0(m.mk_var(0, srt), m);
expr_ref else_value(m.mk_app(min_max_i, m.mk_var(0, srt), m.mk_var(1, srt)), m); expr_ref var1(m.mk_var(1, srt), m);
flt_fi->set_else(else_value); expr_ref else_app(m.mk_app(min_max_i, var0.get(), var1.get()), m);
flt_fi->set_else(else_app);
target_model->register_decl(f, flt_fi); target_model->register_decl(f, flt_fi);
TRACE(bv2fpa, tout << "fp.min/fp.max special: " << std::endl << TRACE(bv2fpa, tout << "fp.min/fp.max special: " << std::endl <<

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1207,9 +1207,9 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
lshift = edr_tmp; lshift = edr_tmp;
rshift = nedr_tmp; rshift = nedr_tmp;
// TODO: non-deterministic parameter evaluation expr_ref ashr_expr(m_bv_util.mk_bv_ashr(a_sig_ext, rshift), m);
shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), expr_ref shl_expr(m_bv_util.mk_bv_shl(a_sig_ext, lshift), m);
m_bv_util.mk_bv_shl(a_sig_ext, lshift)); shifted = m.mk_ite(exp_diff_is_neg, ashr_expr.get(), shl_expr.get());
huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext); huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext);
huge_div = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, shifted, b_sig_ext); huge_div = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, shifted, b_sig_ext);
huge_div_is_even = m.mk_eq(m_bv_util.mk_extract(0, 0, huge_div), m_bv_util.mk_numeral(0, 1)); huge_div_is_even = m.mk_eq(m_bv_util.mk_extract(0, 0, huge_div), m_bv_util.mk_numeral(0, 1));
@ -3461,9 +3461,9 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
dbg_decouple("fpa2bv_to_bv_shift", shift); dbg_decouple("fpa2bv_to_bv_shift", shift);
expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m);
// TODO: non-deterministic parameter evaluation expr_ref lshr_expr(m_bv_util.mk_bv_lshr(big_sig, shift), m);
big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), expr_ref shl_expr(m_bv_util.mk_bv_shl(big_sig, shift), m);
m_bv_util.mk_bv_shl(big_sig, shift)); big_sig_shifted = m.mk_ite(is_neg_shift, lshr_expr.get(), shl_expr.get());
int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted); int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted);
SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3); SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3);
last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted); last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted);