From 5caa7f1a29ee4dcc4198e90cd7701f8111c01f0f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 25 Jun 2025 17:27:53 -0700 Subject: [PATCH] throttle lemmas in nla_solver untested --- src/math/lp/dioph_eq.cpp | 2 +- src/math/lp/explanation.h | 2 +- src/math/lp/nla_core.cpp | 2 +- src/math/lp/nla_monotone_lemmas.cpp | 28 ++++++++- src/math/lp/nla_monotone_lemmas.h | 30 ++++++++++ src/math/lp/nla_order_lemmas.cpp | 43 ++++++++------ src/math/lp/nla_order_lemmas.h | 90 +++++++++++++++++++++-------- src/math/lp/nla_solver.cpp | 6 +- src/math/lp/nla_solver.h | 58 +------------------ 9 files changed, 156 insertions(+), 105 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index f97363ecd..a791cbd07 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/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))) diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index 850e59cd4..732ce9251 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -70,7 +70,7 @@ public: } } - 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 { diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 83e573b14..4c79b5926 100644 --- a/src/math/lp/nla_core.cpp +++ b/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()); } diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index e09d1717e..b14e2a63f 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/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); diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index fb9c469a8..f872707cd 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/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(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(k.mvar), + static_cast(k.is_lt)); + } + }; + private: + hashtable> 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); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index b07e8a331..dbab886ce 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -84,33 +84,20 @@ 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! - // 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";); - 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())); - 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) { @@ -133,6 +120,26 @@ bool order::throttle_mon_ol(const monic& ac, lpvar a, const rational& c_sign, lp return false; } +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 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_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_binomial_sign.insert(key); + c().trail().push(insert_map(m_processed_binomial_sign, key)); + return false; +} + // We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and e void order::order_lemma_on_factor_binomial_explore(const monic& ac, bool k) { TRACE(nla_solver, tout << "ac = " << pp_mon_with_vars(c(), ac);); diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 20fa35bce..7da8ece5a 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -21,24 +21,29 @@ public: 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(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(ac_var)), a(static_cast(a)), + c_sign(c_sign_rat.is_pos() ? 1 : (c_sign_rat.is_neg() ? -1 : 0)), + c(static_cast(c)), bd_var(static_cast(bd_var)), + b_var(static_cast(b_var)), + d_sign(d_sign_rat.is_pos() ? 1 : (d_sign_rat.is_neg() ? -1 : 0)), + d(static_cast(d)), ab_cmp(static_cast(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 @@ public: 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(k.ac_var), static_cast(k.a)), - k.c_sign.hash()), static_cast(k.c)), - static_cast(k.bd_var)), static_cast(k.b_var)), - k.d_sign.hash()), static_cast(k.d)), - static_cast(k.ab_cmp)); + // Optimized hash with better distribution using bit shifts + unsigned h1 = (static_cast(k.ac_var) << 16) | static_cast(k.a); + unsigned h2 = (static_cast(k.c_sign + 1) << 24) | + (static_cast(k.c) << 8) | static_cast(k.bd_var); + unsigned h3 = (static_cast(k.b_var) << 16) | + ((static_cast(k.d_sign + 1) << 8)) | + static_cast(k.d); + unsigned h4 = static_cast(k.ab_cmp); + + return combine_hash(combine_hash(h1, h2), combine_hash(h3, h4)); } }; @@ -64,8 +72,44 @@ public: const monic& bd, const factor& b, const rational& d_sign, lpvar d, llc ab_cmp, const std::string& debug_location); - int_hashtable> 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(xy_var)), x(static_cast(x)), + y(static_cast(y)), sign(static_cast(sign)), + sy(static_cast(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(k.xy_var) << 16) | static_cast(k.x); + unsigned h2 = (static_cast(k.y) << 16) | + ((static_cast(k.sign + 127) << 8)) | // shift sign to positive range + static_cast(k.sy + 127); // shift sy to positive range + + return combine_hash(h1, h2); + } + }; + + hashtable> 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, diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 97ca8dd1d..793789f8f 100644 --- a/src/math/lp/nla_solver.cpp +++ b/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& solver::lemmas() const { + return m_core->lemmas(); } vector const& solver::literals() const { diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index d85399958..57016927b 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -54,63 +54,7 @@ namespace nla { vector 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::const_iterator current_; - vector::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::const_iterator start, - vector::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& lemmas_; - public: - non_empty_lemmas_range(const vector& 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& lemmas() const; }; }