diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 70566e80a..252bbecd3 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -89,55 +89,13 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int SASSERT(!_().mon_has_zero(xy.vars())); int sy = rat_sign(val(y)); // throttle here - if (throttle_binomial_sign(xy, x, y, sign, sy)) + if (c().throttle().insert_new(nla_throttle::BINOMIAL_SIGN_LEMMA, xy.var(), x, y, sign, sy)) 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_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) { - // 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); - - // Check if this combination has already been processed - if (m_processed_mon_ol.contains(key)) { - TRACE(nla_solver, tout << "throttled generate_mon_ol\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)); - return false; -} - -bool order::throttle_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign, int sy) { - // 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\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; + lemma |= ineq(lp::lar_term(xy.var(), - val(x), y), sign == 1 ? llc::LE : llc::GE, 0); } // We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and e @@ -206,7 +164,7 @@ void order::order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic& void order::generate_mon_ol(const monic& ac, lpvar a, const rational& c_sign, - lpvar c, + lpvar c_par, const monic& bd, const factor& b, const rational& d_sign, @@ -217,14 +175,14 @@ void order::generate_mon_ol(const monic& ac, SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign)); // Check if this specific combination should be throttled - if (throttle_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, ab_cmp)) + if (c().throttle().insert_new(nla_throttle::ORDER_LEMMA, ac.var(), a, c_sign, c_par, bd.var(), b.var(), d_sign, d, ab_cmp)) return; lemma_builder lemma(_(), __FUNCTION__); - lemma |= ineq(term(c_sign, c), llc::LE, 0); - lemma &= c; // this explains c == +- d - lemma |= ineq(term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0); - lemma |= ineq(term(ac.var(), rational(-1), var(bd)), ab_cmp, 0); + lemma |= ineq(lp::lar_term(c_sign, c_par), llc::LE, 0); + lemma &= c_par; // this explains c_par == +- d + lemma |= ineq(lp::lar_term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0); + lemma |= ineq(lp::lar_term(rational(1), ac.var(), rational(-1), var(bd)), ab_cmp, 0); lemma &= bd; lemma &= b; lemma &= d; @@ -367,7 +325,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, const monic& bc, const factor& b) { SASSERT(!val(c).is_zero()); - rational c_sign = rational(nla::rat_sign(val(c))); + rational c_sign = rational(rat_sign(val(c))); auto av_c_s = val(a) * c_sign; auto bv_c_s = val(b) * c_sign; if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s) || diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 021c96682..8d4360aa8 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -9,8 +9,6 @@ #pragma once #include "math/lp/factorization.h" #include "math/lp/nla_common.h" -#include "util/hashtable.h" -#include "util/hash.h" namespace nla { class core; @@ -20,96 +18,6 @@ public: order(core *c) : common(c) {} 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 { - 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(static_cast(llc::EQ)) {} - - 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 && - c == other.c && bd_var == other.bd_var && b_var == other.b_var && - d_sign == other.d_sign && d == other.d && ab_cmp == other.ab_cmp; - } - }; - - struct mon_ol_key_hash { - unsigned operator()(const mon_ol_key& k) const { - // 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)); - } - }; - - hashtable> m_processed_mon_ol; - bool 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); - - // 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); - private: bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,