From d717dae3ac4bf29525aa0d9bf879d12e24f44e79 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 26 Jun 2025 14:38:44 -0700 Subject: [PATCH] remove the parameter for throttling nla lemmas --- src/math/lp/nla_core.cpp | 1 - src/math/lp/nla_core.h | 1 - src/math/lp/nla_throttle.cpp | 5 ----- src/math/lp/nla_throttle.h | 4 +--- src/params/smt_params_helper.pyg | 1 - 5 files changed, 1 insertion(+), 11 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index b65729c44..34084700e 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -42,7 +42,6 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_throttle(lra.trail(), lra.settings().stats()) { m_nlsat_delay_bound = lp_settings().nlsat_delay(); - m_throttle.set_enabled(m_params.arith_nl_thrl()); lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { for (lpvar j : columns_with_changed_bounds) { if (is_monic_var(j)) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 9ca96788a..e06faafff 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -436,7 +436,6 @@ public: void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } - void set_throttle_enabled(bool enabled) { m_throttle_enabled = enabled; m_throttle.set_enabled(enabled); } bool throttle_enabled() const { return m_throttle_enabled; } nla_throttle& throttle() { return m_throttle; } const nla_throttle& throttle() const { return m_throttle; } diff --git a/src/math/lp/nla_throttle.cpp b/src/math/lp/nla_throttle.cpp index 83f32c9ec..d56fec1a9 100644 --- a/src/math/lp/nla_throttle.cpp +++ b/src/math/lp/nla_throttle.cpp @@ -11,7 +11,6 @@ namespace nla { bool nla_throttle::insert_new(throttle_kind k, lpvar mvar, bool is_lt) { - if (!m_enabled) return false; signature sig; sig.m_values[0] = static_cast(k); sig.m_values[1] = static_cast(mvar); @@ -20,7 +19,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar mvar, bool is_lt) { } bool nla_throttle::insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, int sign, int sy) { - if (!m_enabled) return false; signature sig; sig.m_values[0] = static_cast(k); sig.m_values[1] = static_cast(xy_var); @@ -33,7 +31,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, i bool nla_throttle::insert_new(throttle_kind k, lpvar ac_var, lpvar a, const rational& c_sign, lpvar c, lpvar bd_var, lpvar b_var, const rational& d_sign, lpvar d, llc ab_cmp) { - if (!m_enabled) return false; signature sig; sig.m_values[0] = static_cast(k); sig.m_values[1] = static_cast(ac_var); @@ -50,7 +47,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar ac_var, lpvar a, const rati } bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below, int plane_type) { - if (!m_enabled) return false; signature sig; sig.m_values[0] = static_cast(k); sig.m_values[1] = static_cast(monic_var); @@ -62,7 +58,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpv } bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below) { - if (!m_enabled) return false; signature sig; sig.m_values[0] = static_cast(k); sig.m_values[1] = static_cast(monic_var); diff --git a/src/math/lp/nla_throttle.h b/src/math/lp/nla_throttle.h index 4c580b457..59178a49a 100644 --- a/src/math/lp/nla_throttle.h +++ b/src/math/lp/nla_throttle.h @@ -49,12 +49,10 @@ private: hashtable> m_seen; trail_stack& m_trail; lp::statistics& m_stats; - bool m_enabled = true; + public: nla_throttle(trail_stack& trail, lp::statistics& stats) : m_trail(trail), m_stats(stats) {} - void set_enabled(bool enabled) { m_enabled = enabled; } - bool enabled() const { return m_enabled; } // Monotone lemma: mvar + is_lt bool insert_new(throttle_kind k, lpvar mvar, bool is_lt); diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 8e1124ee7..c1eb0148a 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -65,7 +65,6 @@ def_module_params(module_name='smt', ('arith.nl.order', BOOL, True, 'run order lemmas'), ('arith.nl.expp', BOOL, False, 'expensive patching'), ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'), - ('arith.nl.thrl', BOOL, True, 'throttle repeated lemmas - debug, remove later!!!'), ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'), ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),