From 56690d16da2bec23e902e97cbe9af681db936c46 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 28 Apr 2020 19:36:05 -0700 Subject: [PATCH] remove incorrect order lemmas Signed-off-by: Lev Nachmanson --- src/math/lp/nla_order_lemmas.cpp | 78 ------------------------------ src/math/lp/nla_order_lemmas.h | 13 ----- src/math/lp/nla_tangent_lemmas.cpp | 1 - 3 files changed, 92 deletions(-) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 54dda5d65..5dd8f8d8a 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -212,24 +212,8 @@ bool order::order_lemma_on_ac_and_bc(const monic& rm_ac, // We try to find a monic n = cd, such that |b| = |d| // and get a lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation void order::order_lemma_on_factorization(const monic& m, const factorization& ab) { - bool sign = m.rsign(); - for (factor f: ab) - sign ^= _().canonize_sign(f); - const rational rsign = sign_to_rat(sign); - const rational fv = val(var(ab[0])) * val(var(ab[1])); - const rational mv = rsign * var_val(m); - TRACE("nla_solver", - tout << "ab.size()=" << ab.size() << "\n"; - tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";); - if (mv == fv) - return; - bool gt = mv > fv; - SASSERT(mv != fv); TRACE("nla_solver", tout << "m="; _().print_monic_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout);); for (unsigned j = 0, k = 1; j < 2; j++, k--) { - order_lemma_on_ab(m, rsign, var(ab[k]), var(ab[j]), gt); - explain(ab); explain(m); - TRACE("nla_solver", _().print_lemma(tout);); order_lemma_on_ac_explore(m, ab, j == 1); } } @@ -332,67 +316,5 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, } return false; } -/** - \brief Add lemma: - a > 0 & b <= value(b) => sign*ab <= value(b)*a if value(a) > 0 - a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0 -*/ -void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b) { - SASSERT(sign * var_val(m) > val(a) * val(b)); - add_lemma(); - if (val(a).is_pos()) { - TRACE("nla_solver", tout << "a is pos\n";); - //negate a > 0 - mk_ineq(a, llc::LE); - // negate b <= val(b) - mk_ineq(b, llc::GT, val(b)); - // ab <= val(b)a - mk_ineq(sign, m.var(), -val(b), a, llc::LE); - } else { - TRACE("nla_solver", tout << "a is neg\n";); - SASSERT(val(a).is_neg()); - //negate a < 0 - mk_ineq(a, llc::GE); - // negate b >= val(b) - mk_ineq(b, llc::LT, val(b)); - // ab <= val(b)a - mk_ineq(sign, m.var(), -val(b), a, llc::LE); - } -} -// we need to deduce ab >= val(b)*a -/** - \brief Add lemma: - a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0 - a < 0 & b <= value(b) => sign*ab >= value(b)*a if value(a) < 0 -*/ -void order::order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b) { - TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) << - ", b = "; c().print_var(b, tout) << "\n";); - SASSERT(sign * var_val(m) < val(a) * val(b)); - add_lemma(); - if (val(a).is_pos()) { - //negate a > 0 - mk_ineq(a, llc::LE); - // negate b >= val(b) - mk_ineq(b, llc::LT, val(b)); - // ab <= val(b)a - mk_ineq(sign, m.var(), -val(b), a, llc::GE); - } else { - SASSERT(val(a).is_neg()); - //negate a < 0 - mk_ineq(a, llc::GE); - // negate b <= val(b) - mk_ineq(b, llc::GT, val(b)); - // ab >= val(b)a - mk_ineq(sign, m.var(), -val(b), a, llc::GE); - } -} - -void order::order_lemma_on_ab(const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) { - if (gt) - order_lemma_on_ab_gt(m, sign, a, b); - else - order_lemma_on_ab_lt(m, sign, a, b); -} } diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 24b7b2cb4..31aacc82e 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -48,19 +48,6 @@ private: void order_lemma_on_factorization(const monic& rm, const factorization& ab); - /** - \brief Add lemma: - a > 0 & b <= value(b) => sign*ab <= value(b)*a if value(a) > 0 - a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0 - */ - void order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b); - // we need to deduce ab >= val(b)*a - /** - \brief Add lemma: - a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0 - a < 0 & b <= value(b) => sign*ab >= value(b)*a if value(a) < 0 - */ - void order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b); void order_lemma_on_ab(const monic& m, const rational& sign, lpvar a, lpvar b, bool gt); void order_lemma_on_factor_binomial_explore(const monic& m, bool k); void order_lemma_on_factor_binomial_rm(const monic& ac, bool k, const monic& bd); diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index f8901640c..90b3d3b0e 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -64,7 +64,6 @@ struct imp { c().explain(m_x, exp); c().explain(m_y, exp); } - void generate_simple_tangent_lemma(const monic& m, const factorization&); void tangent_lemma_on_bf() { get_tang_points(); TRACE("nla_solver", tout << "tang domain = "; print_tangent_domain(tout) << std::endl;);