Refactor basic lemmas out of nla_core

src/util/lp/CMakeLists.txt

@@ -7,6 +7,7 @@ z3_add_component(lp
     dense_matrix.cpp
     eta_matrix.cpp
     factorization.cpp
+    factorization_factory_imp.cpp
     gomory.cpp
     indexed_vector.cpp
     int_solver.cpp
@@ -23,6 +24,7 @@ z3_add_component(lp
     lp_utils.cpp
     matrix.cpp
     mon_eq.cpp
+    nla_basics_lemmas.cpp
     nla_core.cpp
     nla_solver.cpp
     nra_solver.cpp

src/util/lp/factorization_factory_imp.cpp

@@ -0,0 +1,34 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#include "util/lp/factorization_factory_imp.h"
+#include "util/lp/nla_core.h"
+namespace nla {
+        
+factorization_factory_imp::factorization_factory_imp(const rooted_mon& rm, const core& s) :
+        factorization_factory(rm.m_vars, &s.m_monomials[rm.orig_index()]),
+        m_core(s), m_mon(& s.m_monomials[rm.orig_index()]), m_rm(rm) { }
+        
+bool factorization_factory_imp::find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
+        return m_core.find_rm_monomial_of_vars(vars, i);
+}
+const monomial* factorization_factory_imp::find_monomial_of_vars(const svector<lpvar>& vars) const {
+    return m_core.find_monomial_of_vars(vars);
+}
+}

src/util/lp/factorization_factory_imp.h

@@ -0,0 +1,34 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#pragma once
+#include "util/lp/factorization.h"
+namespace nla {
+struct core;
+class rooted_mon;
+struct factorization_factory_imp: factorization_factory {
+    const core&  m_core;
+    const monomial *m_mon;
+    const rooted_mon& m_rm;
+        
+    factorization_factory_imp(const rooted_mon& rm, const core& s);
+    bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const;
+    const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
+};
+}

src/util/lp/nla_basics_lemmas.cpp

@@ -0,0 +1,855 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#include "util/lp/nla_basics_lemmas.h"
+#include "util/lp/nla_core.h"
+#include "util/lp/factorization_factory_imp.h"
+namespace nla {
+template <typename T> rational basics::vvr(T const& t) const { return m_core->vvr(t); }
+rational basics::vvr(lpvar t) const { return m_core->vvr(t); }
+template <typename T> lpvar basics::var(T const& t) const { return m_core->var(t); }
+
+basics::basics(core * c) : m_core(c) {}
+// Monomials m and n vars have the same values, up to "sign"
+// Generate a lemma if values of m.var() and n.var() are not the same up to sign
+bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
+    if (vvr(m) == vvr(n) *sign)
+        return false;
+    TRACE("nla_solver", tout << "sign contradiction:\nm = "; c().print_monomial_with_vars(m, tout); tout << "n= "; c().print_monomial_with_vars(n, tout); tout << "sign: " << sign << "\n";);
+    generate_sign_lemma(m, n, sign);
+    return true;
+}
+
+void basics::generate_zero_lemmas(const monomial& m) {
+    SASSERT(!vvr(m).is_zero() && c().product_value(m).is_zero());
+    int sign = nla::rat_sign(vvr(m));
+    unsigned_vector fixed_zeros;
+    lpvar zero_j = find_best_zero(m, fixed_zeros);
+    SASSERT(is_set(zero_j));
+    unsigned zero_power = 0;
+    for (unsigned j : m){
+        if (j == zero_j) {
+            zero_power++;
+            continue;
+        }
+        get_non_strict_sign(j, sign);
+        if(sign == 0)
+            break;
+    }
+    if (sign && is_even(zero_power))
+        sign = 0;
+    TRACE("nla_solver_details", tout << "zero_j = " << zero_j << ", sign = " << sign << "\n";);
+    if (sign == 0) { // have to generate a non-convex lemma
+        add_trival_zero_lemma(zero_j, m);
+    } else { 
+        generate_strict_case_zero_lemma(m, zero_j, sign);
+    }
+    for (lpvar j : fixed_zeros)
+        add_fixed_zero_lemma(m, j);
+}
+
+bool basics::try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
+    SASSERT(sign);
+    if (c().has_lower_bound(j) && c().get_lower_bound(j) >= rational(0))
+        return true;
+    if (c().has_upper_bound(j) && c().get_upper_bound(j) <= rational(0)) {
+        sign = -sign;
+        return true;
+    }
+    sign = 0;
+    return false;
+}
+
+void basics::get_non_strict_sign(lpvar j, int& sign) const {
+    const rational & v = vvr(j);
+    if (v.is_zero()) {
+        try_get_non_strict_sign_from_bounds(j, sign);
+    } else {
+        sign *= nla::rat_sign(v);
+    }
+}
+
+
+void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) {
+    if (product_sign == 0) {
+        TRACE("nla_solver_bl", tout << "zero product sign\n";);
+        generate_zero_lemmas(m);
+    } else {
+        add_empty_lemma();
+        for(lpvar j: m) {
+            negate_strict_sign(j);
+        }
+        c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT);
+        TRACE("nla_solver", c().print_lemma(tout); tout << "\n";);
+    }
+}
+    
+bool basics::basic_sign_lemma_model_based() {
+    unsigned i = random() % c().m_to_refine.size();
+    unsigned ii = i;
+    do {
+        const monomial& m = c().m_monomials[c().m_to_refine[i]];
+        int mon_sign = nla::rat_sign(vvr(m));
+        int product_sign = c().rat_sign(m);
+        if (mon_sign != product_sign) {
+            basic_sign_lemma_model_based_one_mon(m, product_sign);
+            if (c().done())
+                return true;
+        }
+        i++;
+        if (i == c().m_to_refine.size())
+            i = 0;
+    } while (i != ii);
+    return c().m_lemma_vec->size() > 0;
+}
+
+    
+bool basics::basic_sign_lemma_on_mon(unsigned i, std::unordered_set<unsigned> & explored){
+    const monomial& m = c().m_monomials[i];
+    TRACE("nla_solver_details", tout << "i = " << i << ", mon = "; c().print_monomial_with_vars(m, tout););
+    const index_with_sign&  rm_i_s = c().m_rm_table.get_rooted_mon(i);
+    unsigned k = rm_i_s.index();
+    if (!try_insert(k, explored))
+        return false;
+
+    const auto& mons_to_explore = c().m_rm_table.rms()[k].m_mons;
+    TRACE("nla_solver", tout << "rm = "; c().print_rooted_monomial_with_vars(c().m_rm_table.rms()[k], tout) << "\n";);
+        
+    for (index_with_sign i_s : mons_to_explore) {
+        TRACE("nla_solver", tout << "i_s = (" << i_s.index() << "," << i_s.sign() << ")\n";
+              c().print_monomial_with_vars(c().m_monomials[i_s.index()], tout << "m = ") << "\n";
+              {
+                  for (lpvar j : c().m_monomials[i_s.index()] ) {
+                      lpvar rj = c().m_evars.find(j).var();
+                      if (j == rj)
+                          tout << "rj = j ="  << j << "\n";
+                      else {
+                          lp::explanation e;
+                          c().m_evars.explain(j, e);
+                          tout << "j = " << j << ", e = "; c().print_explanation(e, tout) << "\n";
+                      }
+                  }
+              }
+              );
+        unsigned n = i_s.index();
+        if (n == i) continue;
+        if (basic_sign_lemma_on_two_monomials(m, c().m_monomials[n], rm_i_s.sign()*i_s.sign()))
+            if(done())
+                return true;
+    }
+    TRACE("nla_solver_details", tout << "return false\n";);
+    return false;
+}
+
+/**
+ * \brief <generate lemma by using the fact that -ab = (-a)b) and
+ -ab = a(-b)
+*/
+bool basics::basic_sign_lemma(bool derived) {
+    if (!derived)
+        return basic_sign_lemma_model_based();
+
+    std::unordered_set<unsigned> explored;
+    for (unsigned i : c().m_to_refine){
+        if (basic_sign_lemma_on_mon(i, explored))
+            return true;
+    }
+    return false;
+}
+// the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign
+// but it is not the case in the model
+void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) {
+    add_empty_lemma();
+    TRACE("nla_solver",
+          tout << "m = "; c().print_monomial_with_vars(m, tout);
+          tout << "n = "; c().print_monomial_with_vars(n, tout);
+          );
+    c().mk_ineq(m.var(), -sign, n.var(), llc::EQ);
+    explain(m);
+    explain(n);        
+    TRACE("nla_solver", c().print_lemma(tout););
+}
+// try to find a variable j such that vvr(j) = 0
+// and the bounds on j contain 0 as an inner point
+lpvar basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
+    lpvar zero_j = -1;
+    for (unsigned j : m){
+        if (vvr(j).is_zero()){
+            if (c().var_is_fixed_to_zero(j))
+                fixed_zeros.push_back(j);
+                
+            if (!is_set(zero_j) || c().zero_is_an_inner_point_of_bounds(j))
+                zero_j = j;
+        }
+    }
+    return zero_j;    
+}
+void basics::add_trival_zero_lemma(lpvar zero_j, const monomial& m) {
+    add_empty_lemma();
+    c().mk_ineq(zero_j, llc::NE);
+    c().mk_ineq(m.var(), llc::EQ);
+    TRACE("nla_solver", c().print_lemma(tout););            
+}
+void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j, int sign_of_zj) {
+    TRACE("nla_solver_bl", tout << "sign_of_zj = " << sign_of_zj << "\n";);
+    // we know all the signs
+    add_empty_lemma();
+    c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
+    for (unsigned j : m){
+        if (j != zero_j) {
+            negate_strict_sign(j);
+        }
+    }
+    negate_strict_sign(m.var());
+    TRACE("nla_solver", c().print_lemma(tout););
+}
+void basics::add_fixed_zero_lemma(const monomial& m, lpvar j) {
+    add_empty_lemma();
+    c().explain_fixed_var(j);
+    c().mk_ineq(m.var(), llc::EQ);
+    TRACE("nla_solver", c().print_lemma(tout););
+}
+void basics::add_empty_lemma() { c().add_empty_lemma(); }
+void basics::negate_strict_sign(lpvar j) {
+    TRACE("nla_solver_details", c().print_var(j, tout););
+    if (!vvr(j).is_zero()) {
+        int sign = nla::rat_sign(vvr(j));
+        c().mk_ineq(j, (sign == 1? llc::LE : llc::GE));
+    } else {   // vvr(j).is_zero()
+        if (c().has_lower_bound(j) && c().get_lower_bound(j) >= rational(0)) {
+            c().explain_existing_lower_bound(j);
+            c().mk_ineq(j, llc::GT);
+        } else {
+            SASSERT(c().has_upper_bound(j) && c().get_upper_bound(j) <= rational(0));
+            c().explain_existing_upper_bound(j);
+            c().mk_ineq(j, llc::LT);
+        }
+    }
+}
+
+// here we use the fact
+// xy = 0 -> x = 0 or y = 0
+bool basics::basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f) {
+    TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
+    add_empty_lemma();
+    c().explain_fixed_var(var(rm));
+    std::unordered_set<lpvar> processed;
+    for (auto j : f) {
+        if (try_insert(var(j), processed))
+            c().mk_ineq(var(j), llc::EQ);
+    }
+    explain(rm);
+    TRACE("nla_solver", c().print_lemma(tout););
+    return true;
+}
+// use basic multiplication properties to create a lemma
+bool basics::basic_lemma(bool derived) {
+    if (basic_sign_lemma(derived))
+        return true;
+    if (derived)
+        return false;
+    c().init_rm_to_refine();
+    const auto& rm_ref = c().m_rm_table.to_refine();
+    TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
+    unsigned start = random() % rm_ref.size();
+    unsigned i = start;
+    do {
+        const rooted_mon& r = c().m_rm_table.rms()[rm_ref[i]];
+        SASSERT (!c().check_monomial(c().m_monomials[r.orig_index()]));
+        basic_lemma_for_mon(r, derived);
+        if (++i == rm_ref.size()) {
+            i = 0;
+        }
+    } while(i != start && !done());
+        
+    return false;
+}
+// Use basic multiplication properties to create a lemma
+// for the given monomial.
+// "derived" means derived from constraints - the alternative is model based
+void basics::basic_lemma_for_mon(const rooted_mon& rm, bool derived) {
+    if (derived)
+        basic_lemma_for_mon_derived(rm);
+    else
+        basic_lemma_for_mon_model_based(rm);
+}
+bool basics::basic_lemma_for_mon_derived(const rooted_mon& rm) {
+    if (c().var_is_fixed_to_zero(var(rm))) {
+        for (auto factorization : factorization_factory_imp(rm, c())) {
+            if (factorization.is_empty())
+                continue;
+            if (basic_lemma_for_mon_zero(rm, factorization) ||
+                basic_lemma_for_mon_neutral_derived(rm, factorization)) {
+                explain(factorization);
+                return true;
+            }
+        }
+    } else {
+        for (auto factorization : factorization_factory_imp(rm, c())) {
+            if (factorization.is_empty())
+                continue;
+            if (basic_lemma_for_mon_non_zero_derived(rm, factorization) ||
+                basic_lemma_for_mon_neutral_derived(rm, factorization) ||
+                proportion_lemma_derived(rm, factorization)) {
+                explain(factorization);
+                return true;
+            }
+        }
+    }
+    return false;
+}
+// x = 0 or y = 0 -> xy = 0
+bool basics::basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f) {
+    TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
+    if (! c().var_is_separated_from_zero(var(rm)))
+        return false; 
+    int zero_j = -1;
+    for (auto j : f) {
+        if ( c().var_is_fixed_to_zero(var(j))) {
+            zero_j = var(j);
+            break;
+        }
+    }
+
+    if (zero_j == -1) {
+        return false;
+    } 
+    add_empty_lemma();
+    c().explain_fixed_var(zero_j);
+    c().explain_var_separated_from_zero(var(rm));
+    explain(rm);
+    TRACE("nla_solver",  c().print_lemma(tout););
+    return true;
+}
+// use the fact that
+// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted_mon& rm, const factorization& f) {
+    TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
+
+    lpvar mon_var =  c().m_monomials[rm.orig_index()].var();
+    TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
+        
+    const auto & mv = vvr(mon_var);
+    const auto  abs_mv = abs(mv);
+        
+    if (abs_mv == rational::zero()) {
+        return false;
+    }
+    bool mon_var_is_sep_from_zero =  c().var_is_separated_from_zero(mon_var);
+    lpvar jl = -1;
+    for (auto fc : f ) {
+        lpvar j = var(fc);
+        if (abs(vvr(j)) == abs_mv &&  c().vars_are_equiv(j, mon_var) &&
+            (mon_var_is_sep_from_zero ||  c().var_is_separated_from_zero(j))) {
+            jl = j;
+            break;
+        }
+    }
+    if (jl == static_cast<lpvar>(-1))
+        return false;
+        
+    lpvar not_one_j = -1;
+    for (auto j : f ) {
+        if (var(j) == jl) {
+            continue;
+        }
+        if (abs(vvr(j)) != rational(1)) {
+            not_one_j = var(j);
+            break;
+        }
+    }
+
+    if (not_one_j == static_cast<lpvar>(-1)) {
+        return false;
+    } 
+
+    add_empty_lemma();
+    // mon_var = 0
+    if (mon_var_is_sep_from_zero)
+         c().explain_var_separated_from_zero(mon_var);
+    else
+         c().explain_var_separated_from_zero(jl);
+
+     c().explain_equiv_vars(mon_var, jl);
+        
+    // not_one_j = 1
+    c().mk_ineq(not_one_j, llc::EQ,  rational(1));   
+        
+    // not_one_j = -1
+    c().mk_ineq(not_one_j, llc::EQ, -rational(1));
+    explain(rm);
+    TRACE("nla_solver",  c().print_lemma(tout); );
+    return true;
+}
+// use the fact
+// 1 * 1 ... * 1 * x * 1 ... * 1 = x
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const rooted_mon& rm, const factorization& f) {
+    return false;
+    rational sign = rm.orig().m_sign;
+    lpvar not_one = -1;
+
+    TRACE("nla_solver", tout << "f = ";  c().print_factorization(f, tout););
+    for (auto j : f){
+        TRACE("nla_solver", tout << "j = ";  c().print_factor_with_vars(j, tout););
+        auto v = vvr(j);
+        if (v == rational(1)) {
+            continue;
+        }
+
+        if (v == -rational(1)) { 
+            sign = - sign;
+            continue;
+        } 
+
+        if (not_one == static_cast<lpvar>(-1)) {
+            not_one = var(j);
+            continue;
+        }
+
+        // if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma
+        return false;
+    }
+
+    add_empty_lemma();
+    explain(rm);
+
+    for (auto j : f){
+        lpvar var_j = var(j);
+        if (not_one == var_j) continue;
+        c().mk_ineq(var_j, llc::NE, j.is_var()? vvr(j) :  c().canonize_sign(j) * vvr(j));   
+    }
+
+    if (not_one == static_cast<lpvar>(-1)) {
+        c().mk_ineq( c().m_monomials[rm.orig_index()].var(), llc::EQ, sign);
+    } else {
+        c().mk_ineq( c().m_monomials[rm.orig_index()].var(), -sign, not_one, llc::EQ);
+    }
+    TRACE("nla_solver",
+          tout << "rm = ";  c().print_rooted_monomial_with_vars(rm, tout);
+           c().print_lemma(tout););
+    return true;
+}
+
+bool basics::basic_lemma_for_mon_neutral_derived(const rooted_mon& rm, const factorization& factorization) {
+    return
+        basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization) || 
+        basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(rm, factorization);
+    return false;
+}
+
+// x != 0 or y = 0 => |xy| >= |y|
+void basics::proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization) {
+    rational rmv = abs(vvr(rm));
+    if (rmv.is_zero()) {
+        SASSERT(c().has_zero_factor(factorization));
+        return;
+    }
+    int factor_index = 0;
+    for (factor f : factorization) {
+        if (abs(vvr(f)) > rmv) {
+            generate_pl(rm, factorization, factor_index);
+            return;
+        }
+        factor_index++;
+    }
+}
+// x != 0 or y = 0 => |xy| >= |y|
+bool basics::proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization) {
+    return false;
+    rational rmv = abs(vvr(rm));
+    if (rmv.is_zero()) {
+        SASSERT(c().has_zero_factor(factorization));
+        return false;
+    }
+    int factor_index = 0;
+    for (factor f : factorization) {
+        if (abs(vvr(f)) > rmv) {
+            generate_pl(rm, factorization, factor_index);
+            return true;
+        }
+        factor_index++;
+    }
+    return false;
+}
+// if there are no zero factors then |m| >= |m[factor_index]|
+void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
+    add_empty_lemma();
+    unsigned mon_var = m.var();
+    rational mv = vvr(mon_var);
+    rational sm = rational(nla::rat_sign(mv));
+    c().mk_ineq(sm, mon_var, llc::LT);
+    for (unsigned fi = 0; fi < m.size(); fi ++) {
+        lpvar j = m[fi];
+        if (fi != factor_index) {
+            c().mk_ineq(j, llc::EQ);
+        } else {
+            rational jv = vvr(j);
+            rational sj = rational(nla::rat_sign(jv));
+            SASSERT(sm*mv < sj*jv);
+            c().mk_ineq(sj, j, llc::LT);
+            c().mk_ineq(sm, mon_var, -sj, j, llc::GE );
+        }
+    }
+    TRACE("nla_solver", c().print_lemma(tout); );
+}
+    
+// none of the factors is zero and the product is not zero
+// -> |fc[factor_index]| <= |rm|
+void basics::generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index) {
+    TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = ";
+          c().print_rooted_monomial_with_vars(rm, tout);
+          tout << "fc = "; c().print_factorization(fc, tout);
+          tout << "orig mon = "; c().print_monomial(c().m_monomials[rm.orig_index()], tout););
+    if (fc.is_mon()) {
+        generate_pl_on_mon(*fc.mon(), factor_index);
+        return;
+    }
+    add_empty_lemma();
+    int fi = 0;
+    rational rmv = vvr(rm);
+    rational sm = rational(nla::rat_sign(rmv));
+    unsigned mon_var = var(rm);
+    c().mk_ineq(sm, mon_var, llc::LT);
+    for (factor f : fc) {
+        if (fi++ != factor_index) {
+            c().mk_ineq(var(f), llc::EQ);
+        } else {
+            lpvar j = var(f);
+            rational jv = vvr(j);
+            rational sj = rational(nla::rat_sign(jv));
+            SASSERT(sm*rmv < sj*jv);
+            c().mk_ineq(sj, j, llc::LT);
+            c().mk_ineq(sm, mon_var, -sj, j, llc::GE );
+        }
+    }
+    if (!fc.is_mon()) {
+        explain(fc);
+        explain(rm);
+    }
+    TRACE("nla_solver", c().print_lemma(tout); );
+}   
+// here we use the fact xy = 0 -> x = 0 or y = 0
+void basics::basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f) {        
+    TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
+    SASSERT(vvr(rm).is_zero()&& ! c().rm_check(rm));
+    add_empty_lemma();
+    int sign =  c().get_derived_sign(rm, f);
+    if (sign == 0) {
+        c().mk_ineq(var(rm), llc::NE);        
+        for (auto j : f) {
+            c().mk_ineq(var(j), llc::EQ);
+        }
+    } else {
+        c().mk_ineq(var(rm), llc::NE);        
+        for (auto j : f) {
+            c().explain_separation_from_zero(var(j));
+        }            
+    }
+    explain(rm);
+    explain(f);
+    TRACE("nla_solver", c().print_lemma(tout););
+}
+
+void basics::basic_lemma_for_mon_model_based(const rooted_mon& rm) {
+    TRACE("nla_solver_bl", tout << "rm = "; c().print_rooted_monomial(rm, tout););
+    if (vvr(rm).is_zero()) {
+        for (auto factorization : factorization_factory_imp(rm, c())) {
+            if (factorization.is_empty())
+                continue;
+            basic_lemma_for_mon_zero_model_based(rm, factorization);
+            basic_lemma_for_mon_neutral_model_based(rm, factorization); // todo - the same call is made in the else branch
+        }
+    } else {
+        for (auto factorization : factorization_factory_imp(rm, c())) {
+            if (factorization.is_empty())
+                continue;
+            basic_lemma_for_mon_non_zero_model_based(rm, factorization);
+            basic_lemma_for_mon_neutral_model_based(rm, factorization);
+            proportion_lemma_model_based(rm, factorization) ;
+        }
+    }
+}
+
+// use the fact that
+// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m) {
+    TRACE("nla_solver_bl", c().print_monomial(m, tout););
+
+    lpvar mon_var = m.var();
+    const auto & mv = vvr(mon_var);
+    const auto  abs_mv = abs(mv);
+    if (abs_mv == rational::zero()) {
+        return false;
+    }
+    lpvar jl = -1;
+    for (auto j : m ) {
+        if (abs(vvr(j)) == abs_mv) {
+            jl = j;
+            break;
+        }
+    }
+    if (jl == static_cast<lpvar>(-1))
+        return false;
+    lpvar not_one_j = -1;
+    for (auto j : m ) {
+        if (j == jl) {
+            continue;
+        }
+        if (abs(vvr(j)) != rational(1)) {
+            not_one_j = j;
+            break;
+        }
+    }
+
+    if (not_one_j == static_cast<lpvar>(-1)) {
+        return false;
+    } 
+
+    add_empty_lemma();
+    // mon_var = 0
+    c().mk_ineq(mon_var, llc::EQ);
+        
+    // negate abs(jl) == abs()
+    if (vvr(jl) == - vvr(mon_var))
+        c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma());   
+    else  // jl == mon_var
+        c().mk_ineq(jl, -rational(1), mon_var, llc::NE);   
+
+    // not_one_j = 1
+    c().mk_ineq(not_one_j, llc::EQ,  rational(1));   
+        
+    // not_one_j = -1
+    c().mk_ineq(not_one_j, llc::EQ, -rational(1));
+    TRACE("nla_solver", c().print_lemma(tout); );
+    return true;
+}
+// use the fact
+// 1 * 1 ... * 1 * x * 1 ... * 1 = x
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m) {
+    lpvar not_one = -1;
+    rational sign(1);
+    TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout););
+    for (auto j : m){
+        auto v = vvr(j);
+        if (v == rational(1)) {
+            continue;
+        }
+        if (v == -rational(1)) { 
+            sign = - sign;
+            continue;
+        } 
+        if (not_one == static_cast<lpvar>(-1)) {
+            not_one = j;
+            continue;
+        }
+        // if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma
+        return false;
+    }
+
+    if (not_one + 1) {  // we found the only not_one
+        if (vvr(m) == vvr(not_one) * sign) {
+            TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
+            return false;
+        }
+    }
+        
+    add_empty_lemma();
+    for (auto j : m){
+        if (not_one == j) continue;
+        c().mk_ineq(j, llc::NE, vvr(j));   
+    }
+
+    if (not_one == static_cast<lpvar>(-1)) {
+        c().mk_ineq(m.var(), llc::EQ, sign);
+    } else {
+        c().mk_ineq(m.var(), -sign, not_one, llc::EQ);
+    }
+    TRACE("nla_solver",  c().print_lemma(tout););
+    return true;
+}
+
+// use the fact that
+// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const rooted_mon& rm, const factorization& f) {
+    TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
+
+    lpvar mon_var = c().m_monomials[rm.orig_index()].var();
+    TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
+        
+    const auto & mv = vvr(mon_var);
+    const auto  abs_mv = abs(mv);
+        
+    if (abs_mv == rational::zero()) {
+        return false;
+    }
+    lpvar jl = -1;
+    for (auto j : f ) {
+        if (abs(vvr(j)) == abs_mv) {
+            jl = var(j);
+            break;
+        }
+    }
+    if (jl == static_cast<lpvar>(-1))
+        return false;
+    lpvar not_one_j = -1;
+    for (auto j : f ) {
+        if (var(j) == jl) {
+            continue;
+        }
+        if (abs(vvr(j)) != rational(1)) {
+            not_one_j = var(j);
+            break;
+        }
+    }
+
+    if (not_one_j == static_cast<lpvar>(-1)) {
+        return false;
+    } 
+
+    add_empty_lemma();
+    // mon_var = 0
+    c().mk_ineq(mon_var, llc::EQ);
+        
+    // negate abs(jl) == abs()
+    if (vvr(jl) == - vvr(mon_var))
+        c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma());   
+    else  // jl == mon_var
+        c().mk_ineq(jl, -rational(1), mon_var, llc::NE);   
+
+    // not_one_j = 1
+    c().mk_ineq(not_one_j, llc::EQ,  rational(1));   
+        
+    // not_one_j = -1
+    c().mk_ineq(not_one_j, llc::EQ, -rational(1));
+    explain(rm);
+    explain(f);
+
+    TRACE("nla_solver", c().print_lemma(tout); );
+    return true;
+}
+
+void basics::basic_lemma_for_mon_neutral_model_based(const rooted_mon& rm, const factorization& f) {
+    if (f.is_mon()) {
+        basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(*f.mon());
+        basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(*f.mon());
+    }
+    else {
+        basic_lemma_for_mon_neutral_monomial_to_factor_model_based(rm, f);
+        basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(rm, f);
+    }
+}
+// use the fact
+// 1 * 1 ... * 1 * x * 1 ... * 1 = x
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const rooted_mon& rm, const factorization& f) {
+    rational sign = rm.orig_sign();
+    TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
+    lpvar not_one = -1;
+    for (auto j : f){
+        TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout););
+        auto v = vvr(j);
+        if (v == rational(1)) {
+            continue;
+        }
+            
+        if (v == -rational(1)) { 
+            sign = - sign;
+            continue;
+        } 
+            
+        if (not_one == static_cast<lpvar>(-1)) {
+            not_one = var(j);
+            continue;
+        }
+            
+        // if we are here then there are at least two factors with absolute values different from one : cannot create the lemma
+        return false;
+    }
+
+    if (not_one + 1) {
+        // we found the only not_one
+        if (vvr(rm) == vvr(not_one) * sign) {
+            TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
+            return false;
+        }
+    } else {
+        // we have +-ones only in the factorization
+        if (vvr(rm) == sign) {
+            return false;
+        }
+    }
+
+    TRACE("nla_solver_bl", tout << "not_one = " << not_one << "\n";);
+        
+    add_empty_lemma();
+
+    for (auto j : f){
+        lpvar var_j = var(j);
+        if (not_one == var_j) continue;
+        c().mk_ineq(var_j, llc::NE, j.is_var()? vvr(j) : c().canonize_sign(j) * vvr(j));   
+    }
+
+    if (not_one == static_cast<lpvar>(-1)) {
+        c().mk_ineq(c().m_monomials[rm.orig_index()].var(), llc::EQ, sign);
+    } else {
+        c().mk_ineq(c().m_monomials[rm.orig_index()].var(), -sign, not_one, llc::EQ);
+    }
+    explain(rm);
+    explain(f);
+    TRACE("nla_solver",
+          c().print_lemma(tout);
+          tout << "rm = "; c().print_rooted_monomial_with_vars(rm, tout);
+          );
+    return true;
+}
+
+
+void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) {
+    TRACE("nla_solver_bl", c().print_factorization(f, tout););
+    int zero_j = -1;
+    for (auto j : f) {
+        if (vvr(j).is_zero()) {
+            zero_j = var(j);
+            break;
+        }
+    }
+
+    if (zero_j == -1) { return; } 
+    add_empty_lemma();
+    c().mk_ineq(zero_j, llc::NE);
+    c().mk_ineq(f.mon()->var(), llc::EQ);
+    TRACE("nla_solver", c().print_lemma(tout););
+}
+
+// x = 0 or y = 0 -> xy = 0
+void basics::basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f) {
+    TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
+    if (f.is_mon())
+        basic_lemma_for_mon_non_zero_model_based_mf(f);
+    else
+        basic_lemma_for_mon_non_zero_model_based_mf(f);
+}
+
+bool basics::done() const { return c().done(); }
+
+template <typename T> void basics::explain(const T& t) {
+    c().explain(t, c().current_expl());
+}
+template void basics::explain<monomial>(const monomial& t);
+
+}

