From 77962ff3bba7c9da5163aafaab41330fec394990 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 30 Oct 2025 07:32:50 -0700 Subject: [PATCH] fix param evaluation non-determinism Signed-off-by: Lev Nachmanson --- src/ast/ast.cpp | 16 ++++++---- src/ast/ast_smt2_pp.cpp | 54 ++++++++++++++++++-------------- src/ast/fpa/bv2fpa_converter.cpp | 7 +++-- src/ast/fpa/fpa2bv_converter.cpp | 12 +++---- 4 files changed, 50 insertions(+), 39 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 1ce0be4b2..f6356c359 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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)) { arith_util au(*this); - if (s->get_decl_kind() == REAL_SORT) - // TODO: non-deterministic parameter evaluation - return mk_ite(e, au.mk_real(1), au.mk_real(0)); - else - // TODO: non-deterministic parameter evaluation - return mk_ite(e, au.mk_int(1), au.mk_int(0)); + if (s->get_decl_kind() == REAL_SORT) { + expr_ref one(au.mk_real(1), *this); + expr_ref zero(au.mk_real(0), *this); + return mk_ite(e, one.get(), zero.get()); + } + 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 { return e; diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 5a51fa4d2..5b0c69b3e 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -592,21 +592,22 @@ class smt2_printer { } format * pp_attribute(char const * attr, format * f) { - // TODO: non-deterministic parameter evaluation - return mk_compose(m(), - mk_string(m(), attr), - mk_indent(m(), static_cast(strlen(attr)), f)); + format * attr_fmt = mk_string(m(), attr); + format * indented = mk_indent(m(), static_cast(strlen(attr)), f); + return mk_compose(m(), attr_fmt, indented); } format * pp_simple_attribute(char const * attr, int v) { - // TODO: non-deterministic parameter evaluation - return mk_compose(m(), mk_string(m(), attr), mk_int(m(), v)); + format * attr_fmt = mk_string(m(), attr); + 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) { std::string str = ensure_quote(s); - // TODO: non-deterministic parameter evaluation - return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str)); + format * attr_fmt = mk_string(m(), attr); + format * sym_fmt = mk_string(m(), str); + return mk_compose(m(), attr_fmt, sym_fmt); } format * pp_labels(bool is_pos, buffer const & names, format * f) { @@ -765,26 +766,31 @@ class smt2_printer { SASSERT(it < end); format * fname = m_env.pp_fdecl(t->get_decl(), len); if (len > MAX_INDENT) { - // TODO: non-deterministic parameter evaluation - f = mk_group(m(), mk_compose(m(), - mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), - // TODO: non-deterministic parameter evaluation - mk_indent(m(), SMALL_INDENT, mk_compose(m(), - mk_seq(m(), it, end, f2f()), - mk_string(m(), ")"))))); + format * open_paren = mk_string(m(), "("); + format * head = mk_compose(m(), open_paren, fname); + format * indented_head = mk_indent(m(), 1, head); + format * arg_seq = mk_seq(m(), it, end, f2f()); + format * close_paren = mk_string(m(), ")"); + format * body = mk_compose(m(), arg_seq, close_paren); + format * indented_body = mk_indent(m(), SMALL_INDENT, body); + format * combined = mk_compose(m(), indented_head, indented_body); + f = mk_group(m(), combined); } else { format * first = *it; ++it; - // TODO: non-deterministic parameter evaluation - f = mk_group(m(), mk_compose(m(), - mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), - // TODO: non-deterministic parameter evaluation - mk_indent(m(), len + 2, mk_compose(m(), - mk_string(m(), " "), - first, - mk_seq(m(), it, end, f2f()), - mk_string(m(), ")"))))); + format * open_paren = mk_string(m(), "("); + format * head = mk_compose(m(), open_paren, fname); + format * indented_head = mk_indent(m(), 1, head); + format * space = mk_string(m(), " "); + format * first_part = mk_compose(m(), space, first); + format * rest_seq = mk_seq(m(), it, end, f2f()); + format * with_rest = mk_compose(m(), first_part, rest_seq); + format * close_paren = 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); diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 329e8e5ec..0224d5677 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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 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); - // TODO: non-deterministic parameter evaluation - expr_ref else_value(m.mk_app(min_max_i, m.mk_var(0, srt), m.mk_var(1, srt)), m); - flt_fi->set_else(else_value); + expr_ref var0(m.mk_var(0, srt), m); + expr_ref var1(m.mk_var(1, srt), m); + 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); TRACE(bv2fpa, tout << "fp.min/fp.max special: " << std::endl << diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index c11ae6ca6..e24ac5aa4 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1207,9 +1207,9 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r lshift = edr_tmp; rshift = nedr_tmp; - // TODO: non-deterministic parameter evaluation - shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), - m_bv_util.mk_bv_shl(a_sig_ext, lshift)); + expr_ref ashr_expr(m_bv_util.mk_bv_ashr(a_sig_ext, rshift), m); + expr_ref shl_expr(m_bv_util.mk_bv_shl(a_sig_ext, lshift), m); + 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_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)); @@ -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); expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); - // TODO: non-deterministic parameter evaluation - big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), - m_bv_util.mk_bv_shl(big_sig, shift)); + expr_ref lshr_expr(m_bv_util.mk_bv_lshr(big_sig, shift), m); + expr_ref shl_expr(m_bv_util.mk_bv_shl(big_sig, shift), m); + 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); 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);