From 971ae50ba31fdc54b034e20221ac4afa0312f9b7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 28 Oct 2019 17:12:48 -0700 Subject: [PATCH] move m_intervals to nla_core Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 14 +++----------- src/math/lp/horner.h | 7 +++---- src/math/lp/nla_basics_lemmas.cpp | 2 +- src/math/lp/nla_common.h | 4 +++- src/math/lp/nla_core.cpp | 5 +++-- src/math/lp/nla_core.h | 1 + src/math/lp/nla_grobner.cpp | 4 ++-- src/math/lp/nla_grobner.h | 2 +- src/math/lp/nla_monotone_lemmas.cpp | 2 +- src/math/lp/nla_order_lemmas.h | 2 +- src/math/lp/nla_tangent_lemmas.cpp | 2 +- 11 files changed, 20 insertions(+), 25 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 1058987eb..70e0a0a28 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) : common(c), m_intervals(c, c->reslim()), m_fixed_as_scalars(false) {} +horner::horner(core * c, intervals * i) : common(c, i), m_fixed_as_scalars(false) {} template bool horner::row_has_monomial_to_refine(const T& row) const { @@ -34,8 +34,8 @@ bool horner::row_has_monomial_to_refine(const T& row) const { return true; } return false; - } + // Returns true if the row has at least two monomials sharing a variable template bool horner::row_is_interesting(const T& row) const { @@ -69,11 +69,10 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) { return cn.done(); } - template bool horner::lemmas_on_row(const T& row) { cross_nested cn( - [this](const nex* n) { return m_intervals.check_cross_nested_expr(n, m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()) : nullptr); }, + [this](const nex* n) { return m_intervals->check_cross_nested_expr(n, m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); }, [this](unsigned j) { return c().var_is_fixed(j); }, [this]() { return c().random(); }, m_nex_creator); @@ -121,12 +120,5 @@ void horner::horner_lemmas() { } } } - - - - - - - } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 371280d5f..7f561b1f3 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -30,13 +30,12 @@ class core; class horner : common { - intervals m_intervals; - nex_sum m_row_sum; - unsigned m_row_index; + nex_sum m_row_sum; + unsigned m_row_index; bool m_fixed_as_scalars; public: typedef intervals::interval interv; - horner(core *core); + horner(core *core, intervals*); void horner_lemmas(); template // T has an iterator of (coeff(), var()) bool lemmas_on_row(const T&); diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index b2dc03616..b5486ad86 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) {} +basics::basics(core * c) : common(c, nullptr) {} // 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.h b/src/math/lp/nla_common.h index 7389a3e01..f2f3bb046 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -44,11 +44,13 @@ inline llc negate(llc cmp) { } class core; +class intervals; struct common { core* m_core; nex_creator m_nex_creator; + intervals* m_intervals; - common(core* c): m_core(c) {} + 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; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 560c0a66b..1888c71e4 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -29,8 +29,9 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_basics(this), m_order(this), m_monotone(this), - m_horner(this), - m_grobner(this), + m_intervals(this, lim), + m_horner(this, &m_intervals), + m_grobner(this, &m_intervals), m_emons(m_evars), m_reslim(lim) {} diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d94bf1032..690f03b2b 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -87,6 +87,7 @@ public: basics m_basics; order m_order; monotone m_monotone; + intervals m_intervals; horner m_horner; nla_settings m_nla_settings; nla_grobner m_grobner; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 80c39bb52..00ce49c00 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -21,8 +21,8 @@ #include "math/lp/nla_core.h" #include "math/lp/factorization_factory_imp.h" namespace nla { -nla_grobner::nla_grobner(core *c) - : common(c), +nla_grobner::nla_grobner(core *c, intervals *s) + : common(c, s), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc), m_changed_leading_term(false) {} diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 59010f72f..53b626022 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -95,7 +95,7 @@ class nla_grobner : common { nex_lt m_lt; bool m_changed_leading_term; public: - nla_grobner(core *core); + nla_grobner(core *core, intervals *); void grobner_lemmas(); ~nla_grobner(); private: diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 058dd7401..2d1dd7f57 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) {} +monotone::monotone(core * c) : common(c, nullptr) {} void monotone::monotonicity_lemma() { diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 341bef43d..cf4d38a7d 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) {} + order(core *c) : common(c, nullptr) {} void order_lemma(); private: diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index c1f254765..d654303cd 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -23,7 +23,7 @@ namespace nla { template rational tangents::val(T const& t) const { return m_core->val(t); } -tangents::tangents(core * c) : common(c) {} +tangents::tangents(core * c) : common(c, nullptr) {} std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std::ostream& out) const {