From 521f6a6543a0eb0d293a5a590be50aa3cf6a5171 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 20 Jun 2025 07:25:56 -0700 Subject: [PATCH] throttle tangent plane lemmas Signed-off-by: Lev Nachmanson --- src/math/lp/nla_order_lemmas.cpp | 21 ++++++++++-------- src/math/lp/nla_order_lemmas.h | 4 ++-- src/math/lp/nla_tangent_lemmas.cpp | 21 ++++++++++++++++++ src/math/lp/nla_tangent_lemmas.h | 35 +++++++++++++++++++++++++++++- 4 files changed, 69 insertions(+), 12 deletions(-) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 5a88cb4a0..a86200e1f 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -84,7 +84,7 @@ 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; - if (throttle_monic(xy)) + if (throttle_monic(xy, std::string(__FILE__)+ "," + std::to_string(__LINE__))) return; SASSERT(!_().mon_has_zero(xy.vars())); @@ -95,14 +95,16 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int lemma |= ineq(term(xy.var(), - val(x), y), sign == 1 ? llc::LE : llc::GE, 0); } -bool order::throttle_monic(const monic& ac) { +bool order::throttle_monic(const monic& ac, std::string const & debug_location ) { // Check if this monic has already been processed using its variable ID - if (m_processed_binoms.contains(ac.var())) + if (m_processed_monics.contains(ac.var())) { + std::cout << "throttled at " << debug_location << "\n"; return true; + } // Mark this monic as processed and add to trail for backtracking - m_processed_binoms.insert(ac.var()); - c().trail().push(insert_map(m_processed_binoms, ac.var())); + m_processed_monics.insert(ac.var()); + c().trail().push(insert_map(m_processed_monics, ac.var())); return false; } @@ -110,10 +112,7 @@ bool order::throttle_monic(const monic& ac) { void order::order_lemma_on_factor_binomial_explore(const monic& ac, bool k) { TRACE(nla_solver, tout << "ac = " << pp_mon_with_vars(c(), ac);); SASSERT(ac.size() == 2); - - if (throttle_monic(ac)) - return; - + lpvar c_var = ac.vars()[k]; for (monic const& bd : _().emons().get_products_of(c_var)) { @@ -363,6 +362,8 @@ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rationa lemma b != val(b) || sign*m >= a*val(b) */ void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { + if (throttle_monic(m, std::string(__FILE__)+ "," + std::to_string(__LINE__))) + return; TRACE(nla_solver, tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) << ", b = "; c().print_var(b, tout) << "\n";); SASSERT(sign * var_val(m) < val(a) * val(b)); @@ -373,6 +374,8 @@ void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rationa } void order::order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) { + if (throttle_monic(m, std::string(__FILE__)+ "," + std::to_string(__LINE__))) + return; if (gt) order_lemma_on_ab_gt(lemma, m, sign, a, b); else diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 15d6ec051..007a09789 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -20,8 +20,8 @@ public: order(core *c) : common(c) {} void order_lemma(); - int_hashtable> m_processed_binoms; - bool throttle_monic(const monic&); + int_hashtable> m_processed_monics; + bool throttle_monic(const monic&, 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_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index ff4b6f93c..5c13c4b3d 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -8,6 +8,8 @@ --*/ #include "math/lp/nla_tangent_lemmas.h" #include "math/lp/nla_core.h" +#include "util/trail.h" +#include namespace nla { @@ -70,6 +72,10 @@ private: } void generate_plane(const point & pl) { + // Throttle plane generation based on m_xy.var() and m_below + if (m_tang.throttle_plane(m_j, m_below, std::string(__FILE__) + "," + std::to_string(__LINE__))) + return; + new_lemma 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); @@ -193,5 +199,20 @@ void tangents::tangent_lemma() { } } +bool tangents::throttle_plane(unsigned var, bool below, std::string const & debug_location) { + tangent_key key(var, below); + + // Check if this (var, below) pair has already been processed + if (m_processed_planes.contains(key)) { + std::cout << "throttled plane at " << debug_location << " for var=" << var << ", below=" << below << "\n"; + return true; + } + + // Mark this (var, below) pair as processed and add to trail for backtracking + m_processed_planes.insert(key); + c().trail().push(insert_map(m_processed_planes, key)); + return false; +} + } diff --git a/src/math/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h index daa45a41a..2bcef2772 100644 --- a/src/math/lp/nla_tangent_lemmas.h +++ b/src/math/lp/nla_tangent_lemmas.h @@ -9,10 +9,37 @@ #include "util/rational.h" #include "math/lp/factorization.h" #include "math/lp/nla_common.h" +#include "util/hashtable.h" +#include "util/hash.h" namespace nla { class core; +// Key for throttling tangent plane generation: (var, below) +struct tangent_key { + unsigned var; + bool below; + + tangent_key(unsigned v, bool b) : var(v), below(b) {} + tangent_key() : var(0), below(false) {} + + bool operator==(const tangent_key& other) const { + return var == other.var && below == other.below; + } +}; + +struct tangent_key_hash { + unsigned operator()(const tangent_key& k) const { + return hash_u(k.var) ^ (k.below ? 1 : 0); + } +}; + +struct tangent_key_eq { + bool operator()(const tangent_key& a, const tangent_key& b) const { + return a == b; + } +}; + struct point { rational x; rational y; @@ -41,7 +68,13 @@ inline std::ostream& operator<<(std::ostream& out, point const& a) { return out struct tangents : common { + // Hashtable to throttle tangent plane generation + hashtable m_processed_planes; + tangents(core *core); - void tangent_lemma(); + void tangent_lemma(); + + // Throttling function similar to order::throttle_monic + bool throttle_plane(unsigned var, bool below, std::string const & debug_location); }; // end of tangents } // end of namespace