forgotten changes after a rebase

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

src/math/lp/CMakeLists.txt

@@ -47,7 +47,8 @@ z3_add_component(lp
     polynomial
     nlsat
   PYG_FILES
-    lp_params.pyg
+  	lp_params.pyg
+  	nla_params.pyg
 )
 
 include_directories(${src_SOURCE_DIR})

src/math/lp/factorization_factory_imp.cpp

@@ -22,8 +22,8 @@
 namespace nla {
         
 factorization_factory_imp::factorization_factory_imp(const monomial& rm, const core& s) :
-    factorization_factory(rm.rvars(), &s.m_emons[rm.var()]),
-    m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }
+    factorization_factory(rm.rvars(), &s.emons()[rm.var()]),
+    m_core(s), m_mon(s.emons()[rm.var()]), m_rm(rm) { }
         
 bool factorization_factory_imp::find_canonical_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
     return m_core.find_canonical_monomial_of_vars(vars, i);

src/math/lp/lar_solver.cpp

@@ -2256,6 +2256,10 @@ bool lar_solver::column_corresponds_to_term(unsigned j) const {
     return m_var_register.local_to_external(j) >= m_terms_start_index;
 }
 
+var_index lar_solver::to_column(unsigned ext_j) const {
+    return m_var_register.external_to_local(ext_j);
+}
+
 bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& delta) {
     unsigned tj = term_index + m_terms_start_index;
     unsigned j;

src/math/lp/lar_solver.h

@@ -630,6 +630,7 @@ public:
     lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; }
     bool column_corresponds_to_term(unsigned) const;
     void catch_up_in_updating_int_solver();
+    var_index to_column(unsigned ext_j) const;
     bool tighten_term_bounds_by_delta(unsigned, const impq&);
     void round_to_integer_solution();
     void update_delta_for_terms(const impq & delta, unsigned j, const vector<unsigned>&);

src/math/lp/lp_params.pyg

@@ -7,12 +7,7 @@ def_module_params('lp',
                    ('simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
                    ('enable_hnf', BOOL, True, 'enable hnf cuts'),
                    ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
-                   ('nla', BOOL, False, 'call nonlinear integer solver with incremental linearization')
-
-                          ))           
-
-
-    
+                   ('nla', BOOL, False, 'call nonlinear integer solver with incremental linearization'),
                    ('print_ext_var_names', BOOL, False, 'print external variable names')
                           ))
 

src/math/lp/nla_basics_lemmas.cpp

@@ -104,7 +104,7 @@ bool basics::basic_sign_lemma_model_based() {
     unsigned start = c().random();
     unsigned sz = c().m_to_refine.size();
     for (unsigned i = sz; i-- > 0; ) {
-        monomial const& m = c().m_emons[c().m_to_refine[(start + i) % sz]];
+        monomial const& m = c().emons()[c().m_to_refine[(start + i) % sz]];
         int mon_sign = nla::rat_sign(val(m));
         int product_sign = c().rat_sign(m);
         if (mon_sign != product_sign) {
@@ -327,7 +327,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monomial& rm, const fact
 bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomial& rm, const factorization& f) {
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
 
-    lpvar mon_var =  c().m_emons[rm.var()].var();
+    lpvar mon_var =  c().emons()[rm.var()].var();
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
         
     const auto mv = val(mon_var);
@@ -634,7 +634,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
 bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const monomial& rm, const factorization& f) {
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
 
-    lpvar mon_var = c().m_emons[rm.var()].var();
+    lpvar mon_var = c().emons()[rm.var()].var();
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
         
     const auto mv = val(mon_var);

src/math/lp/nla_core.h

@@ -359,7 +359,7 @@ struct pp_mon {
     core const& c;
     monomial const& m;
     pp_mon(core const& c, monomial const& m): c(c), m(m) {}
-    pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
+    pp_mon(core const& c, lpvar v): c(c), m(c.emons()[v]) {}
 };
 struct pp_mon_with_vars {
     core const& c;

src/math/lp/nla_monotone_lemmas.cpp

@@ -30,7 +30,7 @@ void monotone::monotonicity_lemma() {
     unsigned size = c().m_to_refine.size();
     for(unsigned i = 0; i < size && !done(); i++) { 
         lpvar v = c().m_to_refine[(i + shift) % size];
-        monotonicity_lemma(c().m_emons[v]);
+        monotonicity_lemma(c().emons()[v]);
     }
 }
 

src/math/lp/nla_order_lemmas.cpp

@@ -105,7 +105,7 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) {
     SASSERT(ac.size() == 2);    
     lpvar c = ac.vars()[k];
     
-    for (monomial const& bd : _().m_emons.get_products_of(c)) {
+    for (monomial const& bd : _().emons().get_products_of(c)) {
         if (bd.var() == ac.var()) continue;
         TRACE("nla_solver", tout << "bd = " << pp_mon_with_vars(_(), bd););
         order_lemma_on_factor_binomial_rm(ac, k, bd);
@@ -244,14 +244,14 @@ bool order::order_lemma_on_ac_explore(const monomial& rm, const factorization& a
     TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
     if (c.is_var()) {
         TRACE("nla_solver", tout << "var(c) = " << var(c););
-        for (monomial const& bc : _().m_emons.get_use_list(c.var())) {
+        for (monomial const& bc : _().emons().get_use_list(c.var())) {
             if (order_lemma_on_ac_and_bc(rm ,ac, k, bc)) {
                 return true;
             }
         }
     } 
     else {
-        for (monomial const& bc : _().m_emons.get_products_of(c.var())) {
+        for (monomial const& bc : _().emons().get_products_of(c.var())) {
             if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) {
                 return true;
             }

src/math/lp/numeric_pair.h

@@ -148,6 +148,30 @@ struct numeric_pair {
     template <typename X, typename Y>
     numeric_pair(X xp, Y yp) : x(convert_struct<T, X>::convert(xp)), y(convert_struct<T, Y>::convert(yp)) {}
 
+    bool operator<(const T& a) const {
+        return x < a || (x == a && y < 0);
+    }
+
+    bool operator>(const T& a) const {
+        return x > a || (x == a && y > 0);
+    }
+
+    bool operator==(const T& a) const  {
+        return a == x && y == 0;
+    }
+
+    bool operator!=(const T& a) const  {
+        return !(*this == a);
+    }
+
+    bool operator<=(const T& a) const  {
+        return *this < a || *this == a;
+    }
+
+    bool operator>=(const T& a) const  {
+        return *this > a || *this == a;
+    }
+
     bool operator<(const numeric_pair& a) const {
         return x < a.x || (x == a.x && y < a.y);
     }

src/smt/theory_lra.cpp

@@ -1055,7 +1055,7 @@ public:
         default:
             break;
         }         
-        auto vi = get_var_index(b->get_var());
+        auto vi = get_lpvar(b->get_var());
         return m_solver->compare_values(vi, k, b->get_value()) ? l_true : l_false;
     }