From e8c3324c3f0a6ccb5a233ee9d0256daa1661fa5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Mar 2020 01:30:06 -0700 Subject: [PATCH] reduce number of redundant arguments and pointers Signed-off-by: Nikolaj Bjorner --- src/math/lp/horner.cpp | 8 ++++---- src/math/lp/horner.h | 4 ++-- src/math/lp/nla_basics_lemmas.cpp | 2 +- src/math/lp/nla_common.cpp | 2 +- src/math/lp/nla_common.h | 13 ++++++------- src/math/lp/nla_core.cpp | 2 +- src/math/lp/nla_monotone_lemmas.cpp | 2 +- src/math/lp/nla_order_lemmas.h | 2 +- src/math/lp/nla_tangent_lemmas.cpp | 4 ++-- 9 files changed, 19 insertions(+), 20 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 5d1a9dcce..0fe968098 100644 --- a/src/math/lp/horner.cpp +++ b/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 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 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)); diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 352309c5e..87573467a 100644 --- a/src/math/lp/horner.h +++ b/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 // T has an iterator of (coeff(), var()) bool lemmas_on_row(const T&); @@ -48,6 +48,6 @@ public: template // 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 } diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 270d65a00..2d13a33cb 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/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 diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index d8e8fe92d..1b930f465 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -178,7 +178,7 @@ template 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) { diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index 7ef2580f2..1e3a0db7c 100644 --- a/src/math/lp/nla_common.h +++ b/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 rational val(T const& t) const; rational val(lpvar) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 8089be8ee..99a27d5da 100644 --- a/src/math/lp/nla_core.cpp +++ b/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), diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 978ca51df..f191c02f8 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/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() { diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index cf4d38a7d..341bef43d 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/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: diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index a95ede5e0..a50df5ecb 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/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()) {