From 7dae39c24b1c933f16bb2262a00b2905c9688324 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 29 Oct 2025 07:46:55 -0700 Subject: [PATCH] another batch of nond args fixes Signed-off-by: Lev Nachmanson --- src/ast/rewriter/arith_rewriter.cpp | 109 +++++++++++++++------ src/ast/rewriter/poly_rewriter_def.h | 12 ++- src/muz/rel/dl_base.cpp | 5 +- src/muz/rel/dl_bound_relation.cpp | 16 +-- src/muz/rel/dl_finite_product_relation.cpp | 5 +- src/muz/rel/dl_interval_relation.cpp | 7 +- src/muz/spacer/spacer_convex_closure.cpp | 6 +- src/muz/spacer/spacer_generalizers.cpp | 6 +- src/sat/smt/arith_axioms.cpp | 28 +++--- src/sat/smt/q_solver.cpp | 5 +- src/sat/tactic/sat2goal.cpp | 5 +- 11 files changed, 134 insertions(+), 70 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index e44ab73ad..7daceeca8 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -622,18 +622,41 @@ br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind return BR_FAILED; expr_ref f2 = remove_factor(f, arg1); expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1)); - // TODO: non-deterministic parameter evaluation - result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z)); + expr_ref eq_f(m); + expr_ref eq_f2(m); + expr_ref disj(m); + eq_f = m_util.mk_eq(f, z); + eq_f2 = m_util.mk_eq(f2, z); + disj = m.mk_or(eq_f, eq_f2); switch (kind) { case EQ: + result = disj; break; case GE: - result = m.mk_or(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)), result); + { + expr_ref ge_f(m); + expr_ref ge_f2(m); + expr_ref iff(m); + ge_f = m_util.mk_ge(f, z); + ge_f2 = m_util.mk_ge(f2, z); + iff = m.mk_iff(ge_f, ge_f2); + result = m.mk_or(iff, disj); break; + } case LE: - result = m.mk_or(m.mk_not(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z))), result); + { + expr_ref ge_f(m); + expr_ref ge_f2(m); + expr_ref iff(m); + expr_ref not_iff(m); + ge_f = m_util.mk_ge(f, z); + ge_f2 = m_util.mk_ge(f2, z); + iff = m.mk_iff(ge_f, ge_f2); + not_iff = m.mk_not(iff); + result = m.mk_or(not_iff, disj); break; } + } return BR_REWRITE3; } return BR_FAILED; @@ -869,9 +892,13 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) { rational g = gcd(p, k, a, b); if (g == 1) { expr_ref nb(m_util.mk_numeral(b, true), m); - // TODO: non-deterministic parameter evaluation - result = m.mk_eq(m_util.mk_mod(u, y), - m_util.mk_mod(m_util.mk_mul(nb, arg2), y)); + expr_ref lhs(m); + expr_ref rhs_mul(m); + expr_ref rhs(m); + lhs = m_util.mk_mod(u, y); + rhs_mul = m_util.mk_mul(nb, arg2); + rhs = m_util.mk_mod(rhs_mul, y); + result = m.mk_eq(lhs, rhs); return true; } } @@ -1204,8 +1231,11 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul } br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) { - // TODO: non-deterministic parameter evaluation - result = m.mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0)); + expr_ref modulus(m); + expr_ref zero(m); + modulus = m_util.mk_mod(arg, m_util.mk_int(k)); + zero = m_util.mk_int(0); + result = m.mk_eq(modulus, zero); return BR_REWRITE2; } @@ -1232,8 +1262,13 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu } if (arg1 == arg2) { expr_ref zero(m_util.mk_int(0), m); - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); + expr_ref condition(m); + expr_ref idiv_zero(m); + expr_ref one(m); + condition = m.mk_eq(arg1, zero); + idiv_zero = m_util.mk_idiv(zero, zero); + one = m_util.mk_int(1); + result = m.mk_ite(condition, idiv_zero, one); return BR_REWRITE3; } if (is_num2 && v2.is_pos() && m_util.is_add(arg1)) { @@ -1331,14 +1366,18 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.data()); expr_ref d(m_util.mk_idiv(num, den), m); expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m); - // TODO: non-deterministic parameter evaluation - return expr_ref(m.mk_ite(m.mk_eq(zero, arg), - m_util.mk_idiv(zero, zero), - m.mk_ite(m_util.mk_ge(arg, zero), - d, - nd)), - m); -} + expr_ref cond_zero(m); + expr_ref cond_ge(m); + expr_ref zero_div(m); + expr_ref inner(m); + expr_ref outer(m); + cond_zero = m.mk_eq(zero, arg); + cond_ge = m_util.mk_ge(arg, zero); + zero_div = m_util.mk_idiv(zero, zero); + inner = m.mk_ite(cond_ge, d, nd); + outer = m.mk_ite(cond_zero, zero_div, inner); + return expr_ref(outer, m); +} void arith_rewriter::flat_mul(expr* e, ptr_buffer& args) { args.push_back(e); @@ -1432,8 +1471,11 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul expr* x = nullptr, * y = nullptr, * z = nullptr; if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) { - // TODO: non-deterministic parameter evaluation - result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1))); + expr_ref coeff(m); + expr_ref modulus(m); + coeff = m_util.mk_int(v1); + modulus = m_util.mk_mod(y, m_util.mk_int(v2 / v1)); + result = m_util.mk_mul(coeff, modulus); return BR_REWRITE1; } @@ -2083,21 +2125,29 @@ expr * arith_rewriter::mk_sin_value(rational const & k) { if (k_prime == rational(1, 3) || k_prime == rational(2, 3)) { // sin(pi/3) == sin(2/3 pi) == Sqrt(3)/2 // sin(4/3 pi) == sin(5/3 pi) == - Sqrt(3)/2 - expr * result = m_util.mk_div(mk_sqrt(rational(3)), m_util.mk_numeral(rational(2), false)); + expr_ref numerator(mk_sqrt(rational(3)), m); + expr_ref denom(m_util.mk_numeral(rational(2), false), m); + expr * result = m_util.mk_div(numerator, denom); return neg ? m_util.mk_uminus(result) : result; } if (k_prime == rational(1, 12) || k_prime == rational(11, 12)) { // sin(1/12 pi) == sin(11/12 pi) == [sqrt(6) - sqrt(2)]/4 // sin(13/12 pi) == sin(23/12 pi) == -[sqrt(6) - sqrt(2)]/4 - // TODO: non-deterministic parameter evaluation - expr * result = m_util.mk_div(m_util.mk_sub(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false)); + expr_ref sqrt6(mk_sqrt(rational(6)), m); + expr_ref sqrt2(mk_sqrt(rational(2)), m); + expr_ref diff(m_util.mk_sub(sqrt6, sqrt2), m); + expr_ref denom(m_util.mk_numeral(rational(4), false), m); + expr * result = m_util.mk_div(diff, denom); return neg ? m_util.mk_uminus(result) : result; } if (k_prime == rational(5, 12) || k_prime == rational(7, 12)) { // sin(5/12 pi) == sin(7/12 pi) == [sqrt(6) + sqrt(2)]/4 // sin(17/12 pi) == sin(19/12 pi) == -[sqrt(6) + sqrt(2)]/4 - // TODO: non-deterministic parameter evaluation - expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false)); + expr_ref sqrt6(mk_sqrt(rational(6)), m); + expr_ref sqrt2(mk_sqrt(rational(2)), m); + expr_ref sum(m_util.mk_add(sqrt6, sqrt2), m); + expr_ref denom(m_util.mk_numeral(rational(4), false), m); + expr * result = m_util.mk_div(sum, denom); return neg ? m_util.mk_uminus(result) : result; } return nullptr; @@ -2273,10 +2323,11 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) { return BR_REWRITE2; } - end: +end: if (m_expand_tan) { - // TODO: non-deterministic parameter evaluation - result = m_util.mk_div(m_util.mk_sin(arg), m_util.mk_cos(arg)); + expr* num = m_util.mk_sin(arg); + expr* den = m_util.mk_cos(arg); + result = m_util.mk_div(num, den); return BR_REWRITE2; } return BR_FAILED; diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index d8f336d9f..368cd0a6d 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -923,9 +923,10 @@ bool poly_rewriter::hoist_multiplication(expr_ref& som) { } if (mul_map.find(e, j) && valid[j] && j != k) { m_curr_sort = adds[k]->get_sort(); - // TODO: non-deterministic parameter evaluation - adds[j] = merge_muls(adds[j], adds[k]); - adds[k] = mk_numeral(rational(0)); + expr* merged = merge_muls(adds[j], adds[k]); + expr* zero_expr = mk_numeral(rational(0)); + adds[j] = merged; + adds[k] = zero_expr; valid[j] = false; valid[k] = false; change = true; @@ -1066,8 +1067,9 @@ template expr* poly_rewriter::apply_hoist(expr* a, numeral const& g, obj_hashtable const& shared) { expr* c = nullptr, *t = nullptr, *e = nullptr; if (M().is_ite(a, c, t, e)) { - // TODO: non-deterministic parameter evaluation - return M().mk_ite(c, apply_hoist(t, g, shared), apply_hoist(e, g, shared)); + expr* then_branch = apply_hoist(t, g, shared); + expr* else_branch = apply_hoist(e, g, shared); + return M().mk_ite(c, then_branch, else_branch); } rational k; if (is_nontrivial_gcd(g) && is_int_numeral(a, k)) { diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index b2414b06c..f5a3725ad 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -454,8 +454,9 @@ namespace datalog { r.get_fact(fact); conjs.reset(); for (unsigned i = 0; i < fact.size(); ++i) { - // TODO: non-deterministic parameter evaluation - conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i]))); + expr_ref lhs(m.mk_var(i, sig[i]), m); + expr_ref rhs(util.mk_numeral(fact[i], sig[i]), m); + conjs.push_back(m.mk_eq(lhs, rhs)); } brw.mk_and(conjs.size(), conjs.data(), fml); disjs.push_back(fml); diff --git a/src/muz/rel/dl_bound_relation.cpp b/src/muz/rel/dl_bound_relation.cpp index 52e16dd47..fc1e7b1de 100644 --- a/src/muz/rel/dl_bound_relation.cpp +++ b/src/muz/rel/dl_bound_relation.cpp @@ -658,20 +658,23 @@ namespace datalog { relation_signature const& sig = get_signature(); for (unsigned i = 0; i < sig.size(); ++i) { if (i != find(i)) { - // TODO: non-deterministic parameter evaluation - conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), m.mk_var(find(i), sig[find(i)]))); + expr_ref lhs(m.mk_var(i, sig[i]), m); + expr_ref rhs(m.mk_var(find(i), sig[find(i)]), m); + conjs.push_back(m.mk_eq(lhs, rhs)); continue; } uint_set2 const& upper = (*this)[i]; uint_set::iterator it = upper.lt.begin(), end = upper.lt.end(); for (; it != end; ++it) { - // TODO: non-deterministic parameter evaluation - conjs.push_back(arith.mk_lt(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it]))); + expr_ref lhs(m.mk_var(i, sig[i]), m); + expr_ref rhs(m.mk_var(*it, sig[*it]), m); + conjs.push_back(arith.mk_lt(lhs, rhs)); } it = upper.le.begin(), end = upper.le.end(); for (; it != end; ++it) { - // TODO: non-deterministic parameter evaluation - conjs.push_back(arith.mk_le(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it]))); + expr_ref lhs(m.mk_var(i, sig[i]), m); + expr_ref rhs(m.mk_var(*it, sig[*it]), m); + conjs.push_back(arith.mk_le(lhs, rhs)); } } bsimp.mk_and(conjs.size(), conjs.data(), fml); @@ -707,4 +710,3 @@ namespace datalog { }; - diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 5cb86dbf4..613f71bf4 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -2363,8 +2363,9 @@ namespace datalog { unsigned rel_idx = static_cast(fact[fact_sz-1]); m_others[rel_idx]->to_formula(tmp); for (unsigned i = 0; i + 1 < fact_sz; ++i) { - // TODO: non-deterministic parameter evaluation - conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i]))); + expr_ref lhs(m.mk_var(i, sig[i]), m); + expr_ref rhs(util.mk_numeral(fact[i], sig[i]), m); + conjs.push_back(m.mk_eq(lhs, rhs)); } sh(tmp, fact_sz-1, tmp); conjs.push_back(tmp); diff --git a/src/muz/rel/dl_interval_relation.cpp b/src/muz/rel/dl_interval_relation.cpp index a44195bb8..b49170d49 100644 --- a/src/muz/rel/dl_interval_relation.cpp +++ b/src/muz/rel/dl_interval_relation.cpp @@ -375,9 +375,9 @@ namespace datalog { relation_signature const& sig = get_signature(); for (unsigned i = 0; i < sig.size(); ++i) { if (i != find(i)) { - // TODO: non-deterministic parameter evaluation - conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), - m.mk_var(find(i), sig[find(i)]))); + expr_ref lhs(m.mk_var(i, sig[i]), m); + expr_ref rhs(m.mk_var(find(i), sig[find(i)]), m); + conjs.push_back(m.mk_eq(lhs, rhs)); continue; } interval const& iv = (*this)[i]; @@ -650,4 +650,3 @@ namespace datalog { } }; - diff --git a/src/muz/spacer/spacer_convex_closure.cpp b/src/muz/spacer/spacer_convex_closure.cpp index 224b6e584..08a276088 100644 --- a/src/muz/spacer/spacer_convex_closure.cpp +++ b/src/muz/spacer/spacer_convex_closure.cpp @@ -369,7 +369,6 @@ void convex_closure::cc_1dim(const expr_ref &var, expr_ref_vector &out) { m_data.get_col(j, data); std::sort(data.begin(), data.end(), gt_proc); if (infer_div_pred(data, cr, off)) { - // TODO: non-deterministic parameter evaluation out.push_back(mk_eq_mod(v, cr, off)); } } @@ -379,8 +378,9 @@ void convex_closure::cc_1dim(const expr_ref &var, expr_ref_vector &out) { expr *convex_closure::mk_eq_mod(expr *v, rational d, rational r) { expr *res = nullptr; if (m_arith.is_int(v)) { - // TODO: non-deterministic parameter evaluation - res = m.mk_eq(m_arith.mk_mod(v, m_arith.mk_int(d)), m_arith.mk_int(r)); + expr* mod_expr = m_arith.mk_mod(v, m_arith.mk_int(d)); + expr* rhs = m_arith.mk_int(r); + res = m.mk_eq(mod_expr, rhs); } else if (m_bv.is_bv(v)) { res = m.mk_eq(m_bv.mk_bv_urem(v, m_bv.mk_numeral(d, m_bv_sz)), m_bv.mk_numeral(r, m_bv_sz)); diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index e38497737..9e3703027 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -251,9 +251,9 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma) expr_ref_vector eqs(m); for (unsigned i = 0, sz = vsymbs.size(); i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - // TODO: non-deterministic parameter evaluation - eqs.push_back(m.mk_eq(m.mk_const(vsymbs.get(i)), - m.mk_const(vsymbs.get(j)))); + expr* lhs = m.mk_const(vsymbs.get(i)); + expr* rhs = m.mk_const(vsymbs.get(j)); + eqs.push_back(m.mk_eq(lhs, rhs)); } } diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index bf83f3db0..39d9ad3f1 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -261,10 +261,11 @@ namespace arith { // x mod 2^{i + 1} >= 2^i means the i'th bit is 1. auto bitof = [&](expr* x, unsigned i) { - expr_ref r(m); - // TODO: non-deterministic parameter evaluation - r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i))); - return mk_literal(r); + expr* pow_hi = a.mk_int(rational::power_of_two(i + 1)); + expr* pow_lo = a.mk_int(rational::power_of_two(i)); + expr* mod_expr = a.mk_mod(x, pow_hi); + expr* ge_expr = a.mk_ge(mod_expr, pow_lo); + return mk_literal(ge_expr); }; if (a.is_band(n)) { @@ -390,13 +391,18 @@ namespace arith { // y >= sz & x < 2^{sz-1} => n = 0 // y >= sz & x >= 2^{sz-1} => n = -1 // y = 0 => n = x - auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); - // TODO: non-deterministic parameter evaluation - add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0)))); - // TODO: non-deterministic parameter evaluation - add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1)))); - // TODO: non-deterministic parameter evaluation - add_clause(~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x))); + expr_ref half(a.mk_int(N/2), m); + expr_ref sign_expr(a.mk_ge(x, half), m); + auto signx = mk_literal(sign_expr); + expr_ref modulus(a.mk_mod(y, a.mk_int(N)), m); + expr_ref ge_sz(a.mk_ge(modulus, a.mk_int(sz)), m); + expr_ref eq_zero(m.mk_eq(n, a.mk_int(0)), m); + expr_ref eq_minus_one(m.mk_eq(n, a.mk_int(N - 1)), m); + expr_ref mod_zero(a.mk_eq(modulus, a.mk_int(0)), m); + expr_ref eq_x(m.mk_eq(n, x), m); + add_clause(~mk_literal(ge_sz), signx, mk_literal(eq_zero)); + add_clause(~mk_literal(ge_sz), ~signx, mk_literal(eq_minus_one)); + add_clause(~mk_literal(mod_zero), mk_literal(eq_x)); } else UNREACHABLE(); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 2c52a90a8..b9b089727 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -341,8 +341,9 @@ namespace q { } if (m.is_not(arg, z) && m.is_iff(z, x, y) && is_literal(x) && is_literal(y)) { e1 = m.mk_or(x, y); - // TODO: non-deterministic parameter evaluation - e2 = m.mk_or(mk_not(m, x), mk_not(m, y)); + expr* nx = mk_not(m, x); + expr* ny = mk_not(m, y); + e2 = m.mk_or(nx, ny); return true; } return false; diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp index 1b0f11051..f4b8f2d98 100644 --- a/src/sat/tactic/sat2goal.cpp +++ b/src/sat/tactic/sat2goal.cpp @@ -253,8 +253,9 @@ struct sat2goal::imp { s.collect_bin_clauses(bin_clauses, m_learned, false); for (sat::solver::bin_clause const& bc : bin_clauses) { checkpoint(); - // TODO: non-deterministic parameter evaluation - r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); + expr* lhs = lit2expr(mc, bc.first); + expr* rhs = lit2expr(mc, bc.second); + r.assert_expr(m.mk_or(lhs, rhs)); } // collect clauses assert_clauses(mc, s, s.clauses(), r, true);