From ba83ec929afd0d4fa26e5bfcf8ccce244c39c1b3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 29 Oct 2025 06:25:03 -0700 Subject: [PATCH] passing with open ai codex on some non-deterministic param eval Signed-off-by: Lev Nachmanson --- src/ast/bv_decl_plugin.cpp | 54 ++-- src/ast/format.h | 86 +++--- src/ast/fpa/fpa2bv_rewriter.cpp | 8 +- src/ast/rewriter/bv_rewriter.cpp | 144 ++++++---- src/ast/sls/sls_array_plugin.cpp | 7 +- src/ast/sls/sls_datatype_plugin.cpp | 6 +- src/cmd_context/cmd_context.cpp | 6 +- src/muz/spacer/spacer_qe_project.cpp | 57 ++-- src/muz/spacer/spacer_util.cpp | 6 +- src/muz/transforms/dl_mk_array_blast.cpp | 10 +- src/muz/transforms/dl_mk_scale.cpp | 10 +- src/opt/opt_context.cpp | 5 +- src/qe/mbp/mbp_arith.cpp | 8 +- src/qe/mbp/mbp_arrays.cpp | 7 +- src/qe/mbp/mbp_solve_plugin.cpp | 10 +- src/qe/nlqsat.cpp | 17 +- src/qe/qe_arith_plugin.cpp | 6 +- src/smt/theory_char.cpp | 6 +- src/smt/theory_lra.cpp | 17 +- src/smt/theory_special_relations.cpp | 61 ++-- src/tactic/aig/aig.cpp | 12 +- src/tactic/arith/bv2real_rewriter.cpp | 50 ++-- src/tactic/arith/factor_tactic.cpp | 6 +- src/tactic/arith/lia2card_tactic.cpp | 5 +- src/tactic/arith/pb2bv_tactic.cpp | 12 +- src/tactic/arith/purify_arith_tactic.cpp | 344 ++++++++++++++++++----- src/tactic/fd_solver/enum2bv_solver.cpp | 5 +- src/tactic/fd_solver/smtfd_solver.cpp | 16 +- src/util/sorting_network.h | 55 ++-- 29 files changed, 665 insertions(+), 371 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index cbc4b317d..770202478 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -47,10 +47,11 @@ void bv_decl_plugin::set_manager(ast_manager * m, family_id id) { for (unsigned i = 1; i <= 64; i++) mk_bv_sort(i); - // TODO: non-deterministic parameter evaluation - m_bit0 = m->mk_const_decl(symbol("bit0"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT0)); - // TODO: non-deterministic parameter evaluation - m_bit1 = m->mk_const_decl(symbol("bit1"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT1)); + sort* bv1 = get_bv_sort(1); + func_decl_info bit0_info(m_family_id, OP_BIT0); + func_decl_info bit1_info(m_family_id, OP_BIT1); + m_bit0 = m->mk_const_decl(symbol("bit0"), bv1, bit0_info); + m_bit1 = m->mk_const_decl(symbol("bit1"), bv1, bit1_info); m->inc_ref(m_bit0); m->inc_ref(m_bit1); @@ -511,8 +512,9 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) { unsigned bv_size = arity; m_mkbv.reserve(bv_size+1); if (m_mkbv[bv_size] == 0) { - // TODO: non-deterministic parameter evaluation - m_mkbv[bv_size] = m_manager->mk_func_decl(m_mkbv_sym, arity, domain, get_bv_sort(bv_size), func_decl_info(m_family_id, OP_MKBV)); + sort* rng = get_bv_sort(bv_size); + func_decl_info info(m_family_id, OP_MKBV); + m_mkbv[bv_size] = m_manager->mk_func_decl(m_mkbv_sym, arity, domain, rng, info); m_manager->inc_ref(m_mkbv[bv_size]); } return m_mkbv[bv_size]; @@ -581,27 +583,35 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_CONCAT: if (!get_concat_size(arity, domain, r_size)) m_manager->raise_exception("invalid concat application"); - // TODO: non-deterministic parameter evaluation - return m_manager->mk_func_decl(m_concat_sym, arity, domain, get_bv_sort(r_size), - func_decl_info(m_family_id, k)); + { + sort* rng = get_bv_sort(r_size); + func_decl_info info(m_family_id, k); + return m_manager->mk_func_decl(m_concat_sym, arity, domain, rng, info); + } case OP_SIGN_EXT: if (!get_extend_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid sign_extend application"); - // TODO: non-deterministic parameter evaluation - return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, get_bv_sort(r_size), - func_decl_info(m_family_id, k, num_parameters, parameters)); + { + sort* rng = get_bv_sort(r_size); + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, rng, info); + } case OP_ZERO_EXT: if (!get_extend_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid zero_extend application"); - // TODO: non-deterministic parameter evaluation - return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, get_bv_sort(r_size), - func_decl_info(m_family_id, k, num_parameters, parameters)); + { + sort* rng = get_bv_sort(r_size); + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, rng, info); + } case OP_EXTRACT: if (!get_extract_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid extract application"); - // TODO: non-deterministic parameter evaluation - return m_manager->mk_func_decl(m_extract_sym, arity, domain, get_bv_sort(r_size), - func_decl_info(m_family_id, k, num_parameters, parameters)); + { + sort* rng = get_bv_sort(r_size); + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m_manager->mk_func_decl(m_extract_sym, arity, domain, rng, info); + } case OP_ROTATE_LEFT: if (arity != 1) m_manager->raise_exception("rotate left expects one argument"); @@ -623,9 +633,11 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p m_manager->raise_exception("repeat expects one nonzero integer parameter"); if (!get_bv_size(domain[0], bv_size)) m_manager->raise_exception("repeat expects an argument with bit-vector sort"); - // TODO: non-deterministic parameter evaluation - return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()), - func_decl_info(m_family_id, k, num_parameters, parameters)); + { + sort* rng = get_bv_sort(bv_size * parameters[0].get_int()); + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m_manager->mk_func_decl(m_repeat_sym, arity, domain, rng, info); + } default: return nullptr; } diff --git a/src/ast/format.h b/src/ast/format.h index 3320e0229..8ebf25329 100644 --- a/src/ast/format.h +++ b/src/ast/format.h @@ -87,26 +87,28 @@ namespace format_ns { elem_n) */ template - format * mk_seq1(ast_manager & m, It const & begin, It const & end, ToDoc proc, char const * header, + format * mk_seq1(ast_manager & m, It const & begin, It const & end, ToDoc proc, char const * header, char const * lp = "(", char const * rp = ")") { if (begin == end) - // TODO: non-deterministic parameter evaluation - return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); + { + format * lp_fmt = mk_string(m, lp); + format * header_fmt = mk_string(m, header); + format * rp_fmt = mk_string(m, rp); + return mk_compose(m, lp_fmt, header_fmt, rp_fmt); + } unsigned indent = static_cast(strlen(lp) + strlen(header) + 1); It it = begin; format * first = proc(*it); ++it; - // TODO: non-deterministic parameter evaluation - return mk_group(m, mk_compose(m, - mk_string(m, lp), - mk_string(m, header), - mk_indent(m, indent, - // TODO: non-deterministic parameter evaluation - mk_compose(m, - mk_string(m, " "), - first, - mk_seq(m, it, end, proc), - mk_string(m, rp))))); + format * lp_fmt = mk_string(m, lp); + format * header_fmt = mk_string(m, header); + format * space_fmt = mk_string(m, " "); + format * seq_fmt = mk_seq(m, it, end, proc); + format * rp_fmt = mk_string(m, rp); + format * tail_comp = mk_compose(m, space_fmt, first, seq_fmt, rp_fmt); + format * indented = mk_indent(m, indent, tail_comp); + format * composed = mk_compose(m, lp_fmt, header_fmt, indented); + return mk_group(m, composed); } template @@ -149,8 +151,12 @@ namespace format_ns { unsigned indent = FORMAT_DEFAULT_INDENT, char const * lp = "(", char const * rp = ")") { SASSERT(i >= 1); if (begin == end) - // TODO: non-deterministic parameter evaluation - return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); + { + format * lp_fmt = mk_string(m, lp); + format * header_fmt = mk_string(m, header); + format * rp_fmt = mk_string(m, rp); + return mk_compose(m, lp_fmt, header_fmt, rp_fmt); + } unsigned idx = 0; It end1 = begin; for (;end1 != end && idx < i; ++end1, ++idx) @@ -158,17 +164,19 @@ namespace format_ns { It it = begin; format * first = proc(*it); ++it; - return mk_group(m, - // TODO: non-deterministic parameter evaluation - mk_compose(m, - // TODO: non-deterministic parameter evaluation - mk_compose(m, mk_string(m, lp), mk_string(m, header)), - mk_group(m, mk_indent(m, static_cast(strlen(header) + strlen(lp) + 1), - // TODO: non-deterministic parameter evaluation - mk_compose(m, mk_string(m, " "), first, - mk_seq(m, it, end1, proc)))), - mk_indent(m, indent, mk_seq(m, end1, end, proc)), - mk_string(m, rp))); + unsigned header_indent = static_cast(strlen(header) + strlen(lp) + 1); + format * lp_fmt = mk_string(m, lp); + format * header_fmt = mk_string(m, header); + format * header_compose = mk_compose(m, lp_fmt, header_fmt); + format * space_fmt = mk_string(m, " "); + format * prefix_seq = mk_seq(m, it, end1, proc); + format * prefix_comp = mk_compose(m, space_fmt, first, prefix_seq); + format * indent_prefix = mk_group(m, mk_indent(m, header_indent, prefix_comp)); + format * suffix_seq = mk_seq(m, end1, end, proc); + format * suffix_indent = mk_indent(m, indent, suffix_seq); + format * rp_fmt = mk_string(m, rp); + format * composed = mk_compose(m, header_compose, indent_prefix, suffix_indent, rp_fmt); + return mk_group(m, composed); } /** @@ -181,19 +189,23 @@ namespace format_ns { format * mk_seq4(ast_manager & m, It const & begin, It const & end, ToDoc proc, unsigned indent = FORMAT_DEFAULT_INDENT, char const * lp = "(", char const * rp = ")") { if (begin == end) - // TODO: non-deterministic parameter evaluation - return mk_compose(m, mk_string(m, lp), mk_string(m, rp)); + { + format * lp_fmt = mk_string(m, lp); + format * rp_fmt = mk_string(m, rp); + return mk_compose(m, lp_fmt, rp_fmt); + } unsigned indent1 = static_cast(strlen(lp)); It it = begin; format * first = proc(*it); ++it; - // TODO: non-deterministic parameter evaluation - return mk_group(m, mk_compose(m, - mk_indent(m, indent1, mk_compose(m, mk_string(m, lp), first)), - // TODO: non-deterministic parameter evaluation - mk_indent(m, indent, mk_compose(m, - mk_seq(m, it, end, proc), - mk_string(m, rp))))); + format * lp_fmt = mk_string(m, lp); + format * first_comp = mk_compose(m, lp_fmt, first); + format * first_indent = mk_indent(m, indent1, first_comp); + format * seq_rest = mk_seq(m, it, end, proc); + format * rp_fmt = mk_string(m, rp); + format * tail_comp = mk_compose(m, seq_rest, rp_fmt); + format * tail_indent = mk_indent(m, indent, tail_comp); + return mk_group(m, mk_compose(m, first_indent, tail_indent)); } /** @@ -209,5 +221,3 @@ namespace format_ns { } }; - - diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 423ea851c..fb0c8e44d 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -258,10 +258,10 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res unsigned ebits = m_conv.fu().get_ebits(s); unsigned sbits = m_conv.fu().get_sbits(s); new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); - // TODO: non-deterministic parameter evaluation - new_exp = m_conv.fu().mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), - m_conv.bu().mk_extract(ebits - 1, 0, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var)); + expr_ref sign(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), m()); + expr_ref exponent(m_conv.bu().mk_extract(ebits - 1, 0, new_var), m()); + expr_ref significand(m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), m()); + new_exp = m_conv.fu().mk_fp(sign, exponent, significand); } else if (m_conv.is_rm(s)) { expr_ref new_var(m()); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 380019a95..9c937f8c7 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -384,9 +384,10 @@ br_status bv_rewriter::rw_leq_overflow(bool is_signed, expr * a, expr * b, expr_ } else { SASSERT(lower.is_pos()); - // TODO: non-deterministic parameter evaluation - result = m.mk_and(m_util.mk_ule(mk_numeral(lower, sz), common), - m_util.mk_ule(common, mk_numeral(upper, sz))); + expr_ref lower_bound(m), upper_bound(m); + lower_bound = m_util.mk_ule(mk_numeral(lower, sz), common); + upper_bound = m_util.mk_ule(common, mk_numeral(upper, sz)); + result = m.mk_and(lower_bound, upper_bound); } return BR_REWRITE2; } @@ -448,9 +449,10 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr return BR_DONE; } if (common > 0) { - // TODO: non-deterministic parameter evaluation - result = m_util.mk_ule(concat(numa - common, a->get_args() + common), - concat(numb - common, b->get_args() + common)); + expr_ref tail_a(m), tail_b(m); + tail_a = concat(numa - common, a->get_args() + common); + tail_b = concat(numb - common, b->get_args() + common); + result = m_util.mk_ule(tail_a, tail_b); return BR_REWRITE2; } } @@ -471,10 +473,11 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr return BR_DONE; } if (new_numa != numa) { - // TODO: non-deterministic parameter evaluation - result = is_signed ? m_util.mk_sle(concat(new_numa, a->get_args()), concat(new_numb, b->get_args())) - // TODO: non-deterministic parameter evaluation - : m_util.mk_ule(concat(new_numa, a->get_args()), concat(new_numb, b->get_args())); + expr_ref prefix_a(m), prefix_b(m); + prefix_a = concat(new_numa, a->get_args()); + prefix_b = concat(new_numb, b->get_args()); + result = is_signed ? m_util.mk_sle(prefix_a, prefix_b) + : m_util.mk_ule(prefix_a, prefix_b); return BR_REWRITE2; } } @@ -874,8 +877,10 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ expr* c = nullptr, *t = nullptr, *e = nullptr; if (m.is_ite(arg, c, t, e) && (t->get_ref_count() == 1 || e->get_ref_count() == 1 || !m.is_ite(t) || !m.is_ite(e))) { - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e)); + expr_ref then_branch(m), else_branch(m); + then_branch = m_mk_extract(high, low, t); + else_branch = m_mk_extract(high, low, e); + result = m.mk_ite(c, then_branch, else_branch); return BR_REWRITE2; } @@ -1088,8 +1093,10 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) unsigned k = r2.get_unsigned(); - // TODO: non-deterministic parameter evaluation - result = m_util.mk_concat(mk_zero(k), m_mk_extract(bv_size - 1, k, arg1)); + expr_ref high_part(m), low_part(m); + high_part = mk_zero(k); + low_part = m_mk_extract(bv_size - 1, k, arg1); + result = m_util.mk_concat(high_part, low_part); return BR_REWRITE2; } #if 0 @@ -1126,10 +1133,11 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e } else { // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff) - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size)), - mk_one(bv_size), - mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size)); + expr_ref div_zero_cond(m), div_zero_pos(m), div_zero_neg(m); + div_zero_cond = m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size)); + div_zero_pos = mk_one(bv_size); + div_zero_neg = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size); + result = m.mk_ite(div_zero_cond, div_zero_pos, div_zero_neg); return BR_REWRITE2; } } @@ -1257,10 +1265,11 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), - m.mk_app(get_fid(), OP_BSREM0, arg1), - m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2)); + expr_ref rem_zero_cond(m), rem_zero_branch(m), rem_nonzero_branch(m); + rem_zero_cond = m.mk_eq(arg2, mk_zero(bv_size)); + rem_zero_branch = m.mk_app(get_fid(), OP_BSREM0, arg1); + rem_nonzero_branch = m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2); + result = m.mk_ite(rem_zero_cond, rem_zero_branch, rem_nonzero_branch); return BR_REWRITE2; } @@ -1475,10 +1484,11 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), - m.mk_app(get_fid(), OP_BSMOD0, arg1), - m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2)); + expr_ref mod_zero_cond(m), mod_zero_branch(m), mod_nonzero_branch(m); + mod_zero_cond = m.mk_eq(arg2, mk_zero(bv_size)); + mod_zero_branch = m.mk_app(get_fid(), OP_BSMOD0, arg1); + mod_nonzero_branch = m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2); + result = m.mk_ite(mod_zero_cond, mod_zero_branch, mod_nonzero_branch); return BR_REWRITE2; } @@ -1695,8 +1705,10 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re ptr_buffer args1, args2; for (unsigned i = 0; i < new_args.size(); ++i) args1.push_back(y), args2.push_back(z); - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2)); + expr_ref then_concat(m), else_concat(m); + then_concat = m_util.mk_concat(args1); + else_concat = m_util.mk_concat(args2); + result = m.mk_ite(x, then_concat, else_concat); return BR_REWRITE2; } } @@ -2346,10 +2358,11 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(m.mk_eq(arg1, arg2), - mk_one(1), - mk_zero(1)); + expr_ref eq_cond(m), eq_then(m), eq_else(m); + eq_cond = m.mk_eq(arg1, arg2); + eq_then = mk_one(1); + eq_else = mk_zero(1); + result = m.mk_ite(eq_cond, eq_then, eq_else); return BR_REWRITE2; } @@ -2626,15 +2639,17 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu return BR_FAILED; numeral two(2); - ptr_buffer new_args; + expr_ref_vector eq_args(m); for (unsigned i = 0; i < sz; i++) { bool bit0 = (v % two).is_zero(); - // TODO: non-deterministic parameter evaluation - new_args.push_back(m.mk_eq(m_mk_extract(i,i, lhs), - mk_numeral(bit0 ? 0 : 1, 1))); + expr_ref lhs_bit(m), rhs_bit(m), eq_arg(m); + lhs_bit = m_mk_extract(i, i, lhs); + rhs_bit = mk_numeral(bit0 ? 0 : 1, 1); + eq_arg = m.mk_eq(lhs_bit, rhs_bit); + eq_args.push_back(eq_arg); div(v, two, v); } - result = m.mk_and(new_args); + result = m.mk_and(eq_args); return BR_REWRITE3; } @@ -2661,7 +2676,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { args2 = &rhs; } - ptr_buffer new_eqs; + expr_ref_vector eqs(m); unsigned low1 = 0; unsigned low2 = 0; unsigned i1 = num1; @@ -2673,11 +2688,13 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { unsigned sz2 = get_bv_size(arg2); SASSERT(low1 < sz1 && low2 < sz2); unsigned rsz1 = sz1 - low1; - unsigned rsz2 = sz2 - low2; + unsigned rsz2 = sz2 - low2; if (rsz1 == rsz2) { - // TODO: non-deterministic parameter evaluation - new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), - m_mk_extract(sz2 - 1, low2, arg2))); + expr_ref lhs_part(m), rhs_part(m), eq_part(m); + lhs_part = m_mk_extract(sz1 - 1, low1, arg1); + rhs_part = m_mk_extract(sz2 - 1, low2, arg2); + eq_part = m.mk_eq(lhs_part, rhs_part); + eqs.push_back(eq_part); low1 = 0; low2 = 0; --i1; @@ -2685,25 +2702,29 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { continue; } else if (rsz1 < rsz2) { - // TODO: non-deterministic parameter evaluation - new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), - m_mk_extract(rsz1 + low2 - 1, low2, arg2))); + expr_ref lhs_part(m), rhs_part(m), eq_part(m); + lhs_part = m_mk_extract(sz1 - 1, low1, arg1); + rhs_part = m_mk_extract(rsz1 + low2 - 1, low2, arg2); + eq_part = m.mk_eq(lhs_part, rhs_part); + eqs.push_back(eq_part); low1 = 0; low2 += rsz1; --i1; } else { - // TODO: non-deterministic parameter evaluation - new_eqs.push_back(m.mk_eq(m_mk_extract(rsz2 + low1 - 1, low1, arg1), - m_mk_extract(sz2 - 1, low2, arg2))); + expr_ref lhs_part(m), rhs_part(m), eq_part(m); + lhs_part = m_mk_extract(rsz2 + low1 - 1, low1, arg1); + rhs_part = m_mk_extract(sz2 - 1, low2, arg2); + eq_part = m.mk_eq(lhs_part, rhs_part); + eqs.push_back(eq_part); low1 += rsz2; low2 = 0; --i2; } } SASSERT(i1 == 0 && i2 == 0); - SASSERT(new_eqs.size() >= 1); - result = m.mk_and(new_eqs); + SASSERT(eqs.size() >= 1); + result = m.mk_and(eqs); return BR_REWRITE3; } @@ -3125,11 +3146,12 @@ br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ br_status bv_rewriter::mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - // TODO: non-deterministic parameter evaluation - result = m.mk_or( - m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1])), - m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1])) - ); + expr_ref no_ovfl(m), no_udfl(m), not_no_ovfl(m), not_no_udfl(m); + no_ovfl = m_util.mk_bvsmul_no_ovfl(args[0], args[1]); + no_udfl = m_util.mk_bvsmul_no_udfl(args[0], args[1]); + not_no_ovfl = m.mk_not(no_ovfl); + not_no_udfl = m.mk_not(no_udfl); + result = m.mk_or(not_no_ovfl, not_no_udfl); return BR_REWRITE_FULL; } @@ -3283,7 +3305,11 @@ br_status bv_rewriter::mk_bvssub_under_overflow(unsigned num, expr * const * arg auto bvsaddo_stat = mk_bvsadd_over_underflow(2, args2, bvsaddo); SASSERT(bvsaddo_stat != BR_FAILED); (void)bvsaddo_stat; auto first_arg_ge_zero = m_util.mk_sle(mk_zero(sz), args[0]); - result = m.mk_ite(m.mk_eq(args[1], minSigned), first_arg_ge_zero, bvsaddo); + expr_ref eq_min_signed(m), ite_then(m), ite_else(m); + eq_min_signed = m.mk_eq(args[1], minSigned); + ite_then = first_arg_ge_zero; + ite_else = bvsaddo; + result = m.mk_ite(eq_min_signed, ite_then, ite_else); return BR_REWRITE_FULL; } @@ -3295,8 +3321,10 @@ br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, exp auto sz = get_bv_size(args[1]); auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz); auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz); - // TODO: non-deterministic parameter evaluation - result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne)); + expr_ref eq_min_signed(m), eq_minus_one(m); + eq_min_signed = m.mk_eq(args[0], minSigned); + eq_minus_one = m.mk_eq(args[1], minusOne); + result = m.mk_and(eq_min_signed, eq_minus_one); return BR_REWRITE_FULL; } diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp index 90be6a999..751ebcb0f 100644 --- a/src/ast/sls/sls_array_plugin.cpp +++ b/src/ast/sls/sls_array_plugin.cpp @@ -413,9 +413,10 @@ namespace sls { args2.push_back(k); } expr_ref sel1(a.mk_select(args1), m); - expr_ref sel2(a.mk_select(args2), m); - // TODO: non-deterministic parameter evaluation - bool r = ctx.add_constraint(m.mk_implies(m.mk_eq(sel1, sel2), m.mk_eq(x, y))); + expr_ref sel2(a.mk_select(args2), m); + expr* eq_select = m.mk_eq(sel1, sel2); + expr* eq_arrays = m.mk_eq(x, y); + bool r = ctx.add_constraint(m.mk_implies(eq_select, eq_arrays)); if (r) ++m_stats.m_num_axioms; return r; diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp index 6014e8d6d..16a70cfe4 100644 --- a/src/ast/sls/sls_datatype_plugin.cpp +++ b/src/ast/sls/sls_datatype_plugin.cpp @@ -254,8 +254,10 @@ namespace sls { expr_ref_vector args(m); for (auto a : acc) args.push_back(m.mk_app(a, t)); - // TODO: non-deterministic parameter evaluation - m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args)))); + expr_ref cons(m.mk_app(c, args), m); + expr* is_c = m.mk_app(r, t); + expr_ref eq_term(m.mk_eq(t, cons), m); + m_axioms.push_back(m.mk_iff(is_c, eq_term)); } } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 753219f53..56e746049 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1759,8 +1759,9 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions for (unsigned i = 0; i < sz; ++i) { if (m_assertion_names.size() > i && m_assertion_names[i]) { asms.push_back(m_assertion_names[i]); - // TODO: non-deterministic parameter evaluation - assertions.push_back(m().mk_implies(m_assertion_names[i], m_assertions[i])); + expr* name = m_assertion_names[i]; + expr* assertion = m_assertions[i]; + assertions.push_back(m().mk_implies(name, assertion)); } else { assertions.push_back(m_assertions[i]); @@ -2529,4 +2530,3 @@ std::ostream & operator<<(std::ostream & out, cmd_context::status st) { } return out; } - diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 287a9d456..7e98a2cb9 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -559,9 +559,8 @@ class arith_project_util { tout << "lcm of divs: " << lcm_divs << "\n";); } - // TODO: non-deterministic parameter evaluation - expr_ref z(a.mk_numeral(rational::zero(), a.mk_int()), m); - expr_ref x_term_val(m); + expr_ref z(a.mk_numeral(rational::zero(), true), m); + expr_ref x_term_val(m); // use equality term if (eq_idx < lits.size()) { @@ -627,9 +626,9 @@ class arith_project_util { // (lcm_coeffs * var_val) % lcm_divs instead rational var_val_num; VERIFY(a.is_numeral(var_val, var_val_num)); - // TODO: non-deterministic parameter evaluation - x_term_val = a.mk_numeral( - mod(lcm_coeffs * var_val_num, lcm_divs), a.mk_int()); + rational mod_val = mod(lcm_coeffs * var_val_num, lcm_divs); + x_term_val = a.mk_numeral(mod_val, true); + std::cout << "t"; TRACE(qe, tout << "Substitution for (lcm_coeffs * x): " << mk_pp(x_term_val, m) << "\n";); } @@ -649,10 +648,9 @@ class arith_project_util { // XXX Rewrite before applying divisibility to preserve // syntactic structure m_rw(new_lit); - new_lit = m.mk_eq( - // TODO: non-deterministic parameter evaluation - a.mk_mod(new_lit, a.mk_numeral(m_divs[i], a.mk_int())), - z); + expr* mod_val = a.mk_numeral(m_divs[i], true); + expr* mod_expr = a.mk_mod(new_lit, mod_val); + new_lit = m.mk_eq(mod_expr, z); } else if (m_eq[i] || (num_pos == 0 && m_coeffs[i].is_pos()) || (num_neg == 0 && m_coeffs[i].is_neg())) { new_lit = m.mk_false(); @@ -737,12 +735,11 @@ class arith_project_util { // (t+offset) // // for positive term, subtract from 0 - x_term_val = - mk_add(m_terms.get(max_t), a.mk_numeral(offset, a.mk_int())); + expr* offset_expr = a.mk_numeral(offset, true); + x_term_val = mk_add(m_terms.get(max_t), offset_expr); if (m_strict[max_t]) { - x_term_val = a.mk_add( - // TODO: non-deterministic parameter evaluation - x_term_val, a.mk_numeral(rational::one(), a.mk_int())); + expr* one = a.mk_numeral(rational::one(), true); + x_term_val = a.mk_add(x_term_val, one); } if (m_coeffs[max_t].is_pos()) { x_term_val = a.mk_uminus(x_term_val); @@ -757,9 +754,9 @@ class arith_project_util { if (!lcm_coeffs.is_one()) { // new div constraint: lcm_coeffs | x_term_val - div_lit = m.mk_eq( - a.mk_mod(x_term_val, a.mk_numeral(lcm_coeffs, a.mk_int())), - z); + expr* mod_val = a.mk_numeral(lcm_coeffs, true); + expr* mod_expr = a.mk_mod(x_term_val, mod_val); + div_lit = m.mk_eq(mod_expr, z); } } return true; @@ -980,8 +977,7 @@ class arith_project_util { return; } - // TODO: non-deterministic parameter evaluation - expr_ref z(a.mk_numeral(rational::zero(), a.mk_int()), m); + expr_ref z(a.mk_numeral(rational::zero(), true), m); bool is_mod_eq = false; expr *e1, *e2, *num; @@ -1013,21 +1009,21 @@ class arith_project_util { if (a.is_numeral(t2, t2_num) && t2_num.is_zero()) { // already in the desired form; // new_fml is (num_val | t1) - new_fml = - m.mk_eq(a.mk_mod(t1, a.mk_numeral(num_val, a.mk_int())), z); + expr* mod_val = a.mk_numeral(num_val, true); + expr* mod_expr = a.mk_mod(t1, mod_val); + new_fml = m.mk_eq(mod_expr, z); } else { expr_ref_vector lits(m); // num_val | (t1 - t2) lits.push_back( m.mk_eq(a.mk_mod(a.mk_sub(t1, t2), - a.mk_numeral(num_val, a.mk_int())), + a.mk_numeral(num_val, true)), z)); // 0 <= t2 lits.push_back(a.mk_le(z, t2)); // t2 < abs (num_val) - lits.push_back( - // TODO: non-deterministic parameter evaluation - a.mk_lt(t2, a.mk_numeral(abs(num_val), a.mk_int()))); + expr* abs_val = a.mk_numeral(abs(num_val), true); + lits.push_back(a.mk_lt(t2, abs_val)); new_fml = m.mk_and(lits.size(), lits.data()); } @@ -1079,8 +1075,7 @@ class arith_project_util { */ void mk_lit_substitutes(expr_ref const &x_term_val, expr_map &map, unsigned idx) { - // TODO: non-deterministic parameter evaluation - expr_ref z(a.mk_numeral(rational::zero(), a.mk_int()), m); + expr_ref z(a.mk_numeral(rational::zero(), true), m); expr_ref cxt(m), new_lit(m); for (unsigned i = 0; i < m_lits.size(); ++i) { if (i == idx) { @@ -1107,9 +1102,9 @@ class arith_project_util { // XXX rewrite before applying mod to ensure mod is the // top-level operator m_rw(cxt); - new_lit = m.mk_eq( - // TODO: non-deterministic parameter evaluation - a.mk_mod(cxt, a.mk_numeral(m_divs[i], a.mk_int())), z); + expr* mod_val = a.mk_numeral(m_divs[i], true); + expr* mod_expr = a.mk_mod(cxt, mod_val); + new_lit = m.mk_eq(mod_expr, z); } } map.insert(m_lits.get(i), new_lit, nullptr); diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 4d38c2fe2..053b17a01 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -359,9 +359,9 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) { rational two(2); for (unsigned j = 0; j < bv_size; ++j) { parameter p(j); - // TODO: non-deterministic parameter evaluation - expr *e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), - bv.mk_extract(j, j, c)); + expr* bit1 = m.mk_app(bv.get_family_id(), OP_BIT1); + expr* bit = bv.mk_extract(j, j, c); + expr *e = m.mk_eq(bit1, bit); if ((r % two).is_zero()) { e = m.mk_not(e); } r = div(r, two); if (j == 0) diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 632f1d06a..f59a0883c 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -225,11 +225,12 @@ namespace datalog { get_select_args(a1, args1); get_select_args(a2, args2); for (unsigned j = 0; j < args1.size(); ++j) { - // TODO: non-deterministic parameter evaluation - eqs.push_back(m.mk_eq(args1[j], args2[j])); + expr_ref eq_expr(m.mk_eq(args1[j], args2[j]), m); + eqs.push_back(eq_expr); } - // TODO: non-deterministic parameter evaluation - conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.data()), m.mk_eq(v1, v2))); + expr_ref antecedent(m.mk_and(eqs.size(), eqs.data()), m); + expr_ref consequent(m.mk_eq(v1, v2), m); + conjs.push_back(m.mk_implies(antecedent, consequent)); } } body = m.mk_and(conjs.size(), conjs.data()); @@ -337,4 +338,3 @@ namespace datalog { }; - diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index c6a967fb2..4a237168d 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -52,11 +52,11 @@ namespace datalog { TRACE(dl, tout << new_p->get_name() << " has no value in the current model\n";); continue; } - for (unsigned i = 0; i < old_p->get_arity(); ++i) { - subst.push_back(m.mk_var(i, old_p->get_domain(i))); - } - // TODO: non-deterministic parameter evaluation - subst.push_back(a.mk_numeral(rational(1), a.mk_real())); + for (unsigned i = 0; i < old_p->get_arity(); ++i) { + subst.push_back(m.mk_var(i, old_p->get_domain(i))); + } + // add scaling factor 1 for the new parameter + subst.push_back(a.mk_numeral(rational(1), false)); SASSERT(!new_fi->is_partial() && new_fi->num_entries() == 0); tmp = vs(new_fi->get_else(), subst.size(), subst.data()); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 56e9260e3..90705ae98 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1066,8 +1066,9 @@ namespace opt { expr_ref_vector soft(m); for (unsigned k = 1; k <= min_cardinality; ++k) { auto p_k = m.mk_fresh_const("p", m.mk_bool_sort()); - // TODO: non-deterministic parameter evaluation - soft.push_back(m.mk_ite(p_k, a.mk_int(1), a.mk_int(0))); + expr* one = a.mk_int(1); + expr* zero = a.mk_int(0); + soft.push_back(m.mk_ite(p_k, one, zero)); for (auto c : cardinalities) // p_k => c >= k if (is_max) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 84dab5a70..62aaafc1e 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -577,8 +577,12 @@ namespace mbp { case opt::t_le: t = a.mk_le(t, s); break; case opt::t_eq: t = a.mk_eq(t, s); break; case opt::t_divides: - // TODO: non-deterministic parameter evaluation - t = a.mk_eq(a.mk_mod(t, a.mk_int(r.m_mod)), a.mk_int(0)); + { + expr* mod_val = a.mk_int(r.m_mod); + expr* mod_expr = a.mk_mod(t, mod_val); + expr* zero = a.mk_int(0); + t = a.mk_eq(mod_expr, zero); + } break; default: UNREACHABLE(); diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 53c19e8e4..79eeac0bd 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -866,9 +866,10 @@ namespace mbp { SASSERT(xs.size() == ys.size() && !xs.empty()); expr_ref result(mk_lt(xs.back(), ys.back()), m); for (unsigned i = xs.size()-1; i-- > 0; ) { - // TODO: non-deterministic parameter evaluation - result = m.mk_or(mk_lt(xs[i], ys[i]), - m.mk_and(m.mk_eq(xs[i], ys[i]), result)); + expr_ref is_less(mk_lt(xs[i], ys[i]), m); + expr_ref is_equal(m.mk_eq(xs[i], ys[i]), m); + expr_ref conj(m.mk_and(is_equal, result), m); + result = m.mk_or(is_less, conj); } return result; } diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp index bbd4e752b..6a73f80a0 100644 --- a/src/qe/mbp/mbp_solve_plugin.cpp +++ b/src/qe/mbp/mbp_solve_plugin.cpp @@ -287,10 +287,12 @@ namespace mbp { }; // `first` is a value, different from 0 - // TODO: non-deterministic parameter evaluation - res = m.mk_and(m.mk_eq(second, a.mk_idiv(lhs, first)), - // TODO: non-deterministic parameter evaluation - m.mk_eq(a.mk_int(0), a.mk_mod(lhs, first))); + expr* div_expr = a.mk_idiv(lhs, first); + expr* eq_div = m.mk_eq(second, div_expr); + expr* mod_expr = a.mk_mod(lhs, first); + expr* eq_mod = m.mk_eq(a.mk_int(0), mod_expr); + expr* conjuncts[2] = { eq_div, eq_mod }; + res = m.mk_and(2, conjuncts); return true; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index a941be10d..2ddadf7ad 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -656,18 +656,22 @@ namespace qe { expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m); paxioms.push_back(m.mk_or(den_is0, m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); for (unsigned j = i + 1; j < divs.size(); ++j) { - // TODO: non-deterministic parameter evaluation - paxioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)), - m.mk_not(m.mk_eq(divs[i].num, divs[j].num)), - m.mk_eq(divs[i].name, divs[j].name))); + expr* eq_den = m.mk_eq(divs[i].den, divs[j].den); + expr* eq_num = m.mk_eq(divs[i].num, divs[j].num); + expr* eq_name = m.mk_eq(divs[i].name, divs[j].name); + expr* not_eq_den = m.mk_not(eq_den); + expr* not_eq_num = m.mk_not(eq_num); + paxioms.push_back(m.mk_or(not_eq_den, not_eq_num, eq_name)); } } expr_ref body(arith.mk_real(0), m); expr_ref v0(m.mk_var(0, arith.mk_real()), m); expr_ref v1(m.mk_var(1, arith.mk_real()), m); for (auto const& p : divs) { - // TODO: non-deterministic parameter evaluation - body = m.mk_ite(m.mk_and(m.mk_eq(v0, p.num), m.mk_eq(v1, p.den)), p.name, body); + expr* eq_v0_num = m.mk_eq(v0, p.num); + expr* eq_v1_den = m.mk_eq(v1, p.den); + expr* guard = m.mk_and(eq_v0_num, eq_v1_den); + body = m.mk_ite(guard, p.name, body); } m_div_mc->add(arith.mk_div0(), body); } @@ -969,4 +973,3 @@ tactic * mk_nlqe_tactic(ast_manager & m, params_ref const& p) { return alloc(qe::nlqsat, m, qe::elim_t, p); } - diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 71b48ba05..16ffe3b60 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -468,8 +468,10 @@ namespace qe { // ax + t = 0 void mk_eq(rational const& a, app* x, expr* t, expr_ref& result) { - // TODO: non-deterministic parameter evaluation - result = m_arith.mk_eq(mk_add(mk_mul(a, x), t), mk_zero(x)); + expr_ref ax(mk_mul(a, x), m); + expr_ref sum(mk_add(ax, t), m); + expr* zero = mk_zero(x); + result = m_arith.mk_eq(sum, zero); } void mk_and(unsigned sz, expr*const* args, expr_ref& result) { diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index 523dff596..307a57158 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -259,8 +259,9 @@ namespace smt { unsigned p = 0; arith_util a(m); for (auto b : bits) { - // TODO: non-deterministic parameter evaluation - sum.push_back(m.mk_ite(b, a.mk_int(1 << p), a.mk_int(0))); + expr* one = a.mk_int(1 << p); + expr* zero = a.mk_int(0); + sum.push_back(m.mk_ite(b, one, zero)); p++; } expr_ref sum_bits(a.mk_add(sum), m); @@ -457,4 +458,3 @@ namespace smt { st.update("seq char2bit", m_stats.m_num_blast); } } - diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 45d80d2cc..627396678 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2569,8 +2569,11 @@ public: 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); - // TODO: non-deterministic parameter evaluation - IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n"); + IF_VERBOSE(2, { + auto shl_repr = mk_bounded_pp(n, m); + verbose_stream() << "shl: " << shl_repr << " " << valn + << " := " << valx << " << " << valy << "\n"; + }); return false; } if (a.is_lshr(n)) { @@ -2695,11 +2698,9 @@ public: for (api_bound* other : bounds) { if (other == &b) continue; - // TODO: non-deterministic parameter evaluation - if (b.get_lit() == other->get_lit()) continue; - // TODO: non-deterministic parameter evaluation + literal other_lit = other->get_lit(); + if (b.get_lit() == other_lit) continue; lp_api::bound_kind kind2 = other->get_bound_kind(); - // TODO: non-deterministic parameter evaluation rational const& k2 = other->get_value(); if (k1 == k2 && kind1 == kind2) { // the bounds are equivalent. @@ -3774,8 +3775,8 @@ public: } solutions.shrink(j); - // TODO: non-deterministic parameter evaluation - expr_ref term(m), guard(m); + expr_ref term(m); + expr_ref guard(m); vector sols; lp().solve_for(vars, sols); uint_set seen; diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 644ffb4b0..c58d87e12 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -803,8 +803,9 @@ namespace smt { r.pop(1); fi->set_else(arith.mk_numeral(rational(0), true)); mg.get_model().register_decl(fn, fi); - // TODO: non-deterministic parameter evaluation - result = arith.mk_le(m.mk_app(fn,m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + expr* arg0 = m.mk_app(fn, m.mk_var(0, *ty)); + expr* arg1 = m.mk_app(fn, m.mk_var(1, *ty)); + result = arith.mk_le(arg0, arg1); return result; } @@ -824,8 +825,9 @@ namespace smt { } fi->set_else(arith.mk_numeral(rational(0), true)); mg.get_model().register_decl(fn, fi); - // TODO: non-deterministic parameter evaluation - result = m.mk_eq(m.mk_app(fn, m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + expr* cls0 = m.mk_app(fn, m.mk_var(0, *ty)); + expr* cls1 = m.mk_app(fn, m.mk_var(1, *ty)); + result = m.mk_eq(cls0, cls1); return result; } @@ -850,10 +852,14 @@ namespace smt { hifi->set_else(arith.mk_numeral(rational(0), true)); mg.get_model().register_decl(lofn, lofi); mg.get_model().register_decl(hifn, hifi); - // TODO: non-deterministic parameter evaluation - result = m.mk_and(arith.mk_le(m.mk_app(lofn, m.mk_var(0, *ty)), m.mk_app(lofn, m.mk_var(1, *ty))), - // TODO: non-deterministic parameter evaluation - arith.mk_le(m.mk_app(hifn, m.mk_var(1, *ty)), m.mk_app(hifn, m.mk_var(0, *ty)))); + expr* lo_arg0 = m.mk_app(lofn, m.mk_var(0, *ty)); + expr* lo_arg1 = m.mk_app(lofn, m.mk_var(1, *ty)); + expr* hi_arg0 = m.mk_app(hifn, m.mk_var(0, *ty)); + expr* hi_arg1 = m.mk_app(hifn, m.mk_var(1, *ty)); + expr* lo_constraint = arith.mk_le(lo_arg0, lo_arg1); + expr* hi_constraint = arith.mk_le(hi_arg1, hi_arg0); + expr* conjuncts[2] = { lo_constraint, hi_constraint }; + result = m.mk_and(2, conjuncts); return result; } @@ -927,13 +933,13 @@ namespace smt { expr* x = xV, *S = SV; expr_ref mem_body(m); - // TODO: non-deterministic parameter evaluation - mem_body = m.mk_ite(m.mk_app(is_nil, S), - F, - // TODO: non-deterministic parameter evaluation - m.mk_ite(m.mk_eq(m.mk_app(hd, S), x), - T, - m.mk_app(memf, x, m.mk_app(tl, S)))); + expr* is_nil_S = m.mk_app(is_nil, S); + expr* hd_S = m.mk_app(hd, S); + expr* eq_hd_x = m.mk_eq(hd_S, x); + expr* tl_S = m.mk_app(tl, S); + expr* rec_call = m.mk_app(memf, x, tl_S); + expr* inner_ite = m.mk_ite(eq_hd_x, T, rec_call); + mem_body = m.mk_ite(is_nil_S, F, inner_ite); recfun_replace rep(m); var* vars[2] = { xV, SV }; p.set_definition(rep, mem, false, 2, vars, mem_body); @@ -953,11 +959,16 @@ namespace smt { var_ref SV(m.mk_var(1, listS), m); var_ref tupV(m.mk_var(0, tup), m); expr* a = aV, *b = bV, *A = AV, *S = SV, *t = tupV; - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - next_body = m.mk_ite(m.mk_and(m.mk_app(memf, a, A), m.mk_not(m.mk_app(memf, b, S))), - m.mk_app(pair, m.mk_app(cons, b, m.mk_app(fst, t)), m.mk_app(cons, b, m.mk_app(snd, t))), - t); + expr* mem_a_A = m.mk_app(memf, a, A); + expr* mem_b_S = m.mk_app(memf, b, S); + expr* not_mem_b_S = m.mk_not(mem_b_S); + expr* guard = m.mk_and(mem_a_A, not_mem_b_S); + expr* fst_t = m.mk_app(fst, t); + expr* snd_t = m.mk_app(snd, t); + expr* cons_fst = m.mk_app(cons, b, fst_t); + expr* cons_snd = m.mk_app(cons, b, snd_t); + expr* pair_term = m.mk_app(pair, cons_fst, cons_snd); + next_body = m.mk_ite(guard, pair_term, t); recfun_replace rep(m); var* vars[5] = { aV, bV, AV, SV, tupV }; @@ -989,11 +1000,11 @@ namespace smt { expr_ref Ap(m.mk_app(fst, connected_body.get()), m); expr_ref Sp(m.mk_app(snd, connected_body.get()), m); - // TODO: non-deterministic parameter evaluation - connected_body = m.mk_ite(m.mk_eq(Ap, nilc), F, - // TODO: non-deterministic parameter evaluation - m.mk_ite(m.mk_app(memf, dst, Ap), T, - m.mk_app(connectedf, Ap, dst, Sp))); + expr* eq_Ap_nilc = m.mk_eq(Ap, nilc); + expr* mem_dst_Ap = m.mk_app(memf, dst, Ap); + expr* rec_call = m.mk_app(connectedf, Ap, dst, Sp); + expr* inner_ite = m.mk_ite(mem_dst_Ap, T, rec_call); + connected_body = m.mk_ite(eq_Ap_nilc, F, inner_ite); TRACE(special_relations, tout << connected_body << "\n";); recfun_replace rep(m); diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index a64238569..ae5deb891 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -879,12 +879,15 @@ struct aig_manager::imp { } expr * r; if (m.is_not_eq(t, e)) { - // TODO: non-deterministic parameter evaluation - r = ast_mng.mk_iff(get_cached(c), get_cached(t)); + expr* c_expr = get_cached(c); + expr* t_expr = get_cached(t); + r = ast_mng.mk_iff(c_expr, t_expr); } else { - // TODO: non-deterministic parameter evaluation - r = ast_mng.mk_ite(get_cached(c), get_cached(t), get_cached(e)); + expr* c_expr = get_cached(c); + expr* t_expr = get_cached(t); + expr* e_expr = get_cached(e); + r = ast_mng.mk_ite(c_expr, t_expr, e_expr); } cache_result(n, r); TRACE(aig2expr, tout << "caching ITE/IFF "; m.display_ref(tout, n); tout << "\n";); @@ -1750,4 +1753,3 @@ unsigned aig_manager::get_num_aigs() const { } - diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp index a5c5186d1..660e92dd6 100644 --- a/src/tactic/arith/bv2real_rewriter.cpp +++ b/src/tactic/arith/bv2real_rewriter.cpp @@ -443,12 +443,14 @@ bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_re expr_ref gt_proxy(m().mk_not(le_proxy), m()); expr_ref s2_is_nonpos(m_bv.mk_sle(s2, m_bv.mk_numeral(rational(0), s2_size)), m()); - // TODO: non-deterministic parameter evaluation - expr_ref under(u().mk_bv_add(u().mk_bv_mul(rational(4), s1), u().mk_bv_mul(rational(5), s2)), m()); + expr_ref s1_scaled4(u().mk_bv_mul(rational(4), s1), m()); + expr_ref s2_scaled5(u().mk_bv_mul(rational(5), s2), m()); + expr_ref under(u().mk_bv_add(s1_scaled4, s2_scaled5), m()); expr_ref z1(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(under)), m()); expr_ref le_under(m_bv.mk_sle(under, z1), m()); - // TODO: non-deterministic parameter evaluation - expr_ref over(u().mk_bv_add(u().mk_bv_mul(rational(2), s1), u().mk_bv_mul(rational(3), s2)), m()); + expr_ref s1_scaled2(u().mk_bv_mul(rational(2), s1), m()); + expr_ref s2_scaled3(u().mk_bv_mul(rational(3), s2), m()); + expr_ref over(u().mk_bv_add(s1_scaled2, s2_scaled3), m()); expr_ref z2(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(over)), m()); expr_ref le_over(m_bv.mk_sle(over, z2), m()); @@ -464,11 +466,12 @@ bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_re // predicate may occur in negative polarity. if (is_neg) { // s1 + s2*sqrt(2) > 0 <== s2 > 0 & s1 + s2*(5/4) > 0; 4*s1 + 5*s2 > 0 - // TODO: non-deterministic parameter evaluation - expr* e3 = m().mk_implies(m().mk_and(gt_proxy, m().mk_not(s2_is_nonpos)), m().mk_not(le_under)); + expr* not_s2_nonpos = m().mk_not(s2_is_nonpos); + expr* not_le_under = m().mk_not(le_under); + expr* e3 = m().mk_implies(m().mk_and(gt_proxy, not_s2_nonpos), not_le_under); // s1 + s2*sqrt(2) > 0 <== s2 <= 0 & s1 + s2*(3/2) > 0 <=> 2*s1 + 3*s2 > 0 - // TODO: non-deterministic parameter evaluation - expr* e4 = m().mk_implies(m().mk_and(gt_proxy, s2_is_nonpos), m().mk_not(le_over)); + expr* not_le_over = m().mk_not(le_over); + expr* e4 = m().mk_implies(m().mk_and(gt_proxy, s2_is_nonpos), not_le_over); u().add_side_condition(e3); u().add_side_condition(e4); } @@ -547,11 +550,14 @@ br_status bv2real_rewriter::mk_le(expr * s, expr * t, expr_ref & result) { expr* ge = m_bv.mk_sle(t22, t12); expr* le = m_bv.mk_sle(t12, t22); expr* e1 = m().mk_or(gz1, gz2); - // TODO: non-deterministic parameter evaluation - expr* e2 = m().mk_or(m().mk_not(gz1), m().mk_not(lz2), ge); - // TODO: non-deterministic parameter evaluation - expr* e3 = m().mk_or(m().mk_not(gz2), m().mk_not(lz1), le); - result = m().mk_and(e1, e2, e3); + expr* not_gz1 = m().mk_not(gz1); + expr* not_lz2 = m().mk_not(lz2); + expr* e2 = m().mk_or(not_gz1, not_lz2, ge); + expr* not_gz2 = m().mk_not(gz2); + expr* not_lz1 = m().mk_not(lz1); + expr* e3 = m().mk_or(not_gz2, not_lz1, le); + expr* conjuncts[3] = { e1, e2, e3 }; + result = m().mk_and(3, conjuncts); TRACE(bv2real_rewriter, tout << "\n";); return BR_DONE; } @@ -593,8 +599,10 @@ br_status bv2real_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) { u().align_divisors(s1, s2, t1, t2, d1, d2); u().align_sizes(s1, t1); u().align_sizes(s2, t2); - // TODO: non-deterministic parameter evaluation - result = m().mk_and(m().mk_eq(s1, t1), m().mk_eq(s2, t2)); + expr* eq_s1_t1 = m().mk_eq(s1, t1); + expr* eq_s2_t2 = m().mk_eq(s2, t2); + expr* conjuncts[2] = { eq_s1_t1, eq_s2_t2 }; + result = m().mk_and(2, conjuncts); return BR_DONE; } return BR_FAILED; @@ -657,10 +665,13 @@ br_status bv2real_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) { if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) { // s1*t1 + r1*(s2*t2) + (s1*t2 + s2*t2)*r1 expr_ref u1(m()), u2(m()); - // TODO: non-deterministic parameter evaluation - u1 = u().mk_bv_add(u().mk_bv_mul(s1, t1), u().mk_bv_mul(r1, u().mk_bv_mul(t2, s2))); - // TODO: non-deterministic parameter evaluation - u2 = u().mk_bv_add(u().mk_bv_mul(s1, t2), u().mk_bv_mul(s2, t1)); + expr_ref s1_t1(u().mk_bv_mul(s1, t1), m()); + expr_ref t2_s2(u().mk_bv_mul(t2, s2), m()); + expr_ref r1_t2_s2(u().mk_bv_mul(r1, t2_s2), m()); + u1 = u().mk_bv_add(s1_t1, r1_t2_s2); + expr_ref s1_t2(u().mk_bv_mul(s1, t2), m()); + expr_ref s2_t1(u().mk_bv_mul(s2, t1), m()); + u2 = u().mk_bv_add(s1_t2, s2_t1); rational tmp = d1*d2; if (u().mk_bv2real(u1, u2, tmp, r1, result)) { return BR_DONE; @@ -709,4 +720,3 @@ br_status bv2real_elim_rewriter::mk_app_core(func_decl * f, unsigned num_args, e } template class rewriter_tpl; - diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index fdc254fcc..824fd0020 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -63,8 +63,9 @@ class factor_tactic : public tactic { m_expr2poly.to_expr(fs[i], true, arg); args.push_back(arg); } - // TODO: non-deterministic parameter evaluation - result = m.mk_eq(mk_mul(args.size(), args.data()), mk_zero_for(arg)); + expr* product = mk_mul(args.size(), args.data()); + expr* zero = mk_zero_for(arg); + result = m.mk_eq(product, zero); } // p1^k1 * p2^k2 = 0 --> p1 = 0 or p2 = 0 @@ -335,4 +336,3 @@ tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) { } - diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 42cd46b30..cefa5079c 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -260,8 +260,9 @@ public: return m_pb.mk_eq(sz, weights, args, w); } else { - // TODO: non-deterministic parameter evaluation - return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w)); + expr* ge_expr = mk_ge(sz, weights, args, w); + expr* le_expr = mk_le(sz, weights, args, w); + return m.mk_and(ge_expr, le_expr); } } diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 31a752b50..cb952f9af 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -623,9 +623,9 @@ private: if (is_uninterp_const(lhs) && is_uninterp_const(rhs)) { add_bounds_dependencies(lhs); add_bounds_dependencies(rhs); - // TODO: non-deterministic parameter evaluation - r = m.mk_iff(mon_lit2lit(lit(lhs, false)), - mon_lit2lit(lit(rhs, !pos))); + expr* lhs_lit = mon_lit2lit(lit(lhs, false)); + expr* rhs_lit = mon_lit2lit(lit(rhs, !pos)); + r = m.mk_iff(lhs_lit, rhs_lit); return; } k = EQ; @@ -808,8 +808,10 @@ private: for (unsigned i = 0; i < sz; i += 2) { app * x_i = to_app(m_p[i].m_lit.var()); app * y_i = to_app(m_p[i+1].m_lit.var()); - // TODO: non-deterministic parameter evaluation - eqs.push_back(m.mk_eq(int2lit(x_i), int2lit(y_i))); + expr_ref x_lit(int2lit(x_i), m); + expr_ref y_lit(int2lit(y_i), m); + expr_ref eq_expr(m.mk_eq(x_lit, y_lit), m); + eqs.push_back(eq_expr); } m_b_rw.mk_and(eqs.size(), eqs.data(), r); if (!pos) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 2a042bd26..fba8f5228 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -331,16 +331,30 @@ struct purify_arith_proc { expr * x = args[0]; expr * y = args[1]; // y = 0 \/ y*k = x - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(EQ(y, mk_real_zero()), - EQ(u().mk_mul(y, k), x))); + expr_ref y_is_zero(m()); + expr_ref mul_term(m()); + expr_ref mul_eq_x(m()); + expr_ref disj_y_zero_or_mul(m()); + expr_ref zero_val(m()); + zero_val = mk_real_zero(); + y_is_zero = EQ(y, zero_val); + mul_term = u().mk_mul(y, k); + mul_eq_x = EQ(mul_term, x); + disj_y_zero_or_mul = OR(y_is_zero, mul_eq_x); + push_cnstr(disj_y_zero_or_mul); push_cnstr_pr(result_pr); rational r; if (complete()) { // y != 0 \/ k = div-0(x) - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(NOT(EQ(y, mk_real_zero())), - EQ(k, u().mk_div(x, mk_real_zero())))); + expr_ref not_y_zero(m()); + expr_ref div_zero(m()); + expr_ref k_eq_div_zero(m()); + expr_ref disj_nonzero_or_def(m()); + not_y_zero = NOT(y_is_zero); + div_zero = u().mk_div(x, zero_val); + k_eq_div_zero = EQ(k, div_zero); + disj_nonzero_or_def = OR(not_y_zero, k_eq_div_zero); + push_cnstr(disj_nonzero_or_def); push_cnstr_pr(result_pr); } m_divs.push_back(bin_def(x, y, k)); @@ -377,27 +391,68 @@ struct purify_arith_proc { // y < 0 implies k2 < -y ---> y >= 0 \/ k2 < -y // expr * zero = mk_int_zero(); - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(EQ(y, zero), EQ(x, u().mk_add(u().mk_mul(k1, y), k2)))); + expr_ref y_eq_zero(m()); + expr_ref mul_k1_y(m()); + expr_ref sum_expr(m()); + expr_ref x_eq_sum(m()); + expr_ref or_y_zero_or_sum(m()); + y_eq_zero = EQ(y, zero); + mul_k1_y = u().mk_mul(k1, y); + sum_expr = u().mk_add(mul_k1_y, k2); + x_eq_sum = EQ(x, sum_expr); + or_y_zero_or_sum = OR(y_eq_zero, x_eq_sum); + push_cnstr(or_y_zero_or_sum); push_cnstr_pr(result_pr, mod_pr); - push_cnstr(OR(EQ(y, zero), u().mk_le(zero, k2))); + expr_ref zero_le_k2(m()); + expr_ref or_y_zero_or_le(m()); + zero_le_k2 = u().mk_le(zero, k2); + or_y_zero_or_le = OR(y_eq_zero, zero_le_k2); + push_cnstr(or_y_zero_or_le); push_cnstr_pr(mod_pr); - push_cnstr(OR(u().mk_le(y, zero), u().mk_lt(k2, y))); + expr_ref y_le_zero(m()); + expr_ref k2_lt_y(m()); + expr_ref or_y_le_or_lt(m()); + y_le_zero = u().mk_le(y, zero); + k2_lt_y = u().mk_lt(k2, y); + or_y_le_or_lt = OR(y_le_zero, k2_lt_y); + push_cnstr(or_y_le_or_lt); push_cnstr_pr(mod_pr); - push_cnstr(OR(u().mk_ge(y, zero), u().mk_lt(k2, u().mk_mul(u().mk_numeral(rational(-1), true), y)))); + expr_ref y_ge_zero(m()); + expr_ref neg_one(m()); + expr_ref neg_y(m()); + expr_ref k2_lt_neg_y(m()); + expr_ref or_y_ge_or_lt(m()); + y_ge_zero = u().mk_ge(y, zero); + neg_one = u().mk_numeral(rational(-1), true); + neg_y = u().mk_mul(neg_one, y); + k2_lt_neg_y = u().mk_lt(k2, neg_y); + or_y_ge_or_lt = OR(y_ge_zero, k2_lt_neg_y); + push_cnstr(or_y_ge_or_lt); push_cnstr_pr(mod_pr); rational r; if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero)))); + expr_ref not_y_zero(m()); + expr_ref idiv_zero(m()); + expr_ref k1_eq_idiv_zero(m()); + expr_ref or_nonzero_or_idiv(m()); + not_y_zero = NOT(y_eq_zero); + idiv_zero = u().mk_idiv(x, zero); + k1_eq_idiv_zero = EQ(k1, idiv_zero); + or_nonzero_or_idiv = OR(not_y_zero, k1_eq_idiv_zero); + push_cnstr(or_nonzero_or_idiv); push_cnstr_pr(result_pr); - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero)))); + expr_ref mod_zero(m()); + expr_ref k2_eq_mod_zero(m()); + expr_ref or_nonzero_or_mod(m()); + mod_zero = u().mk_mod(x, zero); + k2_eq_mod_zero = EQ(k2, mod_zero); + or_nonzero_or_mod = OR(not_y_zero, k2_eq_mod_zero); + push_cnstr(or_nonzero_or_mod); push_cnstr_pr(mod_pr); } m_idivs.push_back(bin_def(x, y, k1)); @@ -468,11 +523,21 @@ struct purify_arith_proc { } // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(EQ(x, zero), EQ(k, one))); + expr_ref x_eq_zero(m()); + expr_ref k_eq_one(m()); + expr_ref disj_zero_or_one(m()); + x_eq_zero = EQ(x, zero); + k_eq_one = EQ(k, one); + disj_zero_or_one = OR(x_eq_zero, k_eq_one); + push_cnstr(disj_zero_or_one); push_cnstr_pr(result_pr); - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, p0))); + expr_ref not_x_eq_zero(m()); + expr_ref k_eq_p0(m()); + expr_ref disj_nonzero_or_p0(m()); + not_x_eq_zero = NOT(x_eq_zero); + k_eq_p0 = EQ(k, p0); + disj_nonzero_or_p0 = OR(not_x_eq_zero, k_eq_p0); + push_cnstr(disj_nonzero_or_p0); push_cnstr_pr(result_pr); } else if (!is_int) { @@ -489,14 +554,30 @@ struct purify_arith_proc { SASSERT(n.is_even()); // (^ x (/ 1 n)) --> k | x >= 0 implies (x = k^n and k >= 0), x < 0 implies k = neg-root(x, n) // when n is even - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(NOT(u().mk_ge(x, zero)), - AND(EQ(x, u().mk_power(k, u().mk_numeral(n, false))), - u().mk_ge(k, zero)))); + expr_ref ge_x_zero(m()); + expr_ref not_ge_x_zero(m()); + expr_ref power_arg(m()); + expr_ref x_eq_power(m()); + expr_ref ge_k_zero(m()); + expr_ref conj_eq_and_ge(m()); + expr_ref disj_even_case(m()); + ge_x_zero = u().mk_ge(x, zero); + not_ge_x_zero = NOT(ge_x_zero); + power_arg = u().mk_numeral(n, false); + x_eq_power = EQ(x, u().mk_power(k, power_arg)); + ge_k_zero = u().mk_ge(k, zero); + conj_eq_and_ge = AND(x_eq_power, ge_k_zero); + disj_even_case = OR(not_ge_x_zero, conj_eq_and_ge); + push_cnstr(disj_even_case); push_cnstr_pr(result_pr); - push_cnstr(OR(u().mk_ge(x, zero), - EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false))))); + expr_ref neg_root_arg(m()); + expr_ref k_eq_neg_root(m()); + expr_ref or_ge_or_neg_root(m()); + neg_root_arg = u().mk_numeral(n, false); + k_eq_neg_root = EQ(k, u().mk_neg_root(x, neg_root_arg)); + or_ge_or_neg_root = OR(ge_x_zero, k_eq_neg_root); + push_cnstr(or_ge_or_neg_root); push_cnstr_pr(result_pr); } // else { @@ -608,23 +689,50 @@ struct purify_arith_proc { expr * pi2 = u().mk_mul(u().mk_numeral(rational(1,2), false), u().mk_pi()); expr * mpi2 = u().mk_mul(u().mk_numeral(rational(-1,2), false), u().mk_pi()); // -1 <= x <= 1 implies sin(k) = x, -pi/2 <= k <= pi/2 - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(OR(NOT(u().mk_ge(x, mone)), - NOT(u().mk_le(x, one))), - // TODO: non-deterministic parameter evaluation - AND(EQ(x, u().mk_sin(k)), - AND(u().mk_ge(k, mpi2), - u().mk_le(k, pi2))))); + expr_ref ge_x_mone(m()); + expr_ref le_x_one(m()); + expr_ref not_ge_x_mone(m()); + expr_ref not_le_x_one(m()); + expr_ref sin_k(m()); + expr_ref eq_x_sin(m()); + expr_ref ge_k_mpi2(m()); + expr_ref le_k_pi2(m()); + expr_ref bounds_conj(m()); + expr_ref sin_conj(m()); + expr_ref interval_disj(m()); + ge_x_mone = u().mk_ge(x, mone); + le_x_one = u().mk_le(x, one); + not_ge_x_mone = NOT(ge_x_mone); + not_le_x_one = NOT(le_x_one); + sin_k = u().mk_sin(k); + eq_x_sin = EQ(x, sin_k); + ge_k_mpi2 = u().mk_ge(k, mpi2); + le_k_pi2 = u().mk_le(k, pi2); + bounds_conj = AND(ge_k_mpi2, le_k_pi2); + sin_conj = AND(eq_x_sin, bounds_conj); + interval_disj = OR(OR(not_ge_x_mone, not_le_x_one), sin_conj); + push_cnstr(interval_disj); push_cnstr_pr(result_pr); if (complete()) { // x < -1 implies k = asin_u(x) // x > 1 implies k = asin_u(x) - push_cnstr(OR(u().mk_ge(x, mone), - EQ(k, u().mk_u_asin(x)))); + expr_ref ge_x_mone_guard(m()); + expr_ref asin_val(m()); + expr_ref k_eq_asin(m()); + expr_ref ge_guard_or_eq(m()); + ge_x_mone_guard = u().mk_ge(x, mone); + asin_val = u().mk_u_asin(x); + k_eq_asin = EQ(k, asin_val); + ge_guard_or_eq = OR(ge_x_mone_guard, k_eq_asin); + push_cnstr(ge_guard_or_eq); push_cnstr_pr(result_pr); - push_cnstr(OR(u().mk_le(x, one), - EQ(k, u().mk_u_asin(x)))); + expr_ref le_x_one_guard(m()); + expr_ref k_eq_asin_upper(m()); + expr_ref le_guard_or_eq(m()); + le_x_one_guard = u().mk_le(x, one); + k_eq_asin_upper = EQ(k, asin_val); + le_guard_or_eq = OR(le_x_one_guard, k_eq_asin_upper); + push_cnstr(le_guard_or_eq); push_cnstr_pr(result_pr); } return BR_DONE; @@ -653,23 +761,50 @@ struct purify_arith_proc { expr * pi = u().mk_pi(); expr * zero = u().mk_numeral(rational(0), false); // -1 <= x <= 1 implies cos(k) = x, 0 <= k <= pi - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - push_cnstr(OR(OR(NOT(u().mk_ge(x, mone)), - NOT(u().mk_le(x, one))), - // TODO: non-deterministic parameter evaluation - AND(EQ(x, u().mk_cos(k)), - AND(u().mk_ge(k, zero), - u().mk_le(k, pi))))); + expr_ref ge_x_mone(m()); + expr_ref le_x_one(m()); + expr_ref not_ge_x_mone(m()); + expr_ref not_le_x_one(m()); + expr_ref cos_k(m()); + expr_ref eq_x_cos(m()); + expr_ref ge_k_zero(m()); + expr_ref le_k_pi(m()); + expr_ref bounds_conj(m()); + expr_ref cos_conj(m()); + expr_ref interval_disj(m()); + ge_x_mone = u().mk_ge(x, mone); + le_x_one = u().mk_le(x, one); + not_ge_x_mone = NOT(ge_x_mone); + not_le_x_one = NOT(le_x_one); + cos_k = u().mk_cos(k); + eq_x_cos = EQ(x, cos_k); + ge_k_zero = u().mk_ge(k, zero); + le_k_pi = u().mk_le(k, pi); + bounds_conj = AND(ge_k_zero, le_k_pi); + cos_conj = AND(eq_x_cos, bounds_conj); + interval_disj = OR(OR(not_ge_x_mone, not_le_x_one), cos_conj); + push_cnstr(interval_disj); push_cnstr_pr(result_pr); if (complete()) { // x < -1 implies k = acos_u(x) // x > 1 implies k = acos_u(x) - push_cnstr(OR(u().mk_ge(x, mone), - EQ(k, u().mk_u_acos(x)))); + expr_ref ge_x_mone_guard(m()); + expr_ref acos_val(m()); + expr_ref k_eq_acos(m()); + expr_ref ge_guard_or_eq(m()); + ge_x_mone_guard = u().mk_ge(x, mone); + acos_val = u().mk_u_acos(x); + k_eq_acos = EQ(k, acos_val); + ge_guard_or_eq = OR(ge_x_mone_guard, k_eq_acos); + push_cnstr(ge_guard_or_eq); push_cnstr_pr(result_pr); - push_cnstr(OR(u().mk_le(x, one), - EQ(k, u().mk_u_acos(x)))); + expr_ref le_x_one_guard(m()); + expr_ref k_eq_acos_upper(m()); + expr_ref le_guard_or_eq(m()); + le_x_one_guard = u().mk_le(x, one); + k_eq_acos_upper = EQ(k, acos_val); + le_guard_or_eq = OR(le_x_one_guard, k_eq_acos_upper); + push_cnstr(le_guard_or_eq); push_cnstr_pr(result_pr); } return BR_DONE; @@ -692,10 +827,17 @@ struct purify_arith_proc { // tan(k) = x, -pi/2 < k < pi/2 expr * pi2 = u().mk_mul(u().mk_numeral(rational(1,2), false), u().mk_pi()); expr * mpi2 = u().mk_mul(u().mk_numeral(rational(-1,2), false), u().mk_pi()); - // TODO: non-deterministic parameter evaluation - push_cnstr(AND(EQ(x, u().mk_tan(k)), - AND(u().mk_gt(k, mpi2), - u().mk_lt(k, pi2)))); + expr_ref eq_x_tan(m()); + expr_ref gt_k_mpi2(m()); + expr_ref lt_k_pi2(m()); + expr_ref bounds_conj(m()); + expr_ref tan_conj(m()); + eq_x_tan = EQ(x, u().mk_tan(k)); + gt_k_mpi2 = u().mk_gt(k, mpi2); + lt_k_pi2 = u().mk_lt(k, pi2); + bounds_conj = AND(gt_k_mpi2, lt_k_pi2); + tan_conj = AND(eq_x_tan, bounds_conj); + push_cnstr(tan_conj); push_cnstr_pr(result_pr); return BR_DONE; } @@ -819,33 +961,51 @@ struct purify_arith_proc { auto const& p1 = divs[i]; for (unsigned j = i + 1; j < divs.size(); ++j) { auto const& p2 = divs[j]; - // TODO: non-deterministic parameter evaluation - m_goal.assert_expr(m().mk_implies( - // TODO: non-deterministic parameter evaluation - m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), - m().mk_eq(p1.d, p2.d))); + expr_ref eq_x(m()); + expr_ref eq_y(m()); + expr_ref antecedent(m()); + expr_ref consequent(m()); + expr_ref implication(m()); + eq_x = m().mk_eq(p1.x, p2.x); + eq_y = m().mk_eq(p1.y, p2.y); + antecedent = m().mk_and(eq_x, eq_y); + consequent = m().mk_eq(p1.d, p2.d); + implication = m().mk_implies(antecedent, consequent); + m_goal.assert_expr(implication); } } for (unsigned i = 0; i < mods.size(); ++i) { auto const& p1 = mods[i]; for (unsigned j = i + 1; j < mods.size(); ++j) { auto const& p2 = mods[j]; - // TODO: non-deterministic parameter evaluation - m_goal.assert_expr(m().mk_implies( - // TODO: non-deterministic parameter evaluation - m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), - m().mk_eq(p1.d, p2.d))); + expr_ref eq_x(m()); + expr_ref eq_y(m()); + expr_ref antecedent(m()); + expr_ref consequent(m()); + expr_ref implication(m()); + eq_x = m().mk_eq(p1.x, p2.x); + eq_y = m().mk_eq(p1.y, p2.y); + antecedent = m().mk_and(eq_x, eq_y); + consequent = m().mk_eq(p1.d, p2.d); + implication = m().mk_implies(antecedent, consequent); + m_goal.assert_expr(implication); } } for (unsigned i = 0; i < idivs.size(); ++i) { auto const& p1 = idivs[i]; for (unsigned j = i + 1; j < idivs.size(); ++j) { auto const& p2 = idivs[j]; - // TODO: non-deterministic parameter evaluation - m_goal.assert_expr(m().mk_implies( - // TODO: non-deterministic parameter evaluation - m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), - m().mk_eq(p1.d, p2.d))); + expr_ref eq_x(m()); + expr_ref eq_y(m()); + expr_ref antecedent(m()); + expr_ref consequent(m()); + expr_ref implication(m()); + eq_x = m().mk_eq(p1.x, p2.x); + eq_y = m().mk_eq(p1.y, p2.y); + antecedent = m().mk_and(eq_x, eq_y); + consequent = m().mk_eq(p1.d, p2.d); + implication = m().mk_implies(antecedent, consequent); + m_goal.assert_expr(implication); } } @@ -864,8 +1024,15 @@ struct purify_arith_proc { expr_ref v0(m().mk_var(0, u().mk_real()), m()); expr_ref v1(m().mk_var(1, u().mk_real()), m()); for (auto const& p : divs) { - // TODO: non-deterministic parameter evaluation - body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); + expr_ref eq_v0_x(m()); + expr_ref eq_v1_y(m()); + expr_ref guard(m()); + expr_ref new_body(m()); + eq_v0_x = m().mk_eq(v0, p.x); + eq_v1_y = m().mk_eq(v1, p.y); + guard = m().mk_and(eq_v0_x, eq_v1_y); + new_body = m().mk_ite(guard, p.d, body); + body = new_body; } fmc->add(u().mk_div0(), body); } @@ -874,8 +1041,15 @@ struct purify_arith_proc { expr_ref v0(m().mk_var(0, u().mk_int()), m()); expr_ref v1(m().mk_var(1, u().mk_int()), m()); for (auto const& p : mods) { - // TODO: non-deterministic parameter evaluation - body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); + expr_ref eq_v0_x(m()); + expr_ref eq_v1_y(m()); + expr_ref guard(m()); + expr_ref new_body(m()); + eq_v0_x = m().mk_eq(v0, p.x); + eq_v1_y = m().mk_eq(v1, p.y); + guard = m().mk_and(eq_v0_x, eq_v1_y); + new_body = m().mk_ite(guard, p.d, body); + body = new_body; } fmc->add(u().mk_mod0(), body); @@ -887,8 +1061,15 @@ struct purify_arith_proc { expr_ref v0(m().mk_var(0, u().mk_int()), m()); expr_ref v1(m().mk_var(1, u().mk_int()), m()); for (auto const& p : idivs) { - // TODO: non-deterministic parameter evaluation - body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); + expr_ref eq_v0_x(m()); + expr_ref eq_v1_y(m()); + expr_ref guard(m()); + expr_ref new_body(m()); + eq_v0_x = m().mk_eq(v0, p.x); + eq_v1_y = m().mk_eq(v1, p.y); + guard = m().mk_and(eq_v0_x, eq_v1_y); + new_body = m().mk_ite(guard, p.d, body); + body = new_body; } fmc->add(u().mk_idiv0(), body); } @@ -903,10 +1084,17 @@ struct purify_arith_proc { generic_model_converter* emc = alloc(generic_model_converter, m(), "purify_sin_cos"); mc = concat(mc.get(), emc); for (auto const& kv : m_sin_cos) { - emc->add(kv.m_key->get_decl(), - m().mk_ite(u().mk_ge(kv.m_value.first, mk_real_zero()), u().mk_acos(kv.m_value.second), - // TODO: non-deterministic parameter evaluation - u().mk_add(u().mk_acos(u().mk_uminus(kv.m_value.second)), u().mk_pi()))); + expr_ref ge_nonneg(m()); + expr_ref acos_val(m()); + expr_ref neg_acos_val(m()); + expr_ref pi_sum(m()); + expr_ref ite_expr(m()); + ge_nonneg = u().mk_ge(kv.m_value.first, mk_real_zero()); + acos_val = u().mk_acos(kv.m_value.second); + neg_acos_val = u().mk_acos(u().mk_uminus(kv.m_value.second)); + pi_sum = u().mk_add(neg_acos_val, u().mk_pi()); + ite_expr = m().mk_ite(ge_nonneg, acos_val, pi_sum); + emc->add(kv.m_key->get_decl(), ite_expr); } } diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 10540d33c..706b88dad 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -178,8 +178,9 @@ public: expr_ref head(m); ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); if (enums.size() > num.get_unsigned()) { - // TODO: non-deterministic parameter evaluation - head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); + expr_ref enum_const(m.mk_const(f), m); + expr_ref enum_value(m.mk_const(enums[num.get_unsigned()]), m); + head = m.mk_eq(enum_const, enum_value); consequences[i] = m.mk_implies(a, head); } } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 51cf93a6e..e068fa9ca 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -314,15 +314,18 @@ namespace smtfd { } family_id fid = a->get_family_id(); if (m.is_eq(a)) { - // TODO: non-deterministic parameter evaluation - r = m.mk_eq(m_args.get(0), m_args.get(1)); + expr* lhs = m_args.get(0); + expr* rhs = m_args.get(1); + r = m.mk_eq(lhs, rhs); } else if (m.is_distinct(a)) { r = m.mk_distinct(m_args.size(), m_args.data()); } else if (m.is_ite(a)) { - // TODO: non-deterministic parameter evaluation - r = m.mk_ite(m_args.get(0), m_args.get(1), m_args.get(2)); + expr* cond = m_args.get(0); + expr* then_branch = m_args.get(1); + expr* else_branch = m_args.get(2); + r = m.mk_ite(cond, then_branch, else_branch); } else if (bvfid == fid || bfid == fid || pbfid == fid) { r = m.mk_app(a->get_decl(), m_args.size(), m_args.data()); @@ -1159,8 +1162,9 @@ namespace smtfd { expr_ref a1(m_autil.mk_select(args), m); args[0] = b; expr_ref b1(m_autil.mk_select(args), m); - // TODO: non-deterministic parameter evaluation - expr_ref ext(m.mk_iff(m.mk_eq(a1, b1), m.mk_eq(a, b)), m); + expr* eq_ab = m.mk_eq(a, b); + expr* eq_select = m.mk_eq(a1, b1); + expr_ref ext(m.mk_iff(eq_select, eq_ab), m); if (!m.is_true(eval_abs(ext))) { TRACE(smtfd, tout << mk_bounded_pp(a, m, 2) << " " << mk_bounded_pp(b, m, 2) << "\n";); m_context.add(ext, __FUNCTION__); diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index dcea982ba..e1dd9d2b2 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -343,8 +343,8 @@ Notes: return mk_not(out[k]); } else { - // TODO: non-deterministic parameter evaluation - return mk_min(out[k-1], mk_not(out[k])); + literal not_out_k = mk_not(out[k]); + return mk_min(out[k-1], not_out_k); } case sorting_network_encoding::unate_at_most: return unate_eq(k, n, xs); @@ -385,8 +385,9 @@ Notes: } literal eq(unsigned k, unsigned n, unsigned const* ws, literal const* xs) { - // TODO: non-deterministic parameter evaluation - return mk_and(ge(k, n, ws, xs), le(k, n, ws, xs)); + literal ge_res = ge(k, n, ws, xs); + literal le_res = le(k, n, ws, xs); + return mk_and(ge_res, le_res); #if 0 m_t = EQ; return cmp(k, n, ws, xs); @@ -481,8 +482,8 @@ Notes: for (unsigned j = last; j-- > 0; ) { // c'[j] <-> (xs[i] & c[j-1]) | c[j] literal c0 = j > 0 ? carry[j-1] : ctx.mk_true(); - // TODO: non-deterministic parameter evaluation - carry[j] = mk_or(mk_and(xs[i], c0), carry[j]); + literal and_term = mk_and(xs[i], c0); + carry[j] = mk_or(and_term, carry[j]); } } switch (cmp) { @@ -493,8 +494,10 @@ Notes: case GE_FULL: return carry[k-1]; case EQ: - // TODO: non-deterministic parameter evaluation - return mk_and(mk_not(carry[k]), carry[k-1]); + { + literal not_carry_k = mk_not(carry[k]); + return mk_and(not_carry_k, carry[k-1]); + } default: UNREACHABLE(); return xs[0]; @@ -526,10 +529,12 @@ Notes: // out[i] = c + x[i] + y[i] // c' = c&x[i] | c&y[i] | x[i]&y[i]; literal_vector ors; - // TODO: non-deterministic parameter evaluation - ors.push_back(mk_and(c, mk_not(x[i]), mk_not(y[i]))); - ors.push_back(mk_and(x[i], mk_not(c), mk_not(y[i]))); - ors.push_back(mk_and(y[i], mk_not(c), mk_not(x[i]))); + literal not_x = mk_not(x[i]); + literal not_y = mk_not(y[i]); + literal not_c = mk_not(c); + ors.push_back(mk_and(c, not_x, not_y)); + ors.push_back(mk_and(x[i], not_c, not_y)); + ors.push_back(mk_and(y[i], not_c, not_x)); ors.push_back(mk_and(c, x[i], y[i])); literal o = mk_or(4, ors.data()); out.push_back(o); @@ -583,10 +588,12 @@ Notes: literal_vector eqs; SASSERT(kvec.size() == out.size()); for (unsigned i = 0; i < num_bits; ++i) { - // TODO: non-deterministic parameter evaluation - eqs.push_back(mk_or(mk_not(kvec[i]), out[i])); - // TODO: non-deterministic parameter evaluation - eqs.push_back(mk_or(kvec[i], mk_not(out[i]))); + literal not_k = mk_not(kvec[i]); + literal clause1 = mk_or(not_k, out[i]); + literal not_out = mk_not(out[i]); + literal clause2 = mk_or(kvec[i], not_out); + eqs.push_back(clause1); + eqs.push_back(clause2); } eqs.push_back(mk_not(ovfl)); return mk_and(eqs); @@ -601,8 +608,13 @@ Notes: literal r = ctx.mk_true(); literal g = ctx.mk_false(); for (unsigned j = x.size(); j-- > 0; ) { - g = mk_or(g, mk_and(r, mk_and(x[j], mk_not(y[j])))); - r = mk_or(g, mk_and(r, mk_or( x[j], mk_not(y[j])))); + literal not_y = mk_not(y[j]); + literal and_x_not_y = mk_and(x[j], not_y); + literal and_r_x = mk_and(r, and_x_not_y); + g = mk_or(g, and_r_x); + literal or_x_not_y = mk_or(x[j], not_y); + literal and_r_or = mk_and(r, or_x_not_y); + r = mk_or(g, and_r_or); } return r; } @@ -693,8 +705,10 @@ Notes: case 1: return ands[0]; case 2: - // TODO: non-deterministic parameter evaluation - return mk_min(ands[0], ands[1]); + { + literal min_ab = mk_min(ands[0], ands[1]); + return min_ab; + } default: { return ctx.mk_min(ands.size(), ands.data()); } @@ -1505,4 +1519,3 @@ Notes: } } }; -