remove incorrect order lemmas

Signed-off-by: Lev Nachmanson <[email protected]>

Author: levnach

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);
-}
 
 }

src/math/lp/nla_order_lemmas.h

@@ -48,19 +48,6 @@ class order: common {
 
     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);

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;);