mirror of
https://github.com/Z3Prover/z3
synced 2025-07-24 13:18:55 +00:00
permanent throttling
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
d2990e2f68
commit
74f4639f0c
8 changed files with 339 additions and 19 deletions
|
|
@ -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);
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -343,9 +343,13 @@ namespace nla {
|
|||
return false;
|
||||
}
|
||||
evali.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd);
|
||||
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
|
||||
std::function<void (const lp::explanation&)> 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);
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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<unsigned>(k);
|
||||
sig.m_values[1] = static_cast<unsigned>(r);
|
||||
sig.m_values[2] = static_cast<unsigned>(x);
|
||||
sig.m_values[3] = static_cast<unsigned>(y);
|
||||
sig.m_values[4] = static_cast<unsigned>(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<unsigned>(k);
|
||||
sig.m_values[1] = static_cast<unsigned>(q);
|
||||
sig.m_values[2] = static_cast<unsigned>(x);
|
||||
sig.m_values[3] = static_cast<unsigned>(y);
|
||||
sig.m_values[4] = static_cast<unsigned>(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<unsigned>(k);
|
||||
sig.m_values[1] = static_cast<unsigned>(v1);
|
||||
sig.m_values[2] = static_cast<unsigned>(v2);
|
||||
sig.m_values[3] = static_cast<unsigned>(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<unsigned>(k);
|
||||
sig.m_values[1] = static_cast<unsigned>(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<unsigned>(k);
|
||||
sig.m_values[1] = static_cast<unsigned>(v);
|
||||
sig.m_values[2] = static_cast<unsigned>(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<unsigned>(k);
|
||||
sig.m_values[1] = static_cast<unsigned>(monic);
|
||||
sig.m_values[2] = static_cast<unsigned>(factor);
|
||||
sig.m_values[3] = static_cast<unsigned>(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<throttle_kind>(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<int>(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<int>(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<int>(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<int>(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<int>(k) << "\n";);
|
||||
}
|
||||
|
||||
return true; // Already seen, throttle
|
||||
}
|
||||
|
||||
TRACE(nla_throttle,
|
||||
tout << "new lemma, kind=" << static_cast<int>(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
|
||||
|
|
|
|||
|
|
@ -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 <cstring>
|
||||
|
||||
|
|
@ -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<signature, signature_hash, default_eq<signature>> m_seen;
|
||||
|
||||
// Permanent throttling (forbidden for life, not backtrackable)
|
||||
hashtable<signature, signature_hash, default_eq<signature>> m_permanently_forbidden;
|
||||
|
||||
// Throttle frequency counter: tracks how many times each signature has been throttled
|
||||
map<signature, unsigned, signature_hash, default_eq<signature>> 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);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue