From 146489ff14ab888afbc966aec9dba11b3495bafb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Mar 2020 12:17:43 -0700 Subject: [PATCH] fix the signs for factorns in tangent lemma Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 3 ++- src/math/lp/nla_tangent_lemmas.cpp | 22 ++++++++++++---------- 2 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 40adc33d2..3d3c2efae 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -699,7 +699,8 @@ std::ostream & core::print_factorization(const factorization& f, std::ostream& o } else { for (unsigned k = 0; k < f.size(); k++ ) { - print_factor(f[k], out); + out << "("; + print_factor(f[k], out) << ")"; if (k < f.size() - 1) out << "*"; } diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 1e9eae494..aa6d7c9d6 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -76,10 +76,11 @@ struct imp { void generate_tang_plane(const point & pl) { c().add_empty_lemma(); - c().negate_relation(m_jx, pl.x); - c().negate_relation(m_jy, pl.y); + c().negate_relation(m_jx, m_x.rat_sign()*pl.x); + c().negate_relation(m_jy, m_y.rat_sign()*pl.y); #if Z3DEBUG - int mult_sign = nla::rat_sign(pl.x - c().val(m_jx))*nla::rat_sign(pl.y - c().val(m_jy)); + SASSERT(c().val(m_x) == m_xy.x && c().val(m_y) == m_xy.y); + int mult_sign = nla::rat_sign(pl.x - m_xy.x)*nla::rat_sign(pl.y - m_xy.y); SASSERT((mult_sign == 1) == m_below); // If "mult_sign is 1" then (a - x)(b-y) > 0 and ab - bx - ay + xy > 0 // or -ab + bx + ay < xy or -ay - bx + xy > -ab @@ -87,20 +88,21 @@ struct imp { #endif lp::lar_term t; - t.add_monomial(- pl.x, m_jy); - t.add_monomial(- pl.y, m_jx); + t.add_monomial(- m_y.rat_sign()*pl.x, m_jy); + t.add_monomial(- m_x.rat_sign()*pl.y, m_jx); t.add_var(m_j); c().mk_ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y); } void generate_two_tang_lines() { m_tang.add_empty_lemma(); - c().mk_ineq(m_jx, llc::NE, m_xy.x); - c().mk_ineq(m_j, - m_xy.x, m_jy, llc::EQ); + // Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var()) + c().mk_ineq(m_jx, llc::NE, c().val(m_jx)); + c().mk_ineq(m_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ); m_tang.add_empty_lemma(); - c().mk_ineq(m_jy, llc::NE, m_xy.y); - c().mk_ineq(m_j, - m_xy.y, m_jx, llc::EQ); + c().mk_ineq(m_jy, llc::NE, c().val(m_jy)); + c().mk_ineq(m_j, - m_x.rat_sign() * m_xy.y, m_jx, llc::EQ); } // Get two planes tangent to surface z = xy, one at point a, and another at point b, creating a cut void get_initial_tang_points() { @@ -116,7 +118,7 @@ struct imp { m_b = point(x + delta, y - delta); } else { - // denote x = xy.x and y = xy.y, and vx, vy - the value of x and y. + // denote x = xy.x and y = xy.y, and vx, vy - the values of x and y. // we have val(xy) < vx*y + vy*x - vx*vy = pl(x, y); // The plane with delta (1, 1) is (vx + 1)y + (vy + 1)x - (vx + 1)(vy + 1) = // vx*y + vy*x - vx*vy + y + x - xv*vy - vx - vy - 1 = pl(x, y) - 1