diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a7a2d96dd..ac4d9369b 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -136,7 +136,19 @@ struct statistics { unsigned m_dio_rewrite_conflicts = 0; unsigned m_bounds_tightening_conflicts = 0; unsigned m_bounds_tightenings = 0; + // NLA throttling statistics unsigned m_nla_throttled_lemmas = 0; + unsigned m_nla_throttled_order_lemmas = 0; + unsigned m_nla_throttled_binomial_sign_lemmas = 0; + unsigned m_nla_throttled_monotone_lemmas = 0; + unsigned m_nla_throttled_tangent_lemmas = 0; + unsigned m_nla_throttled_basic_sign_lemmas = 0; + unsigned m_nla_throttled_powers_lemmas = 0; + unsigned m_nla_throttled_division_lemmas = 0; + unsigned m_nla_throttled_grobner_lemmas = 0; + unsigned m_nla_throttled_horner_lemmas = 0; + unsigned m_nla_throttled_factor_zero_lemmas = 0; + unsigned m_nla_throttled_factor_neutral_lemmas = 0; ::statistics m_st = {}; void reset() { @@ -148,6 +160,19 @@ struct statistics { st.update("arith-max-columns", m_max_cols); st.update("arith-max-rows", m_max_rows); st.update("arith-gcd-calls", m_gcd_calls); + // NLA throttling stats + st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas); + st.update("arith-nla-throttled-order-lemmas", m_nla_throttled_order_lemmas); + st.update("arith-nla-throttled-binomial-sign-lemmas", m_nla_throttled_binomial_sign_lemmas); + st.update("arith-nla-throttled-monotone-lemmas", m_nla_throttled_monotone_lemmas); + st.update("arith-nla-throttled-tangent-lemmas", m_nla_throttled_tangent_lemmas); + st.update("arith-nla-throttled-basic-sign-lemmas", m_nla_throttled_basic_sign_lemmas); + st.update("arith-nla-throttled-powers-lemmas", m_nla_throttled_powers_lemmas); + st.update("arith-nla-throttled-division-lemmas", m_nla_throttled_division_lemmas); + st.update("arith-nla-throttled-grobner-lemmas", m_nla_throttled_grobner_lemmas); + st.update("arith-nla-throttled-horner-lemmas", m_nla_throttled_horner_lemmas); + st.update("arith-nla-throttled-factor-zero-lemmas", m_nla_throttled_factor_zero_lemmas); + st.update("arith-nla-throttled-factor-neutral-lemmas", m_nla_throttled_factor_neutral_lemmas); st.update("arith-gcd-conflict", m_gcd_conflicts); st.update("arith-cube-calls", m_cube_calls); st.update("arith-cube-success", m_cube_success); @@ -174,7 +199,6 @@ struct statistics { st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts); st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts); st.update("arith-bounds-tightenings", m_bounds_tightenings); - st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas); st.copy(m_st); } }; diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 20d6cde75..7b0cb4d25 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -22,6 +22,12 @@ bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) { const rational sign = sign_to_rat(m.rsign() ^ n.rsign()); if (var_val(m) == var_val(n) * sign) return false; + + // Throttle basic sign lemmas + if (c().throttle().insert_new_basic_sign(nla_throttle::BASIC_SIGN_LEMMA, m.var(), n.var())) { + return false; // throttled + } + TRACE(nla_solver, tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";); generate_sign_lemma(m, n, sign); return true; @@ -225,6 +231,11 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) { if (val(j).is_zero()) return false; } + + // Throttle factor zero lemmas + if (!f.is_empty() && c().throttle().insert_new_factor(nla_throttle::FACTOR_ZERO_LEMMA, rm.var(), var(f[0]), true)) + return false; // throttled + TRACE(nla_solver, c().trace_print_monic_and_factorization(rm, f, tout);); lemma_builder lemma(c(), "xy = 0 -> x = 0 or y = 0"); lemma.explain_fixed(var(rm)); @@ -536,6 +547,11 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic if (abs_mv == rational::zero()) { return false; } + + // Throttle neutral factor lemmas + if (!f.is_empty() && c().throttle().insert_new_factor(nla_throttle::FACTOR_NEUTRAL_LEMMA, rm.var(), var(f[0]), false)) + return false; // throttled + lpvar u = null_lpvar, v = null_lpvar; bool all_int = true; for (auto fc : f) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e06faafff..ed02d70d6 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -103,7 +103,6 @@ class core { lpvar m_patched_var = 0; monic const* m_patched_monic = nullptr; - nla_throttle m_throttle; bool m_throttle_enabled = true; @@ -439,6 +438,7 @@ public: bool throttle_enabled() const { return m_throttle_enabled; } nla_throttle& throttle() { return m_throttle; } const nla_throttle& throttle() const { return m_throttle; } + nla_throttle m_throttle; }; // end of core diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp index 49b4ee765..bc70d08c2 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/src/math/lp/nla_divisions.cpp @@ -53,8 +53,12 @@ namespace nla { return; auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, - auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { + auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) -> bool { if (y1val >= y2val && y2val > 0 && 0 <= x1val && x1val <= x2val && q1val > q2val) { + // Throttle division lemmas + if (c.throttle().insert_new_division(nla_throttle::DIVISION_LEMMA, q1, x1, y1, 0)) + return false; // throttled + lemma_builder lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2"); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(y2, llc::LE, 0); @@ -67,8 +71,12 @@ namespace nla { }; auto monotonicity2 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, - auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { + auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) -> bool { if (y2val <= y1val && y1val < 0 && x1val >= x2val && x2val >= 0 && q1val > q2val) { + // Throttle division lemmas + if (c.throttle().insert_new_division(nla_throttle::DIVISION_LEMMA, q1, x1, y1, 1)) + return false; // throttled + lemma_builder lemma(c, "y2 <= y1 < 0 & x1 >= x2 >= 0 => x1/y1 <= x2/y2"); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(y1, llc::GE, 0); @@ -81,8 +89,12 @@ namespace nla { }; auto monotonicity3 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, - auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { + auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) -> bool { if (y2val <= y1val && y1val < 0 && x1val <= x2val && x2val <= 0 && q1val < q2val) { + // Throttle division lemmas + if (c.throttle().insert_new_division(nla_throttle::DIVISION_LEMMA, q1, x1, y1, 2)) + return false; // throttled + lemma_builder lemma(c, "y2 <= y1 < 0 & x1 <= x2 <= 0 => x1/y1 >= x2/y2"); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(y1, llc::GE, 0); @@ -95,7 +107,7 @@ namespace nla { }; auto monotonicity = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, - auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { + auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) -> bool { if (monotonicity1(x1, x1val, y1, y1val, q1, q1val, x2, x2val, y2, y2val, q2, q2val)) return true; if (monotonicity1(x2, x2val, y2, y2val, q2, q2val, x1, x1val, y1, y1val, q1, q1val)) @@ -187,17 +199,23 @@ namespace nla { rational hi = yv * div_v + yv - 1; rational lo = yv * div_v; if (xv > hi) { - lemma_builder lemma(c, "y = yv & x <= yv * div(xv, yv) + yv - 1 => div(p, y) <= div(xv, yv)"); - lemma |= ineq(y, llc::NE, yv); - lemma |= ineq(x, llc::GT, hi); - lemma |= ineq(q, llc::LE, div_v); + // Throttle division lemmas + if (!c.throttle().insert_new_division(nla_throttle::DIVISION_LEMMA, q, x, y, 3)) { + lemma_builder lemma(c, "y = yv & x <= yv * div(xv, yv) + yv - 1 => div(p, y) <= div(xv, yv)"); + lemma |= ineq(y, llc::NE, yv); + lemma |= ineq(x, llc::GT, hi); + lemma |= ineq(q, llc::LE, div_v); + } return; } if (xv < lo) { - lemma_builder lemma(c, "y = yv & x >= yv * div(xv, yv) => div(xv, yv) <= div(x, y)"); - lemma |= ineq(y, llc::NE, yv); - lemma |= ineq(x, llc::LT, lo); - lemma |= ineq(q, llc::GE, div_v); + // Throttle division lemmas + if (!c.throttle().insert_new_division(nla_throttle::DIVISION_LEMMA, q, x, y, 4)) { + lemma_builder lemma(c, "y = yv & x >= yv * div(xv, yv) => div(xv, yv) <= div(x, y)"); + lemma |= ineq(y, llc::NE, yv); + lemma |= ineq(x, llc::LT, lo); + lemma |= ineq(q, llc::GE, div_v); + } return; } } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 09660a2a6..a00fe1da1 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -343,9 +343,13 @@ namespace nla { return false; } evali.get_interval(e.poly(), i_wd); - std::function f = [this](const lp::explanation& e) { + std::function f = [this, &e](const lp::explanation& exp) { + // Throttle Grobner lemmas + if (c().throttle().insert_new_grobner(nla_throttle::GROBNER_LEMMA, e.poly().free_vars()[0], 0, e.idx())) + return; // throttled + lemma_builder lemma(m_core, "pdd"); - lemma &= e; + lemma &= exp; }; if (di.check_interval_for_conflict_on_zero(i_wd, e.dep(), f)) { TRACE(grobner, m_solver.display(tout << "conflict ", e) << "\n"); @@ -643,6 +647,13 @@ namespace nla { } bool grobner::add_horner_conflict(const dd::solver::equation& eq) { + // Throttle horner lemmas + if (!eq.poly().free_vars().empty()) { + lpvar first_var = eq.poly().free_vars()[0]; + if (false && c().throttle().insert_new_horner(nla_throttle::HORNER_LEMMA, first_var, eq.idx())) + return false; // throttled + } + nex_creator& nc = m_nex_creator; nc.pop(0); nex_creator::sum_factory sum(nc); diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp index 038d26fff..92908e57c 100644 --- a/src/math/lp/nla_powers.cpp +++ b/src/math/lp/nla_powers.cpp @@ -89,6 +89,10 @@ namespace nla { lemmas.reset(); auto x_exp_0 = [&]() { + // Throttle powers lemmas + if (c.throttle().insert_new_powers(nla_throttle::POWERS_LEMMA, r, x, y, 0)) + return l_false; // throttled + lemma_builder lemma(c, "x != 0 => x^0 = 1"); lemma |= ineq(x, llc::EQ, rational::zero()); lemma |= ineq(y, llc::NE, rational::zero()); @@ -97,6 +101,10 @@ namespace nla { }; auto zero_exp_y = [&]() { + // Throttle powers lemmas + if (c.throttle().insert_new_powers(nla_throttle::POWERS_LEMMA, r, x, y, 1)) + return l_false; // throttled + lemma_builder lemma(c, "y != 0 => 0^y = 0"); lemma |= ineq(x, llc::NE, rational::zero()); lemma |= ineq(y, llc::EQ, rational::zero()); @@ -105,6 +113,10 @@ namespace nla { }; auto x_gt_0 = [&]() { + // Throttle powers lemmas + if (c.throttle().insert_new_powers(nla_throttle::POWERS_LEMMA, r, x, y, 2)) + return l_false; // throttled + lemma_builder lemma(c, "x > 0 => x^y > 0"); lemma |= ineq(x, llc::LE, rational::zero()); lemma |= ineq(r, llc::GT, rational::zero()); @@ -112,6 +124,10 @@ namespace nla { }; auto y_lt_1 = [&]() { + // Throttle powers lemmas + if (c.throttle().insert_new_powers(nla_throttle::POWERS_LEMMA, r, x, y, 3)) + return l_false; // throttled + lemma_builder lemma(c, "x > 1, y < 0 => x^y < 1"); lemma |= ineq(x, llc::LE, rational::one()); lemma |= ineq(y, llc::GE, rational::zero()); diff --git a/src/math/lp/nla_throttle.cpp b/src/math/lp/nla_throttle.cpp index d56fec1a9..404ede6f4 100644 --- a/src/math/lp/nla_throttle.cpp +++ b/src/math/lp/nla_throttle.cpp @@ -68,13 +68,190 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpv return insert_new_impl(sig); } +bool nla_throttle::insert_new_powers(throttle_kind k, lpvar r, lpvar x, lpvar y, unsigned lemma_type) { + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(r); + sig.m_values[2] = static_cast(x); + sig.m_values[3] = static_cast(y); + sig.m_values[4] = static_cast(lemma_type); + return insert_new_impl(sig); +} + +bool nla_throttle::insert_new_division(throttle_kind k, lpvar q, lpvar x, lpvar y, unsigned lemma_type) { + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(q); + sig.m_values[2] = static_cast(x); + sig.m_values[3] = static_cast(y); + sig.m_values[4] = static_cast(lemma_type); + return insert_new_impl(sig); +} + +bool nla_throttle::insert_new_grobner(throttle_kind k, lpvar v1, lpvar v2, unsigned eq_id) { + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(v1); + sig.m_values[2] = static_cast(v2); + sig.m_values[3] = static_cast(eq_id); + return insert_new_impl(sig); +} + +bool nla_throttle::insert_new_basic_sign(throttle_kind k, lpvar m, int sign) { + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(m); + sig.m_values[2] = normalize_sign(sign); + return insert_new_impl(sig); +} + +bool nla_throttle::insert_new_horner(throttle_kind k, lpvar v, unsigned term_id) { + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(v); + sig.m_values[2] = static_cast(term_id); + return insert_new_impl(sig); +} + +bool nla_throttle::insert_new_factor(throttle_kind k, lpvar monic, lpvar factor, bool is_zero) { + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(monic); + sig.m_values[2] = static_cast(factor); + sig.m_values[3] = static_cast(is_zero ? 1 : 0); + return insert_new_impl(sig); +} + bool nla_throttle::insert_new_impl(const signature& sig) { - if (m_seen.contains(sig)) { - TRACE(nla_solver, tout << "throttled lemma generation\n";); + throttle_kind k = static_cast(sig.m_values[0]); + + // Check permanent throttling first (forbidden for life) + if (m_permanently_forbidden.contains(sig)) { + TRACE(nla_throttle, + tout << "permanently throttled lemma generation, kind=" << static_cast(k) + << " sig=[" << sig.m_values[0] << "," << sig.m_values[1] << "," + << sig.m_values[2] << "," << sig.m_values[3] << "," + << sig.m_values[4] << "," << sig.m_values[5] << "," + << sig.m_values[6] << "," << sig.m_values[7] << "]\n";); m_stats.m_nla_throttled_lemmas++; + + // Update specific lemma type statistics + switch (k) { + case ORDER_LEMMA: + m_stats.m_nla_throttled_order_lemmas++; + break; + case BINOMIAL_SIGN_LEMMA: + m_stats.m_nla_throttled_binomial_sign_lemmas++; + break; + case MONOTONE_LEMMA: + m_stats.m_nla_throttled_monotone_lemmas++; + break; + case TANGENT_LEMMA: + m_stats.m_nla_throttled_tangent_lemmas++; + break; + case BASIC_SIGN_LEMMA: + m_stats.m_nla_throttled_basic_sign_lemmas++; + break; + case POWERS_LEMMA: + m_stats.m_nla_throttled_powers_lemmas++; + break; + case DIVISION_LEMMA: + m_stats.m_nla_throttled_division_lemmas++; + break; + case GROBNER_LEMMA: + m_stats.m_nla_throttled_grobner_lemmas++; + break; + case HORNER_LEMMA: + m_stats.m_nla_throttled_horner_lemmas++; + break; + case FACTOR_ZERO_LEMMA: + m_stats.m_nla_throttled_factor_zero_lemmas++; + break; + case FACTOR_NEUTRAL_LEMMA: + m_stats.m_nla_throttled_factor_neutral_lemmas++; + break; + default: + TRACE(nla_throttle, tout << "Unexpected throttle kind: " << static_cast(k) << "\n";); + } + + return true; // Permanently throttled + } + + // Check temporary throttling (backtrackable) + if (m_seen.contains(sig)) { + TRACE(nla_throttle, tout << "throttled lemma generation\n";); + m_stats.m_nla_throttled_lemmas++; + + // Increment throttle count + auto it = m_throttle_count.find_core(sig); + unsigned count = (it != nullptr) ? it->get_data().m_value + 1 : 1; + m_throttle_count.insert(sig, count); + + TRACE(nla_throttle, + tout << "throttled lemma, kind=" << static_cast(k) << " count=" << count + << " sig=[" << sig.m_values[0] << "," << sig.m_values[1] << "," + << sig.m_values[2] << "," << sig.m_values[3] << "," + << sig.m_values[4] << "," << sig.m_values[5] << "," + << sig.m_values[6] << "," << sig.m_values[7] << "]\n";); + + // Check if this lemma should be permanently banned + if (should_permanently_ban(sig, k)) { + m_permanently_forbidden.insert(sig); + TRACE(nla_throttle, + tout << "banned lemma for life, kind=" << static_cast(k) + << " after " << count << " throttles\n";); + } + + // Update specific lemma type statistics + switch (k) { + case ORDER_LEMMA: + m_stats.m_nla_throttled_order_lemmas++; + break; + case BINOMIAL_SIGN_LEMMA: + m_stats.m_nla_throttled_binomial_sign_lemmas++; + break; + case MONOTONE_LEMMA: + m_stats.m_nla_throttled_monotone_lemmas++; + break; + case TANGENT_LEMMA: + m_stats.m_nla_throttled_tangent_lemmas++; + break; + case BASIC_SIGN_LEMMA: + m_stats.m_nla_throttled_basic_sign_lemmas++; + break; + case POWERS_LEMMA: + m_stats.m_nla_throttled_powers_lemmas++; + break; + case DIVISION_LEMMA: + m_stats.m_nla_throttled_division_lemmas++; + break; + case GROBNER_LEMMA: + m_stats.m_nla_throttled_grobner_lemmas++; + break; + case HORNER_LEMMA: + m_stats.m_nla_throttled_horner_lemmas++; + break; + case FACTOR_ZERO_LEMMA: + m_stats.m_nla_throttled_factor_zero_lemmas++; + break; + case FACTOR_NEUTRAL_LEMMA: + m_stats.m_nla_throttled_factor_neutral_lemmas++; + break; + default: + TRACE(nla_throttle, tout << "Unexpected throttle kind: " << static_cast(k) << "\n";); + } + return true; // Already seen, throttle } + TRACE(nla_throttle, + tout << "new lemma, kind=" << static_cast(k) + << " sig=[" << sig.m_values[0] << "," << sig.m_values[1] << "," + << sig.m_values[2] << "," << sig.m_values[3] << "," + << sig.m_values[4] << "," << sig.m_values[5] << "," + << sig.m_values[6] << "," << sig.m_values[7] << "]\n";); + + // Add to temporary throttling (backtrackable) m_seen.insert(sig); m_trail.push(insert_map(m_seen, sig)); return false; // New, don't throttle diff --git a/src/math/lp/nla_throttle.h b/src/math/lp/nla_throttle.h index 59178a49a..6e52d1dc1 100644 --- a/src/math/lp/nla_throttle.h +++ b/src/math/lp/nla_throttle.h @@ -9,6 +9,7 @@ #include "math/lp/nla_defs.h" #include "math/lp/lp_settings.h" #include "util/hashtable.h" +#include "util/map.h" #include "util/trail.h" #include @@ -20,7 +21,14 @@ public: ORDER_LEMMA, // order lemma (9 params) BINOMIAL_SIGN_LEMMA, // binomial sign (6 params) MONOTONE_LEMMA, // monotonicity (2 params) - TANGENT_LEMMA // tangent lemma (5 params: monic_var, x_var, y_var, below, plane_type) + TANGENT_LEMMA, // tangent lemma (5 params: monic_var, x_var, y_var, below, plane_type) + BASIC_SIGN_LEMMA, // basic sign lemmas + POWERS_LEMMA, // x^y constraint lemmas + DIVISION_LEMMA, // q = x/y constraint lemmas + GROBNER_LEMMA, // grobner basis lemmas + HORNER_LEMMA, // horner polynomial evaluation lemmas + FACTOR_ZERO_LEMMA, // lemma for mon zero factors + FACTOR_NEUTRAL_LEMMA // lemma for neutral monomial factors }; private: @@ -46,11 +54,43 @@ private: } }; + // Temporary throttling (backtrackable via trail) hashtable> m_seen; + + // Permanent throttling (forbidden for life, not backtrackable) + hashtable> m_permanently_forbidden; + + // Throttle frequency counter: tracks how many times each signature has been throttled + map> m_throttle_count; + trail_stack& m_trail; lp::statistics& m_stats; + // Throttling thresholds per lemma type + unsigned get_permanent_throttle_threshold(throttle_kind k) const { + switch (k) { + case BASIC_SIGN_LEMMA: return 2; // Ban after 2 throttles - deterministic patterns + case FACTOR_ZERO_LEMMA: return 1; // Ban after 1 throttle - highly deterministic + case FACTOR_NEUTRAL_LEMMA: return 1; // Ban after 1 throttle - highly deterministic + case POWERS_LEMMA: return 3; // Ban after 3 throttles - some variability + case DIVISION_LEMMA: return 3; // Ban after 3 throttles - some variability + case GROBNER_LEMMA: return 5; // Ban after 5 throttles - context dependent + case HORNER_LEMMA: return 4; // Ban after 4 throttles - moderately variable + case ORDER_LEMMA: return 4; // Ban after 4 throttles - context dependent + case BINOMIAL_SIGN_LEMMA: return 3; // Ban after 3 throttles - some variability + case MONOTONE_LEMMA: return 3; // Ban after 3 throttles - context dependent + case TANGENT_LEMMA: return 4; // Ban after 4 throttles - geometric constraints + default: return 3; // Conservative default + } + } + // Check if a lemma should be permanently banned based on throttle count + bool should_permanently_ban(const signature& sig, throttle_kind k) { + unsigned threshold = get_permanent_throttle_threshold(k); + auto it = m_throttle_count.find_core(sig); + return it != nullptr && it->get_data().m_value >= threshold; + } + public: nla_throttle(trail_stack& trail, lp::statistics& stats) : m_trail(trail), m_stats(stats) {} @@ -69,6 +109,24 @@ public: // Tangent lemma (simplified): monic_var + x_var + y_var + below bool insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below); + + // Powers lemma: r + x + y + lemma_type + bool insert_new_powers(throttle_kind k, lpvar r, lpvar x, lpvar y, unsigned lemma_type); + + // Division lemma: q + x + y + lemma_type + bool insert_new_division(throttle_kind k, lpvar q, lpvar x, lpvar y, unsigned lemma_type); + + // Grobner lemma: variables with equation id + bool insert_new_grobner(throttle_kind k, lpvar v1, lpvar v2, unsigned eq_id); + + // Basic sign lemma: m + sign + bool insert_new_basic_sign(throttle_kind k, lpvar m, int sign); + + // Horner lemma: variable + term + bool insert_new_horner(throttle_kind k, lpvar v, unsigned term_id); + + // Factor zero/neutral lemma: monic + factor + bool insert_new_factor(throttle_kind k, lpvar monic, lpvar factor, bool is_zero); private: bool insert_new_impl(const signature& sig);