From b67ee8cdebca67f9054498118208a4b4a3099ae7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 29 Oct 2025 06:57:25 -0700 Subject: [PATCH] another batch of nond args fixes Signed-off-by: Lev Nachmanson --- src/ast/char_decl_plugin.cpp | 8 ++--- .../converters/generic_model_converter.cpp | 8 +++-- src/ast/normal_forms/defined_names.cpp | 19 ++++++++--- src/ast/normal_forms/pull_quant.cpp | 8 ++--- src/ast/rewriter/factor_equivs.cpp | 7 ++-- src/ast/rewriter/factor_rewriter.cpp | 14 +++++--- src/ast/rewriter/maximize_ac_sharing.cpp | 12 ++++--- src/ast/rewriter/rewriter_def.h | 9 +++--- src/ast/rewriter/seq_eq_solver.cpp | 7 ++-- src/ast/sls/sls_seq_plugin.cpp | 11 +++++-- src/smt/seq_regex.cpp | 9 ++++-- src/smt/theory_datatype.cpp | 7 ++-- src/smt/theory_dl.cpp | 6 ++-- src/tactic/bv/bv1_blaster_tactic.cpp | 21 ++++++++---- src/tactic/bv/bvarray2uf_rewriter.cpp | 32 +++++++++++++------ 15 files changed, 123 insertions(+), 55 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 6c65c19b7..19207ea69 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -66,8 +66,8 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, msg << "incorrect number of arguments passed. Expected one character, received " << arity; else { arith_util a(m); - // TODO: non-deterministic parameter evaluation - return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr)); + sort* int_sort = a.mk_int(); + return m.mk_func_decl(symbol("char.to_int"), arity, domain, int_sort, func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); case OP_CHAR_TO_BV: @@ -80,8 +80,8 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, else { bv_util b(m); unsigned sz = num_bits(); - // TODO: non-deterministic parameter evaluation - return m.mk_func_decl(symbol("char.to_bv"), arity, domain, b.mk_sort(sz), func_decl_info(m_family_id, k, 0, nullptr)); + sort* bv_sort = b.mk_sort(sz); + return m.mk_func_decl(symbol("char.to_bv"), arity, domain, bv_sort, func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); case OP_CHAR_FROM_BV: { diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp index 4de5183c4..a8027d93c 100644 --- a/src/ast/converters/generic_model_converter.cpp +++ b/src/ast/converters/generic_model_converter.cpp @@ -262,8 +262,12 @@ expr_ref generic_model_converter::simplify_def(entry const& e) { rep.apply_substitution(c, m.mk_true(), result1); rep.apply_substitution(c, m.mk_false(), result2); th_rewriter rw(m); - // TODO: non-deterministic parameter evaluation - expr_ref result(m.mk_and(m.mk_implies(result2, c), m.mk_implies(c, result1)), m); + expr_ref impl1(m); + expr_ref impl2(m); + expr_ref result(m); + impl1 = m.mk_implies(result2, c); + impl2 = m.mk_implies(c, result1); + result = m.mk_and(impl1, impl2); rw(result); return result; } diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index f45bfcb46..464fd4d47 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -191,9 +191,21 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var bound_vars(var_sorts, var_names, MK_OR(n, MK_NOT(e)), n, defs); } else if (m.is_term_ite(e)) { - // TODO: non-deterministic parameter evaluation - bound_vars(var_sorts, var_names, MK_OR(MK_NOT(to_app(e)->get_arg(0)), MK_EQ(n, to_app(e)->get_arg(1))), n, defs); - bound_vars(var_sorts, var_names, MK_OR(to_app(e)->get_arg(0), MK_EQ(n, to_app(e)->get_arg(2))), n, defs); + expr* cond = to_app(e)->get_arg(0); + expr* then_branch = to_app(e)->get_arg(1); + expr* else_branch = to_app(e)->get_arg(2); + expr_ref not_cond(m); + expr_ref eq_then(m); + expr_ref eq_else(m); + expr_ref disj1(m); + expr_ref disj2(m); + not_cond = m.mk_not(cond); + eq_then = m.mk_eq(n, then_branch); + eq_else = m.mk_eq(n, else_branch); + disj1 = m.mk_or(not_cond, eq_then); + disj2 = m.mk_or(cond, eq_else); + bound_vars(var_sorts, var_names, disj1, n, defs); + bound_vars(var_sorts, var_names, disj2, n, defs); } else if (is_lambda(e)) { // n(y) = \x . M[x,y] @@ -373,4 +385,3 @@ func_decl * defined_names::get_name_decl(unsigned i) const { - diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index 98e7922da..0520d3f60 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -265,9 +265,10 @@ struct pull_quant::imp { return BR_FAILED; if (m.proofs_enabled()) { - // TODO: non-deterministic parameter evaluation - result_pr = m.mk_pull_quant(m.mk_app(f, num, args), - to_quantifier(result.get())); + expr_ref f_app(m); + f_app = m.mk_app(f, num, args); + quantifier* q = to_quantifier(result.get()); + result_pr = m.mk_pull_quant(f_app, q); } return BR_DONE; } @@ -393,4 +394,3 @@ void pull_nested_quant::reset() { m_imp->m_rw.reset(); } - diff --git a/src/ast/rewriter/factor_equivs.cpp b/src/ast/rewriter/factor_equivs.cpp index d8938d659..a39987cc5 100644 --- a/src/ast/rewriter/factor_equivs.cpp +++ b/src/ast/rewriter/factor_equivs.cpp @@ -136,8 +136,11 @@ bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) { for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) { expr_equiv_class::iterator b(a); for (++b; b != end; ++b) { - // TODO: non-deterministic parameter evaluation - out.push_back(m.mk_eq(*a, *b)); + expr* lhs = *a; + expr* rhs = *b; + expr_ref eq(m); + eq = m.mk_eq(lhs, rhs); + out.push_back(eq); dirty = true; } } diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp index bf9e5d024..f0c36e833 100644 --- a/src/ast/rewriter/factor_rewriter.cpp +++ b/src/ast/rewriter/factor_rewriter.cpp @@ -141,10 +141,16 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) { pos0 = pos; } else { - // TODO: non-deterministic parameter evaluation - tmp = m().mk_or(m().mk_and(pos, pos0), m().mk_and(neg, neg0)); - // TODO: non-deterministic parameter evaluation - neg0 = m().mk_or(m().mk_and(neg, pos0), m().mk_and(pos, neg0)); + expr_ref pos_and_pos0(m()); + expr_ref neg_and_neg0(m()); + expr_ref neg_and_pos0(m()); + expr_ref pos_and_neg0(m()); + pos_and_pos0 = m().mk_and(pos, pos0); + neg_and_neg0 = m().mk_and(neg, neg0); + tmp = m().mk_or(pos_and_pos0, neg_and_neg0); + neg_and_pos0 = m().mk_and(neg, pos0); + pos_and_neg0 = m().mk_and(pos, neg0); + neg0 = m().mk_or(neg_and_pos0, pos_and_neg0); pos0 = tmp; } } diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp index 94b4d18f0..14a505fd3 100644 --- a/src/ast/rewriter/maximize_ac_sharing.cpp +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -58,8 +58,10 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr for (unsigned j = i + 1; j < num_args; j++) { if (contains(f, _args[i], _args[j])) { TRACE(ac_sharing_detail, tout << "reusing args: " << i << " " << j << "\n";); - // TODO: non-deterministic parameter evaluation - _args[i] = m.mk_app(f, _args[i], _args[j]); + expr* lhs = _args[i]; + expr* rhs = _args[j]; + expr* combined = m.mk_app(f, lhs, rhs); + _args[i] = combined; SASSERT(num_args > 1); for (unsigned w = j; w + 1 < num_args; w++) { _args[w] = _args[w+1]; @@ -82,8 +84,10 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr } else { insert(f, _args[i], _args[i+1]); - // TODO: non-deterministic parameter evaluation - _args[j] = m.mk_app(f, _args[i], _args[i+1]); + expr* lhs = _args[i]; + expr* rhs = _args[i+1]; + expr* combined = m.mk_app(f, lhs, rhs); + _args[j] = combined; } } num_args = j; diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index c59ac94a2..958cc6075 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -574,8 +574,9 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { num_no_pats = j; } if (ProofGen) { - // TODO: non-deterministic parameter evaluation - quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body), m()); + quantifier_ref new_q(m()); + quantifier* updated_q = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body); + new_q = updated_q; m_pr = nullptr; if (q != new_q) { m_pr = result_pr_stack().get(fr.m_spos); @@ -600,8 +601,8 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { TRACE(reduce_quantifier_bug, tout << mk_ismt2_pp(q, m()) << " " << mk_ismt2_pp(new_body, m()) << "\n";); if (!m_cfg.reduce_quantifier(q, new_body, new_pats.data(), new_no_pats.data(), m_r, m_pr)) { if (fr.m_new_child) { - // TODO: non-deterministic parameter evaluation - m_r = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body); + quantifier* updated_q = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body); + m_r = updated_q; } else { TRACE(rewriter_reuse, tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";); diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp index ff4cd59c3..04d90a853 100644 --- a/src/ast/rewriter/seq_eq_solver.cpp +++ b/src/ast/rewriter/seq_eq_solver.cpp @@ -344,8 +344,10 @@ namespace seq { if (ctx.expr2rep(xs[0]) == ctx.expr2rep(ys[0])) return false; - // TODO: non-deterministic parameter evaluation - expr_ref eq(m.mk_eq(xs[0], ys[0]), m); + expr* lhs = xs[0]; + expr* rhs = ys[0]; + expr_ref eq(m); + eq = m.mk_eq(lhs, rhs); expr* veq = ctx.expr2rep(eq); if (m.is_true(veq)) return false; @@ -730,4 +732,3 @@ namespace seq { }; - diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 1f6d737c6..8d0e61e79 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -161,8 +161,15 @@ namespace sls { if (r == 0 || sx.length() == 0) // create lemma: len(x) = 0 <=> x = "" - // TODO: non-deterministic parameter evaluation - ctx.add_constraint(m.mk_eq(m.mk_eq(e, a.mk_int(0)), m.mk_eq(x, seq.str.mk_string("")))); + { + expr_ref len_zero(m); + expr_ref eq_empty(m); + expr_ref bicond(m); + len_zero = m.mk_eq(e, a.mk_int(0)); + eq_empty = m.mk_eq(x, seq.str.mk_string("")); + bicond = m.mk_eq(len_zero, eq_empty); + ctx.add_constraint(bicond); + } if (ctx.rand(2) == 0 && update(e, rational(sx.length()))) return false; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 4b7f4737a..0b84fe28d 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -396,8 +396,13 @@ namespace smt { else if (re().is_empty(r2)) r = r1; else - // TODO: non-deterministic parameter evaluation - r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1)); + { + expr_ref diff12(m); + expr_ref diff21(m); + diff12 = re().mk_diff(r1, r2); + diff21 = re().mk_diff(r2, r1); + r = re().mk_union(diff12, diff21); + } rewrite(r); return r; } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 0aace16df..7391e0503 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -247,8 +247,11 @@ namespace smt { assert_eq_axiom(arg, acc_own, is_con); } // update_field is identity if 'n' is not created by a matching constructor. - // TODO: non-deterministic parameter evaluation - app_ref imp(m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_expr(), arg1)), m); + expr_ref not_rec(m); + not_rec = m.mk_not(rec_app); + expr_ref eq_expr(m); + eq_expr = m.mk_eq(n->get_expr(), arg1); + app_ref imp(m.mk_implies(not_rec, eq_expr), m); assert_eq_axiom(n, arg1, ~is_con); app_ref n_is_con(m.mk_app(rec, own), m); diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 2b68ca785..bb6f96641 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -252,8 +252,10 @@ namespace smt { get_rep(s, r, v); app_ref lt(m()), le(m()); lt = u().mk_lt(x,y); - // TODO: non-deterministic parameter evaluation - le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x)); + app_ref ry(m()), rx(m()); + ry = m().mk_app(r, y); + rx = m().mk_app(r, x); + le = b().mk_ule(ry, rx); if (m().has_trace_stream()) { app_ref body(m()); body = m().mk_eq(lt, le); diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 217d373a9..3f10037dd 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -142,8 +142,10 @@ class bv1_blaster_tactic : public tactic { unsigned i = bits1.size(); while (i > 0) { --i; - // TODO: non-deterministic parameter evaluation - new_eqs.push_back(m().mk_eq(bits1[i], bits2[i])); + expr* lhs = bits1[i]; + expr* rhs = bits2[i]; + expr* eq = m().mk_eq(lhs, rhs); + new_eqs.push_back(eq); } result = mk_and(m(), new_eqs.size(), new_eqs.data()); } @@ -157,8 +159,12 @@ class bv1_blaster_tactic : public tactic { bit_buffer new_ites; unsigned num = t_bits.size(); for (unsigned i = 0; i < num; i++) - // TODO: non-deterministic parameter evaluation - new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i])); + { + expr* t_bit = t_bits[i]; + expr* e_bit = e_bits[i]; + expr* ite = t_bit == e_bit ? t_bit : m().mk_ite(c, t_bit, e_bit); + new_ites.push_back(ite); + } result = butil().mk_concat(new_ites.size(), new_ites.data()); } @@ -218,8 +224,11 @@ class bv1_blaster_tactic : public tactic { bit_buffer new_bits; unsigned num = bits1.size(); for (unsigned i = 0; i < num; i++) { - // TODO: non-deterministic parameter evaluation - new_bits.push_back(m().mk_ite(m().mk_eq(bits1[i], bits2[i]), m_bit0, m_bit1)); + expr* bit1 = bits1[i]; + expr* bit2 = bits2[i]; + expr* eq_bits = m().mk_eq(bit1, bit2); + expr* ite = m().mk_ite(eq_bits, m_bit0, m_bit1); + new_bits.push_back(ite); } result = butil().mk_concat(new_bits.size(), new_bits.data()); } diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 371df1d67..e68de6b67 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -149,8 +149,12 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); expr_ref body(m_manager); - // TODO: non-deterministic parameter evaluation - body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get())); + expr* x_arg = x.get(); + app_ref ft_app(m_manager); + app_ref fs_app(m_manager); + ft_app = m_manager.mk_app(f_t, x_arg); + fs_app = m_manager.mk_app(f_s, x_arg); + body = m_manager.mk_eq(ft_app, fs_app); result = m_manager.mk_forall(1, sorts, names, body); res = BR_DONE; @@ -296,9 +300,12 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr new_args.push_back(m_manager.mk_app(ss[i].get(), x.get())); expr_ref body(m_manager); - // TODO: non-deterministic parameter evaluation - body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), - m_manager.mk_app(map_f, num, new_args.data())); + expr* x_arg = x.get(); + app_ref ft_app(m_manager); + ft_app = m_manager.mk_app(f_t, x_arg); + app_ref map_app(m_manager); + map_app = m_manager.mk_app(map_f, num, new_args.data()); + body = m_manager.mk_eq(ft_app, map_app); expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); extra_assertions.push_back(frllx); @@ -332,11 +339,16 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); expr_ref body(m_manager); - // TODO: non-deterministic parameter evaluation - body = m_manager.mk_or(m_manager.mk_eq(x, i), - // TODO: non-deterministic parameter evaluation - m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), - m_manager.mk_app(f_s, x.get()))); + expr_ref eq_x_i(m_manager); + eq_x_i = m_manager.mk_eq(x, i); + expr* x_arg = x.get(); + app_ref ft_app(m_manager); + app_ref fs_app(m_manager); + ft_app = m_manager.mk_app(f_t, x_arg); + fs_app = m_manager.mk_app(f_s, x_arg); + expr_ref funcs_eq(m_manager); + funcs_eq = m_manager.mk_eq(ft_app, fs_app); + body = m_manager.mk_or(eq_x_i, funcs_eq); expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); extra_assertions.push_back(frllx);