mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix the signs for factorns in tangent lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-17 12:17:43 -07:00
parent 4c5c17c7d8
commit 146489ff14
2 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/nla_core.cpp
View file

@ -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 << "*";
}

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

@ -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