reduce number of redundant arguments and pointers

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/horner.cpp

@@ -25,7 +25,7 @@
 
 namespace nla {
 typedef intervals::interval interv;
-horner::horner(core * c, intervals * i) : common(c, i), m_row_sum(m_nex_creator) {}
+horner::horner(core * c) : common(c), m_row_sum(m_nex_creator) {}
 
 template <typename T>
 bool horner::row_has_monomial_to_refine(const T& row) const {
@@ -39,8 +39,8 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
 // Returns true if the row has at least two monomials sharing a variable
 template <typename T>
 bool horner::row_is_interesting(const T& row) const {
-    TRACE("nla_solver_details", m_core->print_row(row, tout););
-    if (row.size() > m_core->m_nla_settings.horner_row_length_limit()) {
+    TRACE("nla_solver_details", c().print_row(row, tout););
+    if (row.size() > c().m_nla_settings.horner_row_length_limit()) {
         TRACE("nla_solver_details", tout << "disregard\n";);
         return false;
     }
@@ -84,7 +84,7 @@ bool horner::lemmas_on_row(const T& row) {
         return false;
     
     cross_nested cn(
-        [this, dep](const nex* n) { return m_intervals->check_nex(n, dep); },
+        [this, dep](const nex* n) { return c().m_intervals.check_nex(n, dep); },
         [this](unsigned j)   { return c().var_is_fixed(j); },
         [this]() { return c().random(); }, m_nex_creator);
     bool ret = lemmas_on_expr(cn, to_sum(e));

src/math/lp/horner.h

@@ -34,7 +34,7 @@ class horner : common {
     unsigned         m_row_index;                      
 public:
     typedef intervals::interval interv;
-    horner(core *core, intervals*);
+    horner(core *core);
     bool horner_lemmas();
     template <typename T> // T has an iterator of (coeff(), var())
     bool lemmas_on_row(const T&);
@@ -48,6 +48,6 @@ public:
     
     template <typename T> // T has an iterator of (coeff(), var())
     bool row_has_monomial_to_refine(const T&) const;
-    bool interval_from_term_with_deps(const nex* e, interv&) const;
+    bool interval_from_term_with_deps(const nex* e, intervals::interval&) const;
 }; // end of horner
 }

src/math/lp/nla_basics_lemmas.cpp

@@ -22,7 +22,7 @@
 #include "math/lp/factorization_factory_imp.h"
 namespace nla {
 
-basics::basics(core * c) : common(c, nullptr) {}
+basics::basics(core * c) : common(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

src/math/lp/nla_common.cpp

@@ -178,7 +178,7 @@ template <typename T> void common::create_sum_from_row(const T& row,
                                                        nex_creator::sum_factory& sum,
                                                        u_dependency*& dep) {
 
-    TRACE("nla_horner", tout << "row="; m_core->print_row(row, tout) << "\n";);
+    TRACE("nla_horner", tout << "row="; m_core.print_row(row, tout) << "\n";);
     SASSERT(row.size() > 1);
     sum.reset();
     for (const auto &p : row) {

src/math/lp/nla_common.h

@@ -46,15 +46,14 @@ inline llc negate(llc cmp) {
 class core;
 class intervals;
 struct common {
-    core*                                        m_core;
+    core&                                        m_core;
     nex_creator                                  m_nex_creator;
-    intervals*                                   m_intervals;
     
-    common(core* c, intervals* i): m_core(c), m_intervals(i) {}
-    core& c() { return *m_core; }
-    const core& c() const { return *m_core; }
-    core& _() { return *m_core; }
-    const core& _() const { return *m_core; }
+    common(core* c): m_core(*c) {}
+    core& c() { return m_core; }
+    const core& c() const { return m_core; }
+    core& _() { return m_core; }
+    const core& _() const { return m_core; }
 
     template <typename T> rational val(T const& t) const;
     rational val(lpvar) const;

src/math/lp/nla_core.cpp

@@ -33,7 +33,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_order(this),
     m_monotone(this),
     m_intervals(this, lim),
-    m_horner(this, &m_intervals),
+    m_horner(this),
     m_pdd_manager(s.number_of_vars()),
     m_pdd_grobner(lim, m_pdd_manager),
     m_emons(m_evars),

src/math/lp/nla_monotone_lemmas.cpp

@@ -21,7 +21,7 @@
 #include "math/lp/nla_core.h"
 namespace nla {
 
-monotone::monotone(core * c) : common(c, nullptr) {}
+monotone::monotone(core * c) : common(c) {}
 
     
 void monotone::monotonicity_lemma() {

src/math/lp/nla_order_lemmas.h

@@ -25,7 +25,7 @@ namespace nla {
 class core;
 class order: common {
 public:
-    order(core *c) : common(c, nullptr) {}
+    order(core *c) : common(c) {}
     void order_lemma();
     
 private:

src/math/lp/nla_tangent_lemmas.cpp

@@ -168,7 +168,7 @@ struct imp {
         return out;
     }
 
-    bool  plane_is_correct_cut(const point& plane) const {
+    bool plane_is_correct_cut(const point& plane) const {
         TRACE("nla_solver", tout << "plane = " << plane << "\n";
               tout << "tang_plane() = " << tang_plane(plane) << ", v = " << m_v << ", correct_v = " << m_correct_v << "\n";);
         SASSERT((m_below && m_v < m_correct_v) ||
@@ -179,7 +179,7 @@ struct imp {
     }    
 };
 
-tangents::tangents(core * c) : common(c, nullptr) {}
+tangents::tangents(core * c) : common(c) {}
     
 void tangents::tangent_lemma() {
     if (!c().m_nla_settings.run_tangents()) {