diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index b14e2a63f..6c0c05fa3 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -12,7 +12,7 @@ namespace nla { monotone::monotone(core * c) : common(c) {} -bool monotone::throttle_monotone(const monic& m, bool is_lt, const std::string& debug_location) { +bool monotone::throttle_monotone(const monic& m, bool is_lt) { // Check if throttling is enabled if (!c().params().arith_nl_thrl()) return false; @@ -22,7 +22,7 @@ bool monotone::throttle_monotone(const monic& m, bool is_lt, const std::string& // 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";); + TRACE(nla_solver, tout << "throttled monotonicity_lemma\n";); return true; } @@ -52,7 +52,7 @@ void monotone::monotonicity_lemma(monic const& m) { bool is_lt = m_val < prod_val; // Check if this specific combination should be throttled - if (throttle_monotone(m, is_lt, __FUNCTION__)) + if (throttle_monotone(m, is_lt)) return; if (is_lt) diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index f872707cd..17f540857 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/src/math/lp/nla_monotone_lemmas.h @@ -41,7 +41,7 @@ namespace nla { private: hashtable> m_processed_monotone; - bool throttle_monotone(const monic& m, bool is_lt, const std::string& debug_location); + bool throttle_monotone(const monic& m, bool is_lt); void monotonicity_lemma(monic const& m); void monotonicity_lemma_gt(const monic& m); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index dbab886ce..70566e80a 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -89,7 +89,7 @@ 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, __FUNCTION__)) + if (throttle_binomial_sign(xy, x, y, sign, sy)) return; lemma_builder lemma(c(), __FUNCTION__); @@ -100,7 +100,7 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int 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) { + lpvar d, llc ab_cmp) { // Check if throttling is enabled if (!c().params().arith_nl_thrl()) return false; @@ -110,7 +110,7 @@ bool order::throttle_mon_ol(const monic& ac, lpvar a, const rational& c_sign, lp // 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";); + TRACE(nla_solver, tout << "throttled generate_mon_ol\n";); return true; } @@ -120,7 +120,7 @@ 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) { +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; @@ -130,7 +130,7 @@ bool order::throttle_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign, // 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";); + TRACE(nla_solver, tout << "throttled order_lemma_on_binomial_sign\n";); return true; } @@ -217,7 +217,7 @@ 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, __FUNCTION__)) + if (throttle_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, ab_cmp)) return; lemma_builder lemma(_(), __FUNCTION__); diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 7da8ece5a..021c96682 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -70,7 +70,7 @@ public: 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, const std::string& debug_location); + 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 @@ -108,7 +108,7 @@ public: }; 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); + bool throttle_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign, int sy); private: