remove the parameter for throttling nla lemmas

Author: levnach

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))

src/math/lp/nla_core.h

@@ -436,7 +436,6 @@ class core {
     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; }

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<unsigned>(k);
     sig.m_values[1] = static_cast<unsigned>(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<unsigned>(k);
     sig.m_values[1] = static_cast<unsigned>(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<unsigned>(k);
     sig.m_values[1] = static_cast<unsigned>(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<unsigned>(k);
     sig.m_values[1] = static_cast<unsigned>(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<unsigned>(k);
     sig.m_values[1] = static_cast<unsigned>(monic_var);

src/math/lp/nla_throttle.h

@@ -49,12 +49,10 @@ class nla_throttle {
     hashtable<signature, signature_hash, default_eq<signature>> 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);

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'),