throttle lemmas in nla_solver untested

Author: levnach

src/math/lp/dioph_eq.cpp

@@ -2542,7 +2542,7 @@ namespace lp {
     public:
 
         void explain(explanation& ex) {
-            SASSERT(ex.empty());
+            ex.clear();
             if (has_conflict_index()) {
                 TRACE(dio, print_entry(m_normalize_conflict_index, tout << "conflict:", true) << std::endl;);
                 for (auto ci : lra.flatten(explain_fixed_in_meta_term(m_l_matrix.m_rows[m_normalize_conflict_index], m_normalize_conflict_gcd)))

src/math/lp/explanation.h

@@ -70,7 +70,7 @@ class explanation {
         }
     }
 
-    bool empty() const {  return m_vector.empty() || m_set.empty();  }
+    bool empty() const {  return m_vector.empty() && m_set.empty();  }
     size_t size() const { return std::max(m_vector.size(), m_set.size()); }
 
     class cimpq {

src/math/lp/nla_core.cpp

@@ -1040,7 +1040,7 @@ rational core::val(const factorization& f) const {
     return r;
 }
 
-lemma_builder::lemma_builder(core& c, char const* name):name(name), c(c) {
+lemma_builder::lemma_builder(core& c, const char* name):name(name), c(c) {
     c.m_lemmas.push_back(lemma());
 }
 

src/math/lp/nla_monotone_lemmas.cpp

@@ -7,10 +7,30 @@
   --*/
 #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, const std::string& debug_location) {
+    // 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 at " << debug_location << "\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();
@@ -29,7 +49,13 @@ void monotone::monotonicity_lemma(monic const& m) {
        return;
     const rational prod_val = abs(c().product_value(m));
     const rational m_val = abs(var_val(m));
-    if (m_val < prod_val)
+    bool is_lt = m_val < prod_val;
+    
+    // Check if this specific combination should be throttled
+    if (throttle_monotone(m, is_lt, __FUNCTION__))
+        return;
+    
+    if (is_lt)
         monotonicity_lemma_lt(m);
     else if (m_val > prod_val)
         monotonicity_lemma_gt(m);

src/math/lp/nla_monotone_lemmas.h

@@ -6,13 +6,43 @@
    Nikolaj Bjorner (nbjorner)
   --*/
 #pragma once
+#include "util/hashtable.h"
+#include "util/hash.h"
+
 namespace nla {
     class core;
     class monotone : common {    
     public:
         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, const std::string& debug_location);
+        
         void monotonicity_lemma(monic const& m);
         void monotonicity_lemma_gt(const monic& m);    
         void monotonicity_lemma_lt(const monic& m);

src/math/lp/nla_order_lemmas.cpp

@@ -84,52 +84,59 @@ void order::order_lemma_on_binomial(const monic& ac) {
 void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
     if (!c().var_is_int(x) && val(x).is_big())
         return;
-    // throttle!!!
+    
 
     SASSERT(!_().mon_has_zero(xy.vars()));
     int sy = rat_sign(val(y));
+    // throttle here 
+    if (throttle_binomial_sign(xy, x, y, sign, sy, __FUNCTION__)) 
+        return;
+    
     lemma_builder lemma(c(), __FUNCTION__);
     lemma |= ineq(y,                                   sy == 1      ? llc::LE : llc::GE, 0); // negate sy
     lemma |= ineq(x,                                   sy*sign == 1 ? llc::GT : llc::LT , val(x)); 
     lemma |= ineq(term(xy.var(), - val(x), y), sign == 1    ? llc::LE : llc::GE, 0);
 }
 
-bool order::throttle_monic(const monic& ac, std::string const & debug_location ) { // todo - remove debug location!
+bool order::throttle_mon_ol(const monic& ac, lpvar a, const rational& c_sign, lpvar c_var,
+                           const monic& bd, const factor& b, const rational& d_sign, 
+                           lpvar d, llc ab_cmp, const std::string& debug_location) {
     // Check if throttling is enabled
     if (!c().params().arith_nl_thrl())
         return false;
 
-    // Check if this monic has already been processed using its variable ID
-    if (m_processed_monics.contains(ac.var())) {
-        TRACE(nla_solver, tout << "throttled at " << debug_location << "\n";);
+    // Create the key for this specific generate_mon_ol invocation
+    mon_ol_key key(ac.var(), a, c_sign, c_var, bd.var(), b.var(), d_sign, d, ab_cmp);
+    
+    // Check if this combination has already been processed
+    if (m_processed_mon_ol.contains(key)) {
+        TRACE(nla_solver, tout << "throttled generate_mon_ol at " << debug_location << "\n";);
         return true;
     }
 
-    // Mark this monic as processed and add to trail for backtracking
-    m_processed_monics.insert(ac.var());
-    c().trail().push(insert_map(m_processed_monics, ac.var()));
+    // Mark this combination as processed and add to trail for backtracking
+    m_processed_mon_ol.insert(key);
+    c().trail().push(insert_map(m_processed_mon_ol, key));
     return false;
 }
 
-bool order::throttle_mon_ol(const monic& ac, lpvar a, const rational& c_sign, lpvar c_var,
-                           const monic& bd, const factor& b, const rational& d_sign, 
-                           lpvar d, llc ab_cmp, const std::string& debug_location) {
+bool order::throttle_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign, int sy, const std::string& debug_location) {
     // Check if throttling is enabled
     if (!c().params().arith_nl_thrl())
         return false;
 
-    // Create the key for this specific generate_mon_ol invocation
-    mon_ol_key key(ac.var(), a, c_sign, c_var, bd.var(), b.var(), d_sign, d, ab_cmp);
+    // Create the key for this specific order_lemma_on_binomial_sign invocation
+    binomial_sign_key key(xy.var(), x, y, sign, sy);
 
     // Check if this combination has already been processed
-    if (m_processed_mon_ol.contains(key)) {
-        TRACE(nla_solver, tout << "throttled generate_mon_ol at " << debug_location << "\n";);
+    if (m_processed_binomial_sign.contains(key)) {
+        TRACE(nla_solver, tout << "throttled order_lemma_on_binomial_sign at " << debug_location << "\n";);
         return true;
     }
 
     // Mark this combination as processed and add to trail for backtracking
-    m_processed_mon_ol.insert(key);
-    c().trail().push(insert_map(m_processed_mon_ol, key));
+    m_processed_binomial_sign.insert(key);
+    c().trail().push(insert_map(m_processed_binomial_sign, key));
     return false;
 }
 

src/math/lp/nla_order_lemmas.h

@@ -21,24 +21,29 @@ class order: common {
     void order_lemma();
 
     // Structure to represent the key parameters for throttling generate_mon_ol
+    // Optimized for memory efficiency with packed fields
     struct mon_ol_key {
-        lpvar ac_var;
-        lpvar a;
-        rational c_sign;
-        lpvar c;
-        lpvar bd_var;
-        lpvar b_var;
-        rational d_sign;
-        lpvar d;
-        llc ab_cmp;
+        short ac_var;
+        short a;
+        signed char c_sign;  // -1, 0, 1 fits in signed char
+        short c;
+        short bd_var;
+        short b_var;
+        signed char d_sign;  // -1, 0, 1 fits in signed char  
+        short d;
+        unsigned char ab_cmp;  // llc enum fits in unsigned char
 
         // Default constructor for hashtable
-        mon_ol_key() : ac_var(0), a(0), c_sign(0), c(0), bd_var(0), b_var(0), d_sign(0), d(0), ab_cmp(llc::EQ) {}
+        mon_ol_key() : ac_var(0), a(0), c_sign(0), c(0), bd_var(0), b_var(0), d_sign(0), d(0), ab_cmp(static_cast<unsigned char>(llc::EQ)) {}
 
-        mon_ol_key(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)
-            : ac_var(ac_var), a(a), c_sign(c_sign), c(c), bd_var(bd_var), 
-              b_var(b_var), d_sign(d_sign), d(d), ab_cmp(ab_cmp) {}
+        mon_ol_key(lpvar ac_var, lpvar a, const rational& c_sign_rat, lpvar c,
+                   lpvar bd_var, lpvar b_var, const rational& d_sign_rat, lpvar d, llc ab_cmp)
+            : ac_var(static_cast<short>(ac_var)), a(static_cast<short>(a)), 
+              c_sign(c_sign_rat.is_pos() ? 1 : (c_sign_rat.is_neg() ? -1 : 0)), 
+              c(static_cast<short>(c)), bd_var(static_cast<short>(bd_var)), 
+              b_var(static_cast<short>(b_var)), 
+              d_sign(d_sign_rat.is_pos() ? 1 : (d_sign_rat.is_neg() ? -1 : 0)), 
+              d(static_cast<short>(d)), ab_cmp(static_cast<unsigned char>(ab_cmp)) {}
 
         bool operator==(const mon_ol_key& other) const {
             return ac_var == other.ac_var && a == other.a && c_sign == other.c_sign &&
@@ -49,13 +54,16 @@ class order: common {
 
     struct mon_ol_key_hash {
         unsigned operator()(const mon_ol_key& k) const {
-            return combine_hash(combine_hash(combine_hash(combine_hash(
-                   combine_hash(combine_hash(combine_hash(combine_hash(
-                   static_cast<unsigned>(k.ac_var), static_cast<unsigned>(k.a)),
-                   k.c_sign.hash()), static_cast<unsigned>(k.c)),
-                   static_cast<unsigned>(k.bd_var)), static_cast<unsigned>(k.b_var)),
-                   k.d_sign.hash()), static_cast<unsigned>(k.d)),
-                   static_cast<unsigned>(k.ab_cmp));
+            // Optimized hash with better distribution using bit shifts
+            unsigned h1 = (static_cast<unsigned>(k.ac_var) << 16) | static_cast<unsigned>(k.a);
+            unsigned h2 = (static_cast<unsigned>(k.c_sign + 1) << 24) | 
+                         (static_cast<unsigned>(k.c) << 8) | static_cast<unsigned>(k.bd_var);
+            unsigned h3 = (static_cast<unsigned>(k.b_var) << 16) | 
+                         ((static_cast<unsigned>(k.d_sign + 1) << 8)) | 
+                         static_cast<unsigned>(k.d);
+            unsigned h4 = static_cast<unsigned>(k.ab_cmp);
+            
+            return combine_hash(combine_hash(h1, h2), combine_hash(h3, h4));
         }
     };
 
@@ -64,8 +72,44 @@ class order: common {
                          const monic& bd, const factor& b, const rational& d_sign, 
                          lpvar d, llc ab_cmp, const std::string& debug_location);
 
-    int_hashtable<int_hash, default_eq<int>> m_processed_monics;
-    bool throttle_monic(const monic&, const std::string & debug_location);
+    // Structure to represent the key parameters for throttling order_lemma_on_binomial_sign
+    // Optimized for memory efficiency with packed fields
+    struct binomial_sign_key {
+        short xy_var;
+        short x;
+        short y;
+        signed char sign;
+        signed char sy;
+        
+        // Default constructor for hashtable
+        binomial_sign_key() : xy_var(0), x(0), y(0), sign(0), sy(0) {}
+        
+        binomial_sign_key(lpvar xy_var, lpvar x, lpvar y, int sign, int sy)
+            : xy_var(static_cast<short>(xy_var)), x(static_cast<short>(x)), 
+              y(static_cast<short>(y)), sign(static_cast<signed char>(sign)), 
+              sy(static_cast<signed char>(sy)) {}
+              
+        bool operator==(const binomial_sign_key& other) const {
+            return xy_var == other.xy_var && x == other.x && y == other.y &&
+                   sign == other.sign && sy == other.sy;
+        }
+    };
+    
+    struct binomial_sign_key_hash {
+        unsigned operator()(const binomial_sign_key& k) const {
+            // Optimized hash with better distribution 
+            unsigned h1 = (static_cast<unsigned>(k.xy_var) << 16) | static_cast<unsigned>(k.x);
+            unsigned h2 = (static_cast<unsigned>(k.y) << 16) | 
+                         ((static_cast<unsigned>(k.sign + 127) << 8)) |  // shift sign to positive range
+                         static_cast<unsigned>(k.sy + 127);               // shift sy to positive range
+            
+            return combine_hash(h1, h2);
+        }
+    };
+    
+    hashtable<binomial_sign_key, binomial_sign_key_hash, default_eq<binomial_sign_key>> m_processed_binomial_sign;
+    bool throttle_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign, int sy, const std::string& debug_location);
+    
    private:
 
     bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,

src/math/lp/nla_solver.cpp

@@ -107,9 +107,9 @@ namespace nla {
     void solver::check_bounded_divisions() {
         m_core->check_bounded_divisions();
     }
-    //return only the non-empty lemmas
-    solver::non_empty_lemmas_range solver::lemmas() const {
-        return non_empty_lemmas_range(m_core->lemmas());
+
+    const vector<lemma>&  solver::lemmas() const {
+        return m_core->lemmas();
     }
 
     vector<nla::ineq> const& solver::literals() const {

src/math/lp/nla_solver.h

@@ -54,63 +54,7 @@ namespace nla {
         vector<lp::equality> const& equalities() const;
         bool should_check_feasible() const { return m_core->should_check_feasible(); }
 
-        // Iterator class for filtering out empty lemmas
-        class non_empty_lemma_iterator {
-            vector<nla::lemma>::const_iterator current_;
-            vector<nla::lemma>::const_iterator end_;
-            
-            void advance_to_non_empty() {
-                while (current_ != end_ && current_->is_empty()) {
-                    std::cout << "skip\n";
-                    ++current_;
-                }
-            }
-            
-        public:
-            non_empty_lemma_iterator(vector<nla::lemma>::const_iterator start, 
-                                   vector<nla::lemma>::const_iterator end) 
-                : current_(start), end_(end) {
-                advance_to_non_empty();
-            }
-            
-            const nla::lemma& operator*() const { return *current_; }
-            const nla::lemma* operator->() const { return &*current_; }
-            
-            non_empty_lemma_iterator& operator++() {
-                ++current_;
-                advance_to_non_empty();
-                return *this;
-            }
-            
-            bool operator!=(const non_empty_lemma_iterator& other) const {
-                return current_ != other.current_;
-            }
-            
-            bool operator==(const non_empty_lemma_iterator& other) const {
-                return current_ == other.current_;
-            }
-        };
-        
-        // Helper class to provide range-based iteration over non-empty lemmas
-        class non_empty_lemmas_range {
-            const vector<nla::lemma>& lemmas_;
-        public:
-            non_empty_lemmas_range(const vector<nla::lemma>& lemmas) : lemmas_(lemmas) {}
-            
-            non_empty_lemma_iterator begin() const {
-                return non_empty_lemma_iterator(lemmas_.begin(), lemmas_.end());
-            }
-            
-            non_empty_lemma_iterator end() const {
-                return non_empty_lemma_iterator(lemmas_.end(), lemmas_.end());
-            }
-            
-            bool empty() const {
-                return begin() == end();
-            }
-        };
-        
-        non_empty_lemmas_range lemmas() const;
+        const vector<nla::lemma>&  lemmas() const;
 
     };
 }