mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 04:01:22 +00:00
Code Activity

try permanent ban

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-07-03 10:01:43 -07:00
parent 74f4639f0c
commit 47714163cb
2 changed files with 65 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/lp/lp_settings.h
View file

@ -149,6 +149,18 @@ struct statistics {
unsigned m_nla_throttled_horner_lemmas = 0; unsigned m_nla_throttled_horner_lemmas = 0;
unsigned m_nla_throttled_factor_zero_lemmas = 0; unsigned m_nla_throttled_factor_zero_lemmas = 0;
unsigned m_nla_throttled_factor_neutral_lemmas = 0; unsigned m_nla_throttled_factor_neutral_lemmas = 0;
unsigned m_nla_permanently_banned_lemmas = 0;
unsigned m_nla_permanently_banned_order_lemmas = 0;
unsigned m_nla_permanently_banned_binomial_sign_lemmas = 0;
unsigned m_nla_permanently_banned_monotone_lemmas = 0;
unsigned m_nla_permanently_banned_tangent_lemmas = 0;
unsigned m_nla_permanently_banned_basic_sign_lemmas = 0;
unsigned m_nla_permanently_banned_powers_lemmas = 0;
unsigned m_nla_permanently_banned_division_lemmas = 0;
unsigned m_nla_permanently_banned_grobner_lemmas = 0;
unsigned m_nla_permanently_banned_horner_lemmas = 0;
unsigned m_nla_permanently_banned_factor_zero_lemmas = 0;
unsigned m_nla_permanently_banned_factor_neutral_lemmas = 0;
::statistics m_st = {}; ::statistics m_st = {};
void reset() { void reset() {
@ -173,6 +185,18 @@ struct statistics {
st.update("arith-nla-throttled-horner-lemmas", m_nla_throttled_horner_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-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-nla-throttled-factor-neutral-lemmas", m_nla_throttled_factor_neutral_lemmas);
st.update("arith-nla-permanently-banned-lemmas", m_nla_permanently_banned_lemmas);
st.update("arith-nla-permanently-banned-order-lemmas", m_nla_permanently_banned_order_lemmas);
st.update("arith-nla-permanently-banned-binomial-sign-lemmas", m_nla_permanently_banned_binomial_sign_lemmas);
st.update("arith-nla-permanently-banned-monotone-lemmas", m_nla_permanently_banned_monotone_lemmas);
st.update("arith-nla-permanently-banned-tangent-lemmas", m_nla_permanently_banned_tangent_lemmas);
st.update("arith-nla-permanently-banned-basic-sign-lemmas", m_nla_permanently_banned_basic_sign_lemmas);
st.update("arith-nla-permanently-banned-powers-lemmas", m_nla_permanently_banned_powers_lemmas);
st.update("arith-nla-permanently-banned-division-lemmas", m_nla_permanently_banned_division_lemmas);
st.update("arith-nla-permanently-banned-grobner-lemmas", m_nla_permanently_banned_grobner_lemmas);
st.update("arith-nla-permanently-banned-horner-lemmas", m_nla_permanently_banned_horner_lemmas);
st.update("arith-nla-permanently-banned-factor-zero-lemmas", m_nla_permanently_banned_factor_zero_lemmas);
st.update("arith-nla-permanently-banned-factor-neutral-lemmas", m_nla_permanently_banned_factor_neutral_lemmas);
st.update("arith-gcd-conflict", m_gcd_conflicts); st.update("arith-gcd-conflict", m_gcd_conflicts);
st.update("arith-cube-calls", m_cube_calls); st.update("arith-cube-calls", m_cube_calls);
st.update("arith-cube-success", m_cube_success); st.update("arith-cube-success", m_cube_success);

41
src/math/lp/nla_throttle.cpp
View file

@ -197,6 +197,47 @@ bool nla_throttle::insert_new_impl(const signature& sig) {
// Check if this lemma should be permanently banned // Check if this lemma should be permanently banned
if (should_permanently_ban(sig, k)) { if (should_permanently_ban(sig, k)) {
m_permanently_forbidden.insert(sig); m_permanently_forbidden.insert(sig);
m_stats.m_nla_permanently_banned_lemmas++;
// Update specific lemma type permanent ban statistics
switch (k) {
case ORDER_LEMMA:
m_stats.m_nla_permanently_banned_order_lemmas++;
break;
case BINOMIAL_SIGN_LEMMA:
m_stats.m_nla_permanently_banned_binomial_sign_lemmas++;
break;
case MONOTONE_LEMMA:
m_stats.m_nla_permanently_banned_monotone_lemmas++;
break;
case TANGENT_LEMMA:
m_stats.m_nla_permanently_banned_tangent_lemmas++;
break;
case BASIC_SIGN_LEMMA:
m_stats.m_nla_permanently_banned_basic_sign_lemmas++;
break;
case POWERS_LEMMA:
m_stats.m_nla_permanently_banned_powers_lemmas++;
break;
case DIVISION_LEMMA:
m_stats.m_nla_permanently_banned_division_lemmas++;
break;
case GROBNER_LEMMA:
m_stats.m_nla_permanently_banned_grobner_lemmas++;
break;
case HORNER_LEMMA:
m_stats.m_nla_permanently_banned_horner_lemmas++;
break;
case FACTOR_ZERO_LEMMA:
m_stats.m_nla_permanently_banned_factor_zero_lemmas++;
break;
case FACTOR_NEUTRAL_LEMMA:
m_stats.m_nla_permanently_banned_factor_neutral_lemmas++;
break;
default:
TRACE(nla_throttle, tout << "Unexpected throttle kind in permanent ban: " << static_cast<int>(k) << "\n";);
}
TRACE(nla_throttle, TRACE(nla_throttle,
tout << "banned lemma for life, kind=" << static_cast<int>(k) tout << "banned lemma for life, kind=" << static_cast<int>(k)
<< " after " << count << " throttles\n";); << " after " << count << " throttles\n";);