src/util/lp/nla_basics_lemmas.h

@@ -0,0 +1,115 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#pragma once
+#include "util/lp/monomial.h"    
+#include "util/lp/rooted_mons.h"    
+#include "util/lp/factorization.h"    
+
+
+namespace nla {
+struct core;
+struct basics {
+    core* m_core;
+    core& c() { return *m_core; }
+    const core& c() const { return *m_core; }
+    basics(core *core);
+    bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign);
+
+    void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign);
+    
+    bool basic_sign_lemma_model_based();
+    bool basic_sign_lemma_on_mon(unsigned i, std::unordered_set<unsigned> & explore);
+
+    /**
+     * \brief <generate lemma by using the fact that -ab = (-a)b) and
+     -ab = a(-b)
+    */
+    bool basic_sign_lemma(bool derived);
+    bool basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f);
+
+    void basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f);
+
+    void basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f);
+    // x = 0 or y = 0 -> xy = 0
+    void basic_lemma_for_mon_non_zero_model_based_rm(const rooted_mon& rm, const factorization& f);
+
+    void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f);
+    // x = 0 or y = 0 -> xy = 0
+    bool basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f);
+
+    // use the fact that
+    // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const rooted_mon& rm, const factorization& f);
+    // use the fact that
+    // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted_mon& rm, const factorization& f);
+
+    // use the fact
+    // 1 * 1 ... * 1 * x * 1 ... * 1 = x
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const rooted_mon& rm, const factorization& f);
+    // use the fact
+    // 1 * 1 ... * 1 * x * 1 ... * 1 = x
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m);
+    // use the fact
+    // 1 * 1 ... * 1 * x * 1 ... * 1 = x
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const rooted_mon& rm, const factorization& f);
+    void basic_lemma_for_mon_neutral_model_based(const rooted_mon& rm, const factorization& f);
+    
+    bool basic_lemma_for_mon_neutral_derived(const rooted_mon& rm, const factorization& factorization);
+
+    void basic_lemma_for_mon_model_based(const rooted_mon& rm);
+
+    bool basic_lemma_for_mon_derived(const rooted_mon& rm);
+    
+    // Use basic multiplication properties to create a lemma
+    // for the given monomial.
+    // "derived" means derived from constraints - the alternative is model based
+    void basic_lemma_for_mon(const rooted_mon& rm, bool derived);
+    // use basic multiplication properties to create a lemma
+    bool basic_lemma(bool derived);
+    template <typename T> rational vvr(T const& t) const;
+    rational vvr(lpvar) const;
+    template <typename T> lpvar var(T const& t) const;
+    void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign);
+    void generate_zero_lemmas(const monomial& m);
+    lpvar find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const;
+    bool try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const;
+    void get_non_strict_sign(lpvar j, int& sign) const;
+    void add_trival_zero_lemma(lpvar zero_j, const monomial& m);
+    void generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j, int sign_of_zj);
+    
+    void add_fixed_zero_lemma(const monomial& m, lpvar j);
+    void add_empty_lemma();
+    void negate_strict_sign(lpvar j);
+    bool done() const;
+    // x != 0 or y = 0 => |xy| >= |y|
+    void proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization);
+    // x != 0 or y = 0 => |xy| >= |y|
+    bool proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization);
+    template <typename T> void explain(const T&);
+    // if there are no zero factors then |m| >= |m[factor_index]|
+    void generate_pl_on_mon(const monomial& m, unsigned factor_index);
+    
+    // none of the factors is zero and the product is not zero
+    // -> |fc[factor_index]| <= |rm|
+    void generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index);   
+};
+}

src/util/lp/nla_core.cpp

@@ -18,16 +18,9 @@ Revision History:
 
 --*/
 #include "util/lp/nla_core.h"
+#include "util/lp/factorization_factory_imp.h"
 namespace nla {
 
-template <typename A, typename B>
-bool try_insert(const A& elem, B& collection) {
-    auto it = collection.find(elem);
-    if (it != collection.end())
-        return false;
-    collection.insert(elem);
-    return true;
-}
 
 point operator+(const point& a, const point& b) {
     return point(a.x + b.x, a.y + b.y);
@@ -47,13 +40,11 @@ unsigned core::find_monomial(const unsigned_vector& k) const {
     return it->second;
 }
     
-core::core(lp::lar_solver& s, reslimit& lim, params_ref const& p)
+core::core(lp::lar_solver& s) :
-    :
     m_evars(),
-    m_lar_solver(s)
+    m_lar_solver(s),
-    // m_limit(lim),
+    m_tangents(this),
-    // m_params(p)
+    m_basics(this) {
-{
 }
     
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
@@ -588,19 +579,6 @@ monomial_coeff core::canonize_monomial(monomial const& m) const {
     return monomial_coeff(vars, sign);
 }
 
-// the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign
-// but it is not the case in the model
-void core::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) {
-    add_empty_lemma();
-    TRACE("nla_solver",
-          tout << "m = "; print_monomial_with_vars(m, tout);
-          tout << "n = "; print_monomial_with_vars(n, tout);
-          );
-    mk_ineq(m.var(), -sign, n.var(), llc::EQ);
-    explain(m, current_expl());
-    explain(n, current_expl());        
-    TRACE("nla_solver", print_lemma(tout););
-}
 lemma& core::current_lemma() { return m_lemma_vec->back(); }
 const lemma& core::current_lemma() const { return m_lemma_vec->back(); }
 vector<ineq>& core::current_ineqs() { return current_lemma().ineqs(); }
@@ -673,21 +651,6 @@ bool core::zero_is_an_inner_point_of_bounds(lpvar j) const {
     return true;
 }
     
-// try to find a variable j such that vvr(j) = 0
-// and the bounds on j contain 0 as an inner point
-lpvar core::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
-    lpvar zero_j = -1;
-    for (unsigned j : m){
-        if (vvr(j).is_zero()){
-            if (var_is_fixed_to_zero(j))
-                fixed_zeros.push_back(j);
-                
-            if (!is_set(zero_j) || zero_is_an_inner_point_of_bounds(j))
-                zero_j = j;
-        }
-    }
-    return zero_j;    
-}
 
 bool core:: try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
     SASSERT(sign);
@@ -752,6 +715,7 @@ void core:: add_fixed_zero_lemma(const monomial& m, lpvar j) {
     mk_ineq(m.var(), llc::EQ);
     TRACE("nla_solver", print_lemma(tout););
 }
+
 llc core::negate(llc cmp) {
     switch(cmp) {
     case llc::LE: return llc::GT;
@@ -796,6 +760,7 @@ bool core:: sign_contradiction(const monomial& m) const {
   return m_evars.eq_vars(j);
   }
 */
+
 // Monomials m and n vars have the same values, up to "sign"
 // Generate a lemma if values of m.var() and n.var() are not the same up to sign
 bool core:: basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
@@ -994,38 +959,6 @@ const monomial* core::find_monomial_of_vars(const svector<lpvar>& vars) const {
     return &m_monomials[m_rm_table.rms()[i].orig_index()];
 }
 
-struct factorization_factory_imp: factorization_factory {
-    const core&  m_core;
-    const monomial *m_mon;
-    const rooted_mon& m_rm;
-        
-    factorization_factory_imp(const rooted_mon& rm, const core& s) :
-        factorization_factory(rm.m_vars, &s.m_monomials[rm.orig_index()]),
-        m_core(s), m_mon(& s.m_monomials[rm.orig_index()]), m_rm(rm) { }
-        
-    bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
-        return m_core.find_rm_monomial_of_vars(vars, i);
-    }
-    const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const {
-        return m_core.find_monomial_of_vars(vars);
-    }
-
-};
-// here we use the fact
-// xy = 0 -> x = 0 or y = 0
-bool core::basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f) {
-    TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
-    add_empty_lemma();
-    explain_fixed_var(var(rm));
-    std::unordered_set<lpvar> processed;
-    for (auto j : f) {
-        if (try_insert(var(j), processed))
-            mk_ineq(var(j), llc::EQ);
-    }
-    explain(rm, current_expl());
-    TRACE("nla_solver", print_lemma(tout););
-    return true;
-}
 
 void core::explain_existing_lower_bound(lpvar j) {
     SASSERT(has_lower_bound(j));
@@ -1057,28 +990,6 @@ int core::get_derived_sign(const rooted_mon& rm, const factorization& f) const {
     }
     return nla::rat_sign(sign);
 }
-// here we use the fact xy = 0 -> x = 0 or y = 0
-void core::basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f) {        
-    TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
-    SASSERT(vvr(rm).is_zero()&& !rm_check(rm));
-    add_empty_lemma();
-    int sign = get_derived_sign(rm, f);
-    if (sign == 0) {
-        mk_ineq(var(rm), llc::NE);        
-        for (auto j : f) {
-            mk_ineq(var(j), llc::EQ);
-        }
-    } else {
-        mk_ineq(var(rm), llc::NE);        
-        for (auto j : f) {
-            explain_separation_from_zero(var(j));
-        }            
-    }
-    explain(rm, current_expl());
-    explain(f, current_expl());
-    TRACE("nla_solver", print_lemma(tout););
-}
-
 void core::trace_print_monomial_and_factorization(const rooted_mon& rm, const factorization& f, std::ostream& out) const {
     out << "rooted vars: ";
     print_product(rm.m_vars, out);
@@ -1102,51 +1013,6 @@ void core::explain_fixed_var(lpvar j) {
     current_expl().add(m_lar_solver.get_column_upper_bound_witness(j));
     current_expl().add(m_lar_solver.get_column_lower_bound_witness(j));
 }
-// x = 0 or y = 0 -> xy = 0
-void core::basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f) {
-    TRACE("nla_solver_bl", trace_print_monomial_and_factorization(rm, f, tout););
-    if (f.is_mon())
-        basic_lemma_for_mon_non_zero_model_based_mf(f);
-    else
-        basic_lemma_for_mon_non_zero_model_based_mf(f);
-}
-// x = 0 or y = 0 -> xy = 0
-void core::basic_lemma_for_mon_non_zero_model_based_rm(const rooted_mon& rm, const factorization& f) {
-    TRACE("nla_solver_bl", trace_print_monomial_and_factorization(rm, f, tout););
-    SASSERT (!vvr(rm).is_zero());
-    int zero_j = -1;
-    for (auto j : f) {
-        if (vvr(j).is_zero()) {
-            zero_j = var(j);
-            break;
-        }
-    }
-
-    if (zero_j == -1) { return; } 
-    add_empty_lemma();
-    mk_ineq(zero_j, llc::NE);
-    mk_ineq(var(rm), llc::EQ);
-    explain(rm, current_expl());
-    explain(f, current_expl());
-    TRACE("nla_solver", print_lemma(tout););
-}
-
-void core::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) {
-    TRACE("nla_solver_bl", print_factorization(f, tout););
-    int zero_j = -1;
-    for (auto j : f) {
-        if (vvr(j).is_zero()) {
-            zero_j = var(j);
-            break;
-        }
-    }
-
-    if (zero_j == -1) { return; } 
-    add_empty_lemma();
-    mk_ineq(zero_j, llc::NE);
-    mk_ineq(f.mon()->var(), llc::EQ);
-    TRACE("nla_solver", print_lemma(tout););
-}
 
 bool core:: var_has_positive_lower_bound(lpvar j) const {
     return m_lar_solver.column_has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type<lp::impq>();
@@ -1315,6 +1181,7 @@ void core::explain_equiv_vars(lpvar a, lpvar b) {
         explain_fixed_var(b);
     }
 }
+
 // use the fact that
 // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
 bool core:: basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted_mon& rm, const factorization& f) {
@@ -1564,64 +1431,6 @@ bool core:: has_zero_factor(const factorization& factorization) const {
     return false;
 }
 
-// if there are no zero factors then |m| >= |m[factor_index]|
-void core::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
-    add_empty_lemma();
-    unsigned mon_var = m.var();
-    rational mv = vvr(mon_var);
-    rational sm = rational(nla::rat_sign(mv));
-    mk_ineq(sm, mon_var, llc::LT);
-    for (unsigned fi = 0; fi < m.size(); fi ++) {
-        lpvar j = m[fi];
-        if (fi != factor_index) {
-            mk_ineq(j, llc::EQ);
-        } else {
-            rational jv = vvr(j);
-            rational sj = rational(nla::rat_sign(jv));
-            SASSERT(sm*mv < sj*jv);
-            mk_ineq(sj, j, llc::LT);
-            mk_ineq(sm, mon_var, -sj, j, llc::GE );
-        }
-    }
-    TRACE("nla_solver", print_lemma(tout); );
-}
-    
-// none of the factors is zero and the product is not zero
-// -> |fc[factor_index]| <= |rm|
-void core::generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index) {
-    TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = ";
-          print_rooted_monomial_with_vars(rm, tout);
-          tout << "fc = "; print_factorization(fc, tout);
-          tout << "orig mon = "; print_monomial(m_monomials[rm.orig_index()], tout););
-    if (fc.is_mon()) {
-        generate_pl_on_mon(*fc.mon(), factor_index);
-        return;
-    }
-    add_empty_lemma();
-    int fi = 0;
-    rational rmv = vvr(rm);
-    rational sm = rational(nla::rat_sign(rmv));
-    unsigned mon_var = var(rm);
-    mk_ineq(sm, mon_var, llc::LT);
-    for (factor f : fc) {
-        if (fi++ != factor_index) {
-            mk_ineq(var(f), llc::EQ);
-        } else {
-            lpvar j = var(f);
-            rational jv = vvr(j);
-            rational sj = rational(nla::rat_sign(jv));
-            SASSERT(sm*rmv < sj*jv);
-            mk_ineq(sj, j, llc::LT);
-            mk_ineq(sm, mon_var, -sj, j, llc::GE );
-        }
-    }
-    if (!fc.is_mon()) {
-        explain(fc, current_expl());
-        explain(rm, current_expl());
-    }
-    TRACE("nla_solver", print_lemma(tout); );
-}   
-
 template <typename T>
 bool core:: has_zero(const T& product) const {
     for (const rational & t : product) {
@@ -3167,7 +2976,7 @@ lbool core:: inner_check(bool derived) {
     for (int search_level = 0; search_level < 3 && !done(); search_level++) {
         TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";);
         if (search_level == 0) {
-            basic_lemma(derived);
+            m_basics.basic_lemma(derived);
             if (!m_lemma_vec->empty())
                 return l_false;
         }
@@ -3241,5 +3050,6 @@ lbool core:: test_check(
     m_lar_solver.set_status(lp::lp_status::OPTIMAL);
     return check(l);
 }
+template rational core::product_value<monomial>(const monomial & m) const;
 
 } // end of nla

src/util/lp/nla_core.h

@@ -22,8 +22,19 @@
 #include "util/lp/lp_types.h"
 #include "util/lp/var_eqs.h"
 #include "util/lp/rooted_mons.h"
-
+#include "util/lp/nla_tangent_lemmas.h"
+#include "util/lp/nla_basics_lemmas.h"
 namespace nla {
+
+template <typename A, typename B>
+bool try_insert(const A& elem, B& collection) {
+    auto it = collection.find(elem);
+    if (it != collection.end())
+        return false;
+    collection.insert(elem);
+    return true;
+}
+
 typedef lp::constraint_index lpci;
 typedef lp::lconstraint_kind llc;
 
@@ -91,7 +102,9 @@ struct core {
     vector<lemma> *                                                  m_lemma_vec;
     unsigned_vector                                                  m_to_refine;
     std::unordered_map<unsigned_vector, unsigned, hash_svector>      m_mkeys; // the key is the sorted vars of a monomial 
-    
+    tangents                                                         m_tangents;
+    basics                                                            m_basics;
+    // methods
     unsigned find_monomial(const unsigned_vector& k) const;
     core(lp::lar_solver& s, reslimit& lim, params_ref const& p);
     
@@ -246,9 +259,6 @@ struct core {
     // 
     monomial_coeff canonize_monomial(monomial const& m) const;
 
-    // the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign
-    // but it is not the case in the model
-    void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign);
     lemma& current_lemma();
     const lemma& current_lemma() const;
     vector<ineq>& current_ineqs();
@@ -257,10 +267,6 @@ struct core {
 
     int vars_sign(const svector<lpvar>& v);
 
-    void negate_strict_sign(lpvar j);
-    
-    void generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j, int sign_of_zj);
-
     bool has_upper_bound(lpvar j) const; 
 
     bool has_lower_bound(lpvar j) const; 
@@ -271,20 +277,6 @@ struct core {
     
     bool zero_is_an_inner_point_of_bounds(lpvar j) const;
     
-    // try to find a variable j such that vvr(j) = 0
-    // and the bounds on j contain 0 as an inner point
-    lpvar find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const;
-
-    bool try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const;
-
-    void get_non_strict_sign(lpvar j, int& sign) const;
-
-    void add_trival_zero_lemma(lpvar zero_j, const monomial& m);
-    
-    void generate_zero_lemmas(const monomial& m);
-
-    void add_fixed_zero_lemma(const monomial& m, lpvar j);
-    
     int rat_sign(const monomial& m) const;
     inline int rat_sign(lpvar j) const { return nla::rat_sign(vvr(j)); }
 
@@ -296,18 +288,6 @@ struct core {
     */
     // Monomials m and n vars have the same values, up to "sign"
     // Generate a lemma if values of m.var() and n.var() are not the same up to sign
-    bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign);
-
-    void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign);
-    
-    bool basic_sign_lemma_model_based();
-    bool basic_sign_lemma_on_mon(unsigned i, std::unordered_set<unsigned> & explore);
-
-    /**
-     * \brief <generate lemma by using the fact that -ab = (-a)b) and
-     -ab = a(-b)
-    */
-    bool basic_sign_lemma(bool derived);
 
     bool var_is_fixed_to_zero(lpvar j) const;
     bool var_is_fixed_to_val(lpvar j, const rational& v) const;
@@ -328,8 +308,6 @@ struct core {
 
     const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
 
-    bool basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f);
-
     void explain_existing_lower_bound(lpvar j);
 
     void explain_existing_upper_bound(lpvar j);
@@ -338,19 +316,12 @@ struct core {
 
     int get_derived_sign(const rooted_mon& rm, const factorization& f) const;
     // here we use the fact xy = 0 -> x = 0 or y = 0
-    void basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f);
-
     void trace_print_monomial_and_factorization(const rooted_mon& rm, const factorization& f, std::ostream& out) const;
 
     void explain_var_separated_from_zero(lpvar j);
 
     void explain_fixed_var(lpvar j);
     // x = 0 or y = 0 -> xy = 0
-    void basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f);
-    // x = 0 or y = 0 -> xy = 0
-    void basic_lemma_for_mon_non_zero_model_based_rm(const rooted_mon& rm, const factorization& f);
-
-    void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f);
 
     bool var_has_positive_lower_bound(lpvar j) const;
 
@@ -358,15 +329,6 @@ struct core {
     
     bool var_is_separated_from_zero(lpvar j) const;
     
-    // x = 0 or y = 0 -> xy = 0
-    bool basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f);
-
-    // use the fact that
-    // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const rooted_mon& rm, const factorization& f);
-    // use the fact that
-    // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m);
 
     bool vars_are_equiv(lpvar a, lpvar b) const;
 
@@ -374,61 +336,19 @@ struct core {
     void explain_equiv_vars(lpvar a, lpvar b);
     // use the fact that
     // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-    bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted_mon& rm, const factorization& f);
-
-    // use the fact
-    // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const rooted_mon& rm, const factorization& f);
-    // use the fact
-    // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m);
-    // use the fact
-    // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const rooted_mon& rm, const factorization& f);
-    void basic_lemma_for_mon_neutral_model_based(const rooted_mon& rm, const factorization& f);
-    
-    bool basic_lemma_for_mon_neutral_derived(const rooted_mon& rm, const factorization& factorization);
-
     void explain(const factorization& f, lp::explanation& exp);
 
     bool has_zero_factor(const factorization& factorization) const;
 
-    // if there are no zero factors then |m| >= |m[factor_index]|
-    void generate_pl_on_mon(const monomial& m, unsigned factor_index);
-    
-    // none of the factors is zero and the product is not zero
-    // -> |fc[factor_index]| <= |rm|
-    void generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index);   
 
     template <typename T>
     bool has_zero(const T& product) const;
 
     template <typename T>
     bool mon_has_zero(const T& product) const;
-
-    // x != 0 or y = 0 => |xy| >= |y|
-    void proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization);
-    // x != 0 or y = 0 => |xy| >= |y|
-    bool proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization);
-
-    void basic_lemma_for_mon_model_based(const rooted_mon& rm);
-
-    bool basic_lemma_for_mon_derived(const rooted_mon& rm);
-    
-    // Use basic multiplication properties to create a lemma
-    // for the given monomial.
-    // "derived" means derived from constraints - the alternative is model based
-    void basic_lemma_for_mon(const rooted_mon& rm, bool derived);
-
     void init_rm_to_refine();
-
     lp::lp_settings& settings();
-    
     unsigned random();
-    
-    // use basic multiplication properties to create a lemma
-    bool basic_lemma(bool derived);
-
     void map_monomial_vars_to_monomial_indices(unsigned i);
 
     void map_vars_to_monomials();

src/util/lp/nla_tangent_lemmas.cpp

@@ -220,6 +220,5 @@ void tangents::get_tang_points(point &a, point &b, bool below, const rational& v
     push_tang_points(a, b, xy, below, correct_val, val);
     TRACE("nla_solver", tout << "pushed a = "; print_point(a, tout); tout << "\npushed b = "; print_point(b, tout); tout << std::endl;);
 }
-
 }