rebase with master branch

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

src/math/lp/nla_basics_lemmas.cpp

@@ -359,7 +359,8 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
 
 // x != 0 or y = 0 => |xy| >= |y|
 void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
-    if (c().factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,           return;     // or smaller than 1
+    if (c().has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,        
+        return;     // or smaller than 1
     rational rmv = abs(var_val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
@@ -485,6 +486,8 @@ bool basics::is_separated_from_zero(const factorization& f) const {
     return true;
 }
 
+
+
 // here we use the fact xy = 0 -> x = 0 or y = 0
 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {        
     TRACE("nla_solver",  c().trace_print_monic_and_factorization(rm, f, tout););

src/math/lp/nla_core.cpp

@@ -1895,23 +1895,4 @@ bool core::influences_nl_var(lpvar j) const {
     return false;
 }
 
-bool core::factorization_has_real(const factorization& f) const {
-    for (const factor& fc: f) {
-        lpvar j = var(fc);
-        if (!var_is_int(j))
-            return true;
-    }
-    return false;
-}
-
-bool core::monic_has_real(const monic& m) const {
-    if (!var_is_int(m.var()))
-        return true;
-    for (lpvar j : m) {
-        if (!var_is_int(j))
-            return true;
-    }
-    return false;
-}
-
 } // end of nla

src/math/lp/nla_core.h

@@ -24,7 +24,6 @@
 #include "math/lp/horner.h"
 #include "math/lp/nla_intervals.h"
 #include "math/grobner/pdd_solver.h"
-#include "math/lp/nla_lemma.h"
 #include "nlsat/nlsat_solver.h"
 
 
@@ -68,6 +67,18 @@ public:
     const rational& rs() const { return m_rs; };
 };
 
+class lemma {
+    vector<ineq>     m_ineqs;
+    lp::explanation  m_expl;
+public:
+    void push_back(const ineq& i) { m_ineqs.push_back(i);}
+    size_t size() const { return m_ineqs.size() + m_expl.size(); }
+    const vector<ineq>& ineqs() const { return m_ineqs; }
+    vector<ineq>& ineqs() { return m_ineqs; }
+    lp::explanation& expl() { return m_expl; }
+    const lp::explanation& expl() const { return m_expl; }
+    bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
+};
 
 class core;
 //
@@ -153,7 +164,7 @@ public:
 
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
-    const lp::u_set& to_refine() const { return m_to_refine; }         
+    
     const lp::u_set&  active_var_set () const { return m_active_var_set;}
     bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
 
@@ -441,8 +452,9 @@ public:
     bool patch_blocker(lpvar u, const monic& m) const;
     bool has_big_num(const monic&) const;
     bool var_is_big(lpvar) const;
-    bool factorization_has_real(const factorization&) const;
-    bool monic_has_real(const monic&) const;
+    bool has_real(const factorization&) const;
+    bool has_real(const monic& m) const;
+
 };  // end of core
 
 struct pp_mon {

src/math/lp/nla_lemma.h

@@ -1,40 +0,0 @@
-/*++
-  Copyright (c) 2017 Microsoft Corporation
-
-  Module Name:
-
-  nla_core.h
-
-  Author:
-  Nikolaj Bjorner (nbjorner)
-  Lev Nachmanson (levnach)
-
---*/
-#pragma once
-namespace nla {
-struct ineq {
-    lp::lconstraint_kind m_cmp;
-    lp::lar_term         m_term;
-    rational             m_rs;
-    ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {}
-    bool operator==(const ineq& a) const {
-        return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
-    }
-    const lp::lar_term& term() const { return m_term; };
-    lp::lconstraint_kind cmp() const { return m_cmp;  };
-    const rational& rs() const { return m_rs; };
-};
-
-class lemma {
-    vector<ineq>     m_ineqs;
-    lp::explanation  m_expl;
-public:
-    void push_back(const ineq& i) { m_ineqs.push_back(i);}
-    size_t size() const { return m_ineqs.size() + m_expl.size(); }
-    const vector<ineq>& ineqs() const { return m_ineqs; }
-    vector<ineq>& ineqs() { return m_ineqs; }
-    lp::explanation& expl() { return m_expl; }
-    const lp::explanation& expl() const { return m_expl; }
-    bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
-};
-}

src/math/lp/nla_monotone_lemmas.cpp

@@ -11,25 +11,13 @@ namespace nla {
 
 monotone::monotone(core * c) : common(c) {}
 
-// return false if at least one variable, including the monic var, is real,
-// or one of the variable from m.vars() is zero
-bool monotone::monotonicity_lemma_candidate(const monic & m) const {
-    if (!c().var_is_int(m.var()))
-        return false;
-    for (lpvar j : m) {
-        if (!c().var_is_int(j) || val(j).is_zero())
-            return false;        
-    }
-    return true;
-}
     
 void monotone::monotonicity_lemma() {
     unsigned shift = random();
     unsigned size = c().m_to_refine.size();
     for (unsigned i = 0; i < size && !done(); i++) { 
         lpvar v = c().m_to_refine[(i + shift) % size];
-        if (monotonicity_lemma_candidate(c().emons()[v]))
-            monotonicity_lemma(c().emons()[v]);
+        monotonicity_lemma(c().emons()[v]);
     }
 }
    
@@ -45,9 +33,6 @@ void monotone::monotonicity_lemma(monic const& m) {
         monotonicity_lemma_lt(m, prod_val);
     else if (m_val > prod_val)
         monotonicity_lemma_gt(m, prod_val);
-    else {
-        TRACE("nla_solver", tout << "equal\n";);
-    }
 }
 
 void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {

src/math/lp/nla_monotone_lemmas.h

@@ -18,6 +18,5 @@ private:
     void monotonicity_lemma_lt(const monic& m, const rational& prod_val);    
     std::vector<rational> get_sorted_key(const monic& rm) const;
     vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
-    bool monotonicity_lemma_candidate(const monic& m) const;
 };
 }

src/math/lp/nla_solver.cpp

@@ -12,8 +12,6 @@
 #include "math/lp/var_eqs.h"
 #include "math/lp/factorization.h"
 #include "math/lp/nla_solver.h"
-#include "math/lp/nla_core.h"
-
 namespace nla {
 
 nla_settings& solver::settings() { return m_core->m_nla_settings; }

src/math/lp/nla_solver.h

@@ -14,8 +14,7 @@ Author:
 #include "math/lp/lar_solver.h"
 #include "math/lp/monic.h"
 #include "math/lp/nla_settings.h"
-#include "math/lp/nla_lemma.h"
-
+#include "math/lp/nla_core.h"
 namespace nra {
 class solver;
 }

src/math/lp/nra_solver.cpp

@@ -33,7 +33,7 @@ struct solver::imp {
         m_nla_core(nla_core) {}
 
     bool need_check() {
-        return m_nla_core.to_refine().size() != 0;
+        return m_nla_core.m_to_refine.size() != 0;
     }
 
 

src/smt/theory_lra.cpp

@@ -990,7 +990,6 @@ public:
         
         lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
-        m_switcher.m_use_nla = true;
         m_lia = alloc(lp::int_solver, *m_solver.get());
         get_one(true);
         get_zero(true);