consolidate throttling

src/math/lp/nla_monotone_lemmas.cpp

@@ -7,31 +7,10 @@
   --*/
 #include "math/lp/nla_basics_lemmas.h"
 #include "math/lp/nla_core.h"
-#include "util/trail.h"
 namespace nla {
 
 monotone::monotone(core * c) : common(c) {}
     
-bool monotone::throttle_monotone(const monic& m, bool is_lt) {
-    // Check if throttling is enabled
-    if (!c().params().arith_nl_thrl())
-        return false;
-    
-    // Create the key for this specific monotonicity_lemma invocation
-    monotone_key key(m.var(), is_lt);
-    
-    // Check if this combination has already been processed
-    if (m_processed_monotone.contains(key)) {
-        TRACE(nla_solver, tout << "throttled monotonicity_lemma\n";);
-        return true;
-    }
-    
-    // Mark this combination as processed and add to trail for backtracking
-    m_processed_monotone.insert(key);
-    c().trail().push(insert_map(m_processed_monotone, key));
-    return false;
-}
-    
 void monotone::monotonicity_lemma() {
     unsigned shift = random();
     unsigned size = c().m_to_refine.size();
@@ -52,7 +31,7 @@ void monotone::monotonicity_lemma(monic const& m) {
     bool is_lt = m_val < prod_val;
     
     // Check if this specific combination should be throttled
-    if (throttle_monotone(m, is_lt))
+    if (c().throttle().insert_new(nla_throttle::MONOTONE_LEMMA, m.var(), is_lt))
         return;
     
     if (is_lt)

src/math/lp/nla_monotone_lemmas.h

@@ -6,8 +6,6 @@
    Nikolaj Bjorner (nbjorner)
   --*/
 #pragma once
-#include "util/hashtable.h"
-#include "util/hash.h"
 
 namespace nla {
     class core;
@@ -16,33 +14,7 @@ namespace nla {
         monotone(core *core);
         void monotonicity_lemma();
         
-        // Structure to represent the key parameters for throttling monotonicity_lemma
-        struct monotone_key {
-            short mvar;
-            bool is_lt;
-            
-            // Default constructor for hashtable
-            monotone_key() : mvar(0), is_lt(false) {}
-            
-            monotone_key(lpvar mvar, bool is_lt)
-                : mvar(static_cast<short>(mvar)), is_lt(is_lt) {}
-                
-            bool operator==(const monotone_key& other) const {
-                return mvar == other.mvar && is_lt == other.is_lt;
-            }
-        };
-        
-        struct monotone_key_hash {
-            unsigned operator()(const monotone_key& k) const {
-                return combine_hash(static_cast<unsigned>(k.mvar), 
-                                  static_cast<unsigned>(k.is_lt));
-            }
-        };
-        
     private:
-        hashtable<monotone_key, monotone_key_hash, default_eq<monotone_key>> m_processed_monotone;
-        bool throttle_monotone(const monic& m, bool is_lt);
-        
         void monotonicity_lemma(monic const& m);
         void monotonicity_lemma_gt(const monic& m);    
         void monotonicity_lemma_lt(const monic& m);

src/math/lp/nla_tangent_lemmas.cpp

@@ -70,6 +70,9 @@ private:
     }
 
     void generate_plane(const point & pl) {
+        if (c().throttle().insert_new(nla_throttle::TANGENT_LEMMA, m_j, m_jx, m_jy, m_below))
+            return;
+            
         lemma_builder lemma(c(), "generate tangent plane");
         c().negate_relation(lemma, m_jx, m_x.rat_sign()*pl.x);
         c().negate_relation(lemma, m_jy, m_y.rat_sign()*pl.y);

src/math/lp/nla_throttle.cpp

@@ -10,6 +10,69 @@
 
 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);
+    sig.m_values[2] = static_cast<unsigned>(is_lt ? 1 : 0);
+    return insert_new_impl(sig);
+}
+
+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);
+    sig.m_values[2] = static_cast<unsigned>(x);
+    sig.m_values[3] = static_cast<unsigned>(y);
+    sig.m_values[4] = normalize_sign(sign);
+    sig.m_values[5] = normalize_sign(sy);
+    return insert_new_impl(sig);
+}
+
+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);
+    sig.m_values[2] = static_cast<unsigned>(a);
+    sig.m_values[3] = pack_rational_sign(c_sign);
+    sig.m_values[4] = static_cast<unsigned>(c);
+    sig.m_values[5] = static_cast<unsigned>(bd_var);
+    sig.m_values[6] = static_cast<unsigned>(b_var);
+    // Pack d_sign, d, and ab_cmp into the last slot
+    sig.m_values[7] = (pack_rational_sign(d_sign) << 24) | 
+                     ((static_cast<unsigned>(d) & 0xFFFF) << 8) |
+                     (static_cast<unsigned>(ab_cmp) & 0xFF);
+    return insert_new_impl(sig);
+}
+
+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);
+    sig.m_values[2] = static_cast<unsigned>(x_var);
+    sig.m_values[3] = static_cast<unsigned>(y_var);
+    sig.m_values[4] = static_cast<unsigned>(below ? 1 : 0);
+    sig.m_values[5] = static_cast<unsigned>(plane_type);
+    return insert_new_impl(sig);
+}
+
+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);
+    sig.m_values[2] = static_cast<unsigned>(x_var);
+    sig.m_values[3] = static_cast<unsigned>(y_var);
+    sig.m_values[4] = static_cast<unsigned>(below ? 1 : 0);
+    // No plane_type parameter, so leave m_values[5] as 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";);

src/math/lp/nla_throttle.h

@@ -17,8 +17,9 @@ class nla_throttle {
 public:
     enum throttle_kind {
         ORDER_LEMMA,            // order lemma (9 params)
-        BINOMIAL_SIGN_LEMMA,    // binomial sign (5 params) 
-        MONOTONE_LEMMA          // monotonicity (2 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)
     };
 
 private:
@@ -50,51 +51,24 @@ private:
     
 public:
     nla_throttle(trail_stack& trail) : m_trail(trail) {}
-    
       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) {
-        if (!m_enabled) return false;
-        signature sig;
-        sig.m_values[0] = static_cast<unsigned>(k);
-        sig.m_values[1] = static_cast<unsigned>(mvar);
-        sig.m_values[2] = static_cast<unsigned>(is_lt);
-        return insert_new_impl(sig);
-    }
+    bool insert_new(throttle_kind k, lpvar mvar, bool is_lt);
     
     // Binomial sign: xy_var + x + y + sign + sy
-    bool 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);
-        sig.m_values[2] = static_cast<unsigned>(x);
-        sig.m_values[3] = static_cast<unsigned>(y);
-        sig.m_values[4] = normalize_sign(sign);
-        sig.m_values[5] = normalize_sign(sy);
-        return insert_new_impl(sig);
-    }
+    bool insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, int sign, int sy);
     
     // Order lemma: ac_var + a + c_sign + c + bd_var + b_var + d_sign + d + ab_cmp
     bool 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);
-        sig.m_values[2] = static_cast<unsigned>(a);
-        sig.m_values[3] = pack_rational_sign(c_sign);
-        sig.m_values[4] = static_cast<unsigned>(c);
-        sig.m_values[5] = static_cast<unsigned>(bd_var);
-        sig.m_values[6] = static_cast<unsigned>(b_var);
-        // Pack d_sign, d, and ab_cmp into the last slot
-        sig.m_values[7] = (pack_rational_sign(d_sign) << 24) | 
-                         ((static_cast<unsigned>(d) & 0xFFFF) << 8) |
-                         (static_cast<unsigned>(ab_cmp) & 0xFF);
-        return insert_new_impl(sig);
-    }
+                    lpvar bd_var, lpvar b_var, const rational& d_sign, lpvar d, llc ab_cmp);
+    
+    // Tangent lemma: monic_var + x_var + y_var + below + plane_type
+    bool insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below, int plane_type);
+    
+    // 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);
 
 private:
     bool insert_new_impl(const signature& sig);
@@ -107,6 +81,7 @@ private:
     static unsigned normalize_sign(int sign) {
         return static_cast<unsigned>(sign + 127);
     }
+    
 };
 
 }