From 9e52a38580fece077ec75caf98cbe37f05d60ff5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 26 Jun 2025 13:26:26 -0700 Subject: [PATCH] add throttling to generate_plane1/2 --- src/math/lp/nla_tangent_lemmas.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index cec01da59..91676b660 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -94,6 +94,10 @@ private: } void generate_line1() { + // Use plane_type 1 to distinguish line1 from other tangent lemmas + if (c().throttle().insert_new(nla_throttle::TANGENT_LEMMA, m_j, m_jx, m_jy, m_below, 1)) + return; + lemma_builder lemma(c(), "tangent line 1"); // Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var()) lemma |= ineq(m_jx, llc::NE, c().val(m_jx)); @@ -101,7 +105,11 @@ private: explain(lemma); } - void generate_line2() { + void generate_line2() { + // Use plane_type 2 to distinguish line2 from other tangent lemmas + if (c().throttle().insert_new(nla_throttle::TANGENT_LEMMA, m_j, m_jx, m_jy, m_below, 2)) + return; + lemma_builder lemma(c(), "tangent line 2"); lemma |= ineq(m_jy, llc::NE, c().val(m_jy)); lemma |= ineq(lp::lar_term(m_j, - m_x.rat_sign() * m_xy.y, m_jx), llc::EQ, 0);