consolidate throttling

Author: levnach

src/math/lp/CMakeLists.txt

@@ -34,6 +34,7 @@ z3_add_component(lp
     nla_powers.cpp
     nla_solver.cpp
     nla_tangent_lemmas.cpp
+    nla_throttle.cpp
     nra_solver.cpp    
     permutation_matrix.cpp
     random_updater.cpp      

src/math/lp/nla_core.cpp

@@ -37,10 +37,12 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
     m_horner(this),
     m_grobner(this),
     m_emons(m_evars),
+    m_throttle(lra.trail()),
     m_use_nra_model(false),
     m_nra(s, m_nra_lim, *this) 
 {
      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

@@ -28,6 +28,7 @@
 #include "math/lp/nla_intervals.h"
 #include "nlsat/nlsat_solver.h"
 #include "params/smt_params_helper.hpp"
+#include "math/lp/nla_throttle.h"
 
 namespace nra {
     class solver;
@@ -102,6 +103,9 @@ class core {
     lpvar                    m_patched_var = 0;
     monic const*             m_patched_monic = nullptr; 
 
+    nla_throttle             m_throttle;
+    bool                     m_throttle_enabled = true;
+
 
 
     void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
@@ -432,6 +436,11 @@ 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; }
+
 };  // end of core
 
 struct pp_mon {

src/math/lp/nla_throttle.cpp

@@ -0,0 +1,24 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Author:
+    Lev Nachmanson (levnach)
+
+  --*/
+#include "math/lp/nla_throttle.h"
+#include "util/trace.h"
+
+namespace nla {
+
+bool nla_throttle::insert_new_impl(const signature& sig) {
+    if (m_seen.contains(sig)) {
+        TRACE(nla_solver, tout << "throttled lemma generation\n";);
+        return true;  // Already seen, throttle
+    }
+    
+    m_seen.insert(sig);
+    m_trail.push(insert_map(m_seen, sig));
+    return false;     // New, don't throttle
+}
+
+} // namespace nla

src/math/lp/nla_throttle.h

@@ -0,0 +1,112 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Author:
+    Lev Nachmanson (levnach)
+
+  --*/
+#pragma once
+#include "math/lp/nla_defs.h"
+#include "util/hashtable.h"
+#include "util/trail.h"
+#include <cstring>
+
+namespace nla {
+
+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)
+    };
+
+private:
+    struct signature {
+        unsigned m_values[8];
+        
+        signature() { 
+            std::memset(m_values, 0, sizeof(m_values)); 
+        }
+        
+        bool operator==(const signature& other) const {
+            return std::memcmp(m_values, other.m_values, sizeof(m_values)) == 0;
+        }
+    };
+    
+    struct signature_hash {
+        unsigned operator()(const signature& s) const {
+            unsigned hash = 0;
+            for (int i = 0; i < 8; i++) {
+                hash = combine_hash(hash, s.m_values[i]);
+            }
+            return hash;
+        }
+    };
+    
+    hashtable<signature, signature_hash, default_eq<signature>> m_seen;
+    trail_stack& m_trail;
+    bool m_enabled = true;
+    
+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);
+    }
+    
+    // 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);
+    }
+    
+    // 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);
+    }
+
+private:
+    bool insert_new_impl(const signature& sig);
+    
+    // Helper functions for packing values
+    static unsigned pack_rational_sign(const rational& r) {
+        return r.is_pos() ? 1 : (r.is_neg() ? 255 : 0);
+    }
+    
+    static unsigned normalize_sign(int sign) {
+        return static_cast<unsigned>(sign + 127);
+    }
+};
+
+}