run tangent and ordered lemmas only on canonical monomials

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/util/lp/nla_core.cpp

@@ -805,12 +805,20 @@ std::ostream & core::print_factorization(const factorization& f, std::ostream& o
     return out;
 }
     
-bool core::find_canonical_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
-    SASSERT(vars_are_roots(vars));
+bool core::find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i) const {
     monomial const* sv = m_emons.find_canonical(vars);
     return sv && (i = sv->var(), true);
 }
 
+bool core::is_canonical_monomial(lpvar j) const {
+    const monomial & m = m_emons[j];
+    unsigned k;
+    SASSERT(find_canonical_monomial_of_vars(m.rvars(), k));
+    find_canonical_monomial_of_vars(m.rvars(), k);
+    return j == k;
+}
+
+
 void core::explain_existing_lower_bound(lpvar j) {
     SASSERT(has_lower_bound(j));
     current_expl().add(m_lar_solver.get_column_lower_bound_witness(j));
@@ -1410,7 +1418,7 @@ bool core::divide(const monomial& bc, const factor& c, factor & b) const {
         b = factor(b_rvars[0], factor_type::VAR);
     } else {
         monomial const* sv = m_emons.find_canonical(b_rvars);
-        if (!sv) {
+        if (sv == nullptr) {
             TRACE("nla_solver_div", tout << "not in rooted";);
             return false;
         }
@@ -1592,11 +1600,14 @@ bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf)
     }
     return false;
 }
-    
+
+// finds a canonical monomial with its binary factorization
 bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
     m = nullptr;
-    // todo: randomise loop
-    for (unsigned i: m_to_refine) {
+    unsigned r = random(), sz = m_to_refine.size();
+    for (unsigned k = 0; k < sz; k++) {
+        lpvar i = m_to_refine[(k + r) % sz];
+        if (!is_canonical_monomial(i)) continue;
         m = &m_emons[i];
         SASSERT (!check_monomial(*m));
         if (m->size() == 2) {

src/util/lp/nla_core.h

@@ -239,7 +239,8 @@ public:
 
     bool var_is_fixed(lpvar j) const;
         
-    bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const;
+    bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i) const;
+    bool is_canonical_monomial(lpvar) const;
 
     bool var_has_positive_lower_bound(lpvar j) const;
 

src/util/lp/nla_order_lemmas.cpp

@@ -28,12 +28,18 @@ namespace nla {
 // a > b && c > 0 => ac > bc
 void order::order_lemma() {
     TRACE("nla_solver", );
-    const auto& rm_ref = c().m_to_refine; // todo : run on the rooted subset or m_to_refine
-    unsigned start = random();
-    unsigned sz = rm_ref.size();
-    for (unsigned i = 0; i < sz && !done(); ++i) {        
-        const monomial& rm = c().m_emons[rm_ref[(i + start) % sz]];
-        order_lemma_on_rmonomial(rm);
+    if (!c().m_settings.run_order()) {
+        TRACE("nla_solver", tout << "not generating order lemmas\n";);
+        return;
+    }
+    
+    const auto& to_ref = c().m_to_refine;
+    unsigned r = random();
+    unsigned sz = to_ref.size();
+    for (unsigned i = 0; i < sz && !done(); ++i) {
+        lpvar j = to_ref[(i + r) % sz];
+        if (c().is_canonical_monomial(j))
+            order_lemma_on_canonical_monomial(c().emons()[j]);
     }
 }
 
@@ -41,7 +47,7 @@ void order::order_lemma() {
 // a > b && c > 0 => ac > bc
 // Consider here some binary factorizations of m=ac and
 // try create order lemmas with either factor playing the role of c.
-void order::order_lemma_on_rmonomial(const monomial& m) {
+void order::order_lemma_on_canonical_monomial(const monomial& m) {
     TRACE("nla_solver_details",
           tout << "m = " << pp_mon(c(), m););
 

src/util/lp/nla_order_lemmas.h

@@ -68,7 +68,7 @@ private:
     void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d);
     void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign);
     void order_lemma_on_binomial(const monomial& ac);
-    void order_lemma_on_rmonomial(const monomial& rm);
+    void order_lemma_on_canonical_monomial(const monomial& rm);
     // |c_sign| = 1, and c*c_sign > 0
     // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
     void generate_ol(const monomial& ac,                     

src/util/lp/nla_tangent_lemmas.cpp

@@ -29,54 +29,6 @@ tangents::tangents(core * c) : common(c) {}
 std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std::ostream& out) const {
     return out << "(" << a <<  ", " << b << ")";
 }
-unsigned tangents::find_binomial_to_refine() {
-    unsigned start = c().random();
-    unsigned sz = c().m_to_refine.size();
-    for (unsigned k = 0; k < sz; k++) {
-        lpvar j = c().m_to_refine[(k + start) % sz];
-        if (c().emons()[j].size() == 2)
-            return j;
-    }
-    return -1;
-}
-
-void tangents::generate_simple_tangent_lemma() {
-    lpvar j = find_binomial_to_refine();
-    if (!is_set(j)) return;
-    const monomial& m = c().emons()[j];
-    SASSERT(m.size() != 2);
-    TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
-    c().add_empty_lemma();
-    const 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;
-    }
-    bool gt = abs(mv) > abs(v);
-    if (gt) {
-        for (lpvar j : m.vars()) {
-            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(sign, m.var(), llc::LE, std::max(v, rational(-1)));
-    } else {
-        for (lpvar j : m.vars()) {
-            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(sign, m.var(), llc::LT);
-        c().mk_ineq(sign, m.var(), llc::GE, v);
-    }
-    TRACE("nla_solver", c().print_lemma(tout););
-}
-    
 void tangents::tangent_lemma() {
     if (!c().m_settings.run_tangents()) {
         TRACE("nla_solver", tout << "not generating tangent lemmas\n";);
@@ -231,4 +183,3 @@ void tangents::get_tang_points(point &a, point &b, bool below, const rational& v
     TRACE("nla_solver", tout << "pushed a = " << a << "\npushed b = " << b << std::endl;);
 }
 }
-

src/util/lp/nla_tangent_lemmas.h

@@ -54,8 +54,6 @@ public:
     void tangent_lemma();
 private:    
     lpvar find_binomial_to_refine();
-    void generate_simple_tangent_lemma();    
-
     void generate_explanations_of_tang_lemma(const monomial& m, const factorization& bf, lp::explanation& exp);
     
     void tangent_lemma_bf(const monomial& m,const factorization& bf);