mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

add throttling to generate_plane1/2

Browse source
This commit is contained in:
Lev Nachmanson 2025-06-26 13:26:26 -07:00 • committed by Lev Nachmanson
parent ac34dbd030
commit 9e52a38580
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nla_tangent_lemmas.cpp
View file

@ -94,6 +94,10 @@ private:
} }
void generate_line1() { 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"); 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()) // 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)); lemma |= ineq(m_jx, llc::NE, c().val(m_jx));
@ -101,7 +105,11 @@ private:
explain(lemma); 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_builder lemma(c(), "tangent line 2");
lemma |= ineq(m_jy, llc::NE, c().val(m_jy)); 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); lemma |= ineq(lp::lar_term(m_j, - m_x.rat_sign() * m_xy.y, m_jx), llc::EQ, 0);