From 58c8f3f118bfb53664643ac45d056cf9f2bb4ee0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 19 May 2019 21:55:46 -0700 Subject: [PATCH] remove the generate_simple_tangent_lemma() Signed-off-by: Lev Nachmanson --- src/util/lp/nla_core.cpp | 103 ----------------------------- src/util/lp/nla_core.h | 1 - src/util/lp/nla_tangent_lemmas.cpp | 42 ------------ 3 files changed, 146 deletions(-) diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index ae9901c8a..08a120c17 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -1632,109 +1632,6 @@ rational core::val(const factorization& f) const { 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()))); - for (lpvar j : m.vars()) { - if (val(j).is_pos()) { - mk_ineq(j, llc::LE); - } else { - SASSERT(val(j).is_neg()); - mk_ineq(j, llc::GE); - } - } - mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT)); - TRACE("nla_solver", print_lemma(tout);); -} - -void core::generate_simple_tangent_lemma(const rooted_mon* rm) { - if (rm->size() != 2) - return; - TRACE("nla_solver", tout << "rm:"; print_rooted_monomial_with_vars(*rm, tout) << std::endl;); - add_empty_lemma(); - unsigned i_mon = rm->orig_index(); - const monomial & m = m_monomials[i_mon]; - const rational v = product_value(m); - const rational& mv = vvr(m); - SASSERT(mv != v); - SASSERT(!mv.is_zero() && !v.is_zero()); - rational sign = rational(nla::rat_sign(mv)); - if (sign != nla::rat_sign(v)) { - generate_simple_sign_lemma(-sign, m); - return; - } - bool gt = abs(mv) > abs(v); - if (gt) { - for (lpvar j : m) { - const rational & jv = vvr(j); - rational js = rational(nla::rat_sign(jv)); - mk_ineq(js, j, llc::LT); - mk_ineq(js, j, llc::GT, jv); - } - mk_ineq(sign, i_mon, llc::LT); - mk_ineq(sign, i_mon, llc::LE, v); - } else { - for (lpvar j : m) { - const rational & jv = vvr(j); - rational js = rational(nla::rat_sign(jv)); - mk_ineq(js, j, llc::LT); - mk_ineq(js, j, llc::LT, jv); - } - mk_ineq(sign, m.var(), llc::LT); - mk_ineq(sign, m.var(), llc::GE, v); - } - TRACE("nla_solver", print_lemma(tout);); -} - -void core::tangent_lemma() { - bfc bf; - lpvar j; - rational sign; - const rooted_mon* rm = nullptr; - - if (find_bfc_to_refine(bf, j, sign, rm)) { - tangent_lemma_bf(bf, j, sign, rm); - } else { - TRACE("nla_solver", tout << "cannot find a bfc to refine\n"; ); - if (rm != nullptr) - generate_simple_tangent_lemma(rm); - } -} - -void core::generate_explanations_of_tang_lemma(const rooted_mon& rm, const bfc& bf, lp::explanation& exp) { - // here we repeat the same explanation for each lemma - explain(rm, exp); - explain(bf.m_x, exp); - explain(bf.m_y, exp); -} - -void core::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const rooted_mon* rm){ - point a, b; - point xy (vvr(bf.m_x), vvr(bf.m_y)); - rational correct_mult_val = xy.x * xy.y; - rational val = vvr(j) * sign; - bool below = val < correct_mult_val; - TRACE("nla_solver", tout << "rm = " << rm << ", below = " << below << std::endl; ); - get_tang_points(a, b, below, val, xy); - TRACE("nla_solver", tout << "sign = " << sign << ", tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;); - unsigned lemmas_size_was = m_lemma_vec->size(); - generate_two_tang_lines(bf, xy, sign, j); - generate_tang_plane(a.x, a.y, bf.m_x, bf.m_y, below, j, sign); - generate_tang_plane(b.x, b.y, bf.m_x, bf.m_y, below, j, sign); - // if rm == nullptr there is no need to explain equivs since we work on a monomial and not on a rooted monomial - if (rm != nullptr) { - lp::explanation expl; - generate_explanations_of_tang_lemma(*rm, bf, expl); - for (unsigned i = lemmas_size_was; i < m_lemma_vec->size(); i++) { - auto &l = (*m_lemma_vec)[i]; - l.expl().add(expl); - } - } - TRACE("nla_solver", - for (unsigned i = lemmas_size_was; i < m_lemma_vec->size(); i++) - print_specific_lemma((*m_lemma_vec)[i], tout); ); -} - void core::add_empty_lemma() { m_lemma_vec->push_back(lemma()); } diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h index 2e3ea4583..e6062d2fe 100644 --- a/src/util/lp/nla_core.h +++ b/src/util/lp/nla_core.h @@ -326,7 +326,6 @@ public: bool find_bfc_to_refine_on_monomial(const monomial&, factorization & bf); bool find_bfc_to_refine(const monomial* & m, factorization& bf); - void generate_simple_sign_lemma(const rational& sign, const monomial& m); void negate_relation(unsigned j, const rational& a); bool conflict_found() const; diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp index 3bb122ae2..8ae9a606c 100644 --- a/src/util/lp/nla_tangent_lemmas.cpp +++ b/src/util/lp/nla_tangent_lemmas.cpp @@ -82,7 +82,6 @@ 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, 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,47 +99,6 @@ void tangents::tangent_lemma_bf(const monomial& m, const factorization& bf){ c().print_specific_lemma((*c().m_lemma_vec)[i], tout); ); } -// 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;); - rational v = c().product_value(m.vars()); - const rational mv = val(m); - SASSERT(mv != v); - SASSERT(!mv.is_zero() && !v.is_zero()); - rational sign = rational(nla::rat_sign(mv)); - if (sign != nla::rat_sign(v)) { - 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 (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::LE); - c().mk_ineq(js, j, llc::GT, abs(jv)); - } - c().mk_ineq(sign, m.var(), llc::LT); - c().mk_ineq(sign, m.var(), llc::LE, abs(v)); - } else { - 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, abs(jv)); - } - c().mk_ineq(sign, m.var(), llc::LT); - c().mk_ineq(sign, m.var(), llc::GE, abs(v)); - } - TRACE("nla_solver", c().print_lemma(tout);); -} void tangents::generate_two_tang_lines(const factorization & bf, const point& xy, lpvar j) { add_empty_lemma();