From 711572e73c258a27d051341ea81f27f50fdfb24c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Nov 2025 16:58:33 -0800 Subject: [PATCH] fix crash on arie branch Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 20 +++++++++---------- src/math/lp/nla_stellensatz.cpp | 31 +++++++++++++---------------- src/math/lp/nla_stellensatz.h | 2 +- 3 files changed, 24 insertions(+), 29 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 02f2e1321..35cfbe023 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -771,17 +771,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } } if (m_util.is_idiv(arg1, t, e) && is_numeral(e, a1) && a1 > 0) { - - // e > 0 => t div e ~ arg2 <=> e * (t div e) ~ e * arg2 <=> t - mod t e ~ e * arg2 - if (is_numeral(arg2, a2) && a2 == 0 && (kind == LE || kind == GE)) { - switch (kind) { - case LE: result = m_util.mk_le(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3; - case GE: result = m_util.mk_ge(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3; - case EQ: result = m.mk_eq(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3; - } - } - // generally: result = m_util.mk_sub(t, m_util.mk_mod(t, e)); - } + if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) { a2.neg(); new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1)); @@ -792,6 +782,14 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } } else if (st == BR_DONE && arg1 == orig_arg1 && arg2 == orig_arg2) { + // e > 0 => t div e ~ arg2 <=> e * (t div e) ~ e * arg2 <=> t - mod t e ~ e * arg2 + if (is_numeral(arg2, a2) && a2 == 0 && (kind == LE || kind == GE)) { + switch (kind) { + case LE: result = m_util.mk_le(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3; + case GE: result = m_util.mk_ge(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3; + case EQ: result = m.mk_eq(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3; + } + } // Nothing new; return BR_FAILED to avoid rewriting loops. return BR_FAILED; } diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp index fbc2c8ef4..6092ab66b 100644 --- a/src/math/lp/nla_stellensatz.cpp +++ b/src/math/lp/nla_stellensatz.cpp @@ -216,6 +216,7 @@ namespace nla { ci = m_constraints.size(); m_constraints.push_back({p, k, j }); m_constraint_index.insert({p.index(), k}, ci); + m_tabu.reserve(ci + 1); return ci; } @@ -223,7 +224,6 @@ namespace nla { if (m_active.contains(ci)) return; m_active.insert(ci); - m_tabu.reserve(ci + 1); m_tabu[ci] = tabu; } @@ -284,20 +284,17 @@ namespace nla { for (unsigned cx = 0; cx < num_x; ++cx) { auto other_ci = m_occurs[x][cx]; - switch (resolve_variable(x, ci, other_ci, p_value, f, _m1, _f_p)) { - case l_false: return l_false; - case l_true: break; - case l_undef: break; - } + if (!resolve_variable(x, ci, other_ci, p_value, f, _m1, _f_p)) + return l_false; } return l_undef; } - lbool stellensatz::resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci, + bool stellensatz::resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci, rational const& p_value, factorization const &f, unsigned_vector const &_m1, dd::pdd _f_p) { if (ci == other_ci) - return l_undef; + return true; auto const &[other_p, other_k, other_j] = m_constraints[other_ci]; auto const &[p, k, j] = m_constraints[ci]; auto g = factor(x, other_ci); @@ -310,13 +307,13 @@ namespace nla { SASSERT(g.degree > 0); SASSERT(p_value != 0); if (g.degree > f.degree) // future: could handle this too by considering tabu to be a map into degrees. - return l_undef; + return true; if (p_value > 0 && p_value2 > 0) - return l_undef; + return true; if (p_value < 0 && p_value2 < 0) - return l_undef; + return true; if (any_of(other_p.free_vars(), [&](unsigned j) { return m_tabu[ci].contains(j); })) - return l_undef; + return true; TRACE(arith, tout << "factor (" << other_ci << ") " << other_p << " -> j" << x << "^" << g.degree << " * " << g.p << " + " << g.q << "\n"); @@ -334,9 +331,9 @@ namespace nla { g_p = g_p.mul(m2); if (!has_term_offset(f_p)) - return l_undef; + return true; if (!has_term_offset(g_p)) - return l_undef; + return true; TRACE(arith, tout << "m1 " << m1 << " m2 " << m2 << " m1m2: " << m1m2 << "\n"); @@ -372,7 +369,7 @@ namespace nla { auto new_ci = add(ci_a, ci_b); CTRACE(arith, !is_new_constraint(new_ci), display_constraint(tout << "not new ", new_ci) << "\n"); if (!is_new_constraint(new_ci)) - return l_undef; + return true; if (m_constraints[new_ci].p.degree() <= 3) init_occurs(new_ci); TRACE(arith, tout << "eliminate j" << x << ":\n"; display_constraint(tout << "ci: ", ci) << "\n"; @@ -381,7 +378,7 @@ namespace nla { display_constraint(tout << "new_ci: ", new_ci) << "\n"); if (conflict(new_ci)) - return l_false; + return false; if (!constraint_is_true(new_ci)) { auto const &[new_p, new_k, new_j] = m_constraints[new_ci]; @@ -391,7 +388,7 @@ namespace nla { add_active(new_ci, new_tabu); } } - return l_true; + return true; } bool stellensatz::conflict(lp::constraint_index ci) { diff --git a/src/math/lp/nla_stellensatz.h b/src/math/lp/nla_stellensatz.h index af01724b3..815ab6b46 100644 --- a/src/math/lp/nla_stellensatz.h +++ b/src/math/lp/nla_stellensatz.h @@ -166,7 +166,7 @@ namespace nla { unsigned degree_of_var_in_constraint(lpvar v, lp::constraint_index ci) const; factorization factor(lpvar v, lp::constraint_index ci); lbool resolve_variable(lpvar x, lp::constraint_index ci); - lbool resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci, rational const& p_value, + bool resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci, rational const& p_value, factorization const& f, unsigned_vector const& m1, dd::pdd _f_p); bool constraint_is_true(lp::constraint_index ci) const;