From f20a028f7bd877953ad2c9dc5d3b6bcb5a5aec1c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 16 May 2019 13:58:42 -0700 Subject: [PATCH] hook up generate_simple_tangent_lemma() Signed-off-by: Lev Nachmanson --- src/util/lp/nla_core.cpp | 8 +++++++ src/util/lp/nla_core.h | 2 ++ src/util/lp/nla_tangent_lemmas.cpp | 34 +++++++++++++++++------------- src/util/lp/nla_tangent_lemmas.h | 2 +- 4 files changed, 30 insertions(+), 16 deletions(-) diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index d394c8d07..ae9901c8a 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -1624,6 +1624,14 @@ bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){ return false; } +rational core::val(const factorization& f) const { + rational r(1); + for (const factor &p : f) { + r *= val(p); + } + return r; +} + void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) { add_empty_lemma(); SASSERT(sign == nla::rat_sign(product_value(m.vars()))); diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h index f369b07e8..2e3ea4583 100644 --- a/src/util/lp/nla_core.h +++ b/src/util/lp/nla_core.h @@ -108,6 +108,8 @@ public: rational val(const factor& f) const { return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); } + rational val(const factorization&) const; + lpvar var(const factor& f) const { return f.var(); } svector sorted_rvars(const factor& f) const; diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp index 17128ae26..3bb122ae2 100644 --- a/src/util/lp/nla_tangent_lemmas.cpp +++ b/src/util/lp/nla_tangent_lemmas.cpp @@ -82,7 +82,7 @@ void tangents::tangent_lemma_bf(const monomial& m, const factorization& bf){ TRACE("nla_solver", tout << "tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;); unsigned lemmas_size_was = c().m_lemma_vec->size(); rational sign(1); - generate_simple_tangent_lemma(m); + generate_simple_tangent_lemma(m, bf); generate_two_tang_lines(bf, xy, j); generate_tang_plane(a.x, a.y, bf[0], bf[1], below, j); generate_tang_plane(b.x, b.y, bf[0], bf[1], below, j); @@ -100,11 +100,12 @@ void tangents::tangent_lemma_bf(const monomial& m, const factorization& bf){ c().print_specific_lemma((*c().m_lemma_vec)[i], tout); ); } -void tangents::generate_simple_tangent_lemma(const monomial& m) { - if (m.size() != 2) - return; +// using a fact that +// a != 0 & b != 0 & |a|*|b| = c & |a'| ~ |a| & |b'| ~ |b| => |a'|*|b'| ~ c, +// where ~ is < or >. +void tangents::generate_simple_tangent_lemma(const monomial& m, const factorization& bf) { TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;); - const rational v = c().product_value(m.vars()); + rational v = c().product_value(m.vars()); const rational mv = val(m); SASSERT(mv != v); SASSERT(!mv.is_zero() && !v.is_zero()); @@ -113,30 +114,33 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) { c().generate_simple_sign_lemma(-sign, m); return; } - /* c().add_empty_lemma(); + v = val(bf); + SASSERT(rat_sign(v) == rat_sign(mv)); bool gt = abs(mv) > abs(v); + unsigned j; if (gt) { - for (lpvar j : m.vars()) { + for (const factor& f : bf) { + j = var(f); const rational jv = val(j); rational js = rational(nla::rat_sign(jv)); - c().mk_ineq(js, j, llc::LT); - c().mk_ineq(js, j, llc::GT, jv); + c().mk_ineq(js, j, llc::LE); + c().mk_ineq(js, j, llc::GT, abs(jv)); } - c().mk_ineq(sign, m.var(), llc::LE, std::max(v, rational(-1))); + c().mk_ineq(sign, m.var(), llc::LT); + c().mk_ineq(sign, m.var(), llc::LE, abs(v)); } else { - for (lpvar j : m.vars()) { + for (const factor& f : bf) { + j = var(f); const rational jv = val(j); rational js = rational(nla::rat_sign(jv)); - c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0))); + c().mk_ineq(js, j, llc::LT, abs(jv)); } c().mk_ineq(sign, m.var(), llc::LT); - c().mk_ineq(sign, m.var(), llc::GE, v); + c().mk_ineq(sign, m.var(), llc::GE, abs(v)); } TRACE("nla_solver", c().print_lemma(tout);); - */ } -// todo : consider using generate_simple_tangent_lemma on each factorization void tangents::generate_two_tang_lines(const factorization & bf, const point& xy, lpvar j) { add_empty_lemma(); diff --git a/src/util/lp/nla_tangent_lemmas.h b/src/util/lp/nla_tangent_lemmas.h index 95f2e142c..059cbea41 100644 --- a/src/util/lp/nla_tangent_lemmas.h +++ b/src/util/lp/nla_tangent_lemmas.h @@ -54,7 +54,7 @@ public: private: lpvar find_binomial_to_refine(); void generate_explanations_of_tang_lemma(const monomial& m, const factorization& bf, lp::explanation& exp); - void generate_simple_tangent_lemma(const monomial& m); + void generate_simple_tangent_lemma(const monomial& m, const factorization&); void tangent_lemma_bf(const monomial& m,const factorization& bf); void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j);