From 0039b68ca3803b8e5cda9343cf3aa17153281ace Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Dec 2019 21:01:45 -1000 Subject: [PATCH] merged dependency.h from main repo Signed-off-by: Lev Nachmanson --- src/math/lp/nla_common.cpp | 15 ++++++------ src/math/lp/nla_common.h | 9 +++---- src/math/lp/nla_grobner.cpp | 8 +++---- src/math/lp/nla_grobner.h | 17 +++++++------ src/math/lp/nla_intervals.cpp | 16 ++++++------- src/math/lp/nla_intervals.h | 45 ++++++++++++++++------------------- 6 files changed, 51 insertions(+), 59 deletions(-) diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 3ce457b55..c2b485622 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -161,15 +161,15 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe } -template common::ci_dependency* common::create_sum_from_row(const T& row, +template u_dependency* common::create_sum_from_row(const T& row, nex_creator& cn, nex_creator::sum_factory& sum, bool fixed_as_scalars, - ci_dependency_manager* dep_manager + u_dependency_manager* dep_manager ) { TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); - ci_dependency * dep = nullptr; + u_dependency * dep = nullptr; SASSERT(row.size() > 1); sum.reset(); for (const auto &p : row) { @@ -190,9 +190,9 @@ template common::ci_dependency* common::create_sum_from_row(const T } template -common::ci_dependency* common::get_fixed_vars_dep_from_row(const T& row, ci_dependency_manager& dep_manager) { +u_dependency* common::get_fixed_vars_dep_from_row(const T& row, u_dependency_manager& dep_manager) { TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); - ci_dependency* dep = nullptr; + u_dependency* dep = nullptr; for (const auto &p : row) { lpvar j = p.var(); if (!c().is_monic_var(j)) { @@ -256,6 +256,5 @@ var_weight common::get_var_weight(lpvar j) const { } -template nla::common::ci_dependency* nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, bool, ci_dependency_manager*); - -template dependency_manager::dependency* nla::common::get_fixed_vars_dep_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, dependency_manager&); +template u_dependency* nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, bool, u_dependency_manager*); +template dependency_manager::config>::dependency* nla::common::get_fixed_vars_dep_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, scoped_dependency_manager&); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index b0ed12bc8..581c19ef5 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -109,22 +109,19 @@ struct common { } }; - struct ci_dependency_config { + struct u_dependency_config { typedef ci_value_manager value_manager; typedef region allocator; static const bool ref_count = false; typedef lp::constraint_index value; }; - typedef dependency_manager ci_dependency_manager; - - typedef ci_dependency_manager::dependency ci_dependency; // nex* nexvar(lpvar j, nex_creator&, svector & fixed_vars_constraints); nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool); template - ci_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, bool, ci_dependency_manager*); + u_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, bool, u_dependency_manager*); template - ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); + u_dependency* get_fixed_vars_dep_from_row(const T&, u_dependency_manager& dep_manager); void set_active_vars_weights(); var_weight get_var_weight(lpvar) const; }; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index c552fbbe1..374a64c6e 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -174,7 +174,7 @@ void grobner::add_row(unsigned i) { TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n'; for (auto p : row) c().print_var(p.var(), tout) << "\n"; ); nex_creator::sum_factory sf(m_nex_creator); - ci_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, m_look_for_fixed_vars_in_rows, &m_gc.dep()); + u_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, m_look_for_fixed_vars_in_rows, &m_gc.dep()); nex* e = m_nex_creator.simplify(sf.mk()); TRACE("grobner", tout << "e = " << *e << "\n";); m_gc.assert_eq_0(e, dep); @@ -792,7 +792,7 @@ std::ostream& grobner_core::display(std::ostream& out) const { return out; } -void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) { +void grobner_core::assert_eq_0(nex* e, u_dependency * dep) { if (e == nullptr || is_zero_scalar(e)) return; equation * eq = alloc(equation); @@ -807,7 +807,7 @@ void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) { update_stats_max_degree_and_size(eq); } -void grobner_core::init_equation(equation* eq, nex*e, common::ci_dependency * dep) { +void grobner_core::init_equation(equation* eq, nex*e, u_dependency * dep) { eq->m_bidx = m_equations_to_delete.size(); eq->m_dep = dep; eq->m_expr = e; @@ -819,7 +819,7 @@ grobner_core::~grobner_core() { del_equations(0); } -std::ostream& grobner_core::display_dependency(std::ostream& out, common::ci_dependency* dep) const { +std::ostream& grobner_core::display_dependency(std::ostream& out, u_dependency* dep) const { svector expl; m_dep_manager.linearize(dep, expl); lp::explanation e(expl); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 8f8bba765..894f5495d 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -77,7 +77,7 @@ public: class equation { unsigned m_bidx; //!< position at m_equations_to_delete nex * m_expr; // simplified expressionted monomials - common::ci_dependency * m_dep; //!< justification for the equality + u_dependency * m_dep; //!< justification for the equality public: unsigned get_num_monomials() const { switch(m_expr->type()) { @@ -102,7 +102,7 @@ public: } } const nex* expr() const { return m_expr; } - common::ci_dependency * dep() const { return m_dep; } + u_dependency * dep() const { return m_dep; } unsigned hash() const { return m_bidx; } friend class grobner_core; }; @@ -119,8 +119,7 @@ private: equation_set m_to_superpose; equation_set m_to_simplify; region m_alloc; - common::ci_value_manager m_val_manager; - mutable common::ci_dependency_manager m_dep_manager; + mutable u_dependency_manager m_dep_manager; nex_lt m_lt; bool m_changed_leading_term; params m_params; @@ -129,16 +128,16 @@ public: grobner_core(nex_creator& nc, reslimit& lim) : m_nex_creator(nc), m_limit(lim), - m_dep_manager(m_val_manager, m_alloc), + m_dep_manager(), m_changed_leading_term(false) {} ~grobner_core(); void reset(); bool compute_basis_loop(); - void assert_eq_0(nex*, common::ci_dependency * dep); + void assert_eq_0(nex*, u_dependency * dep); concat equations(); - common::ci_dependency_manager& dep() const { return m_dep_manager; } + u_dependency_manager& dep() const { return m_dep_manager; } void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const; void display_equations(std::ostream& out, equation_set const& v, char const* header) const; @@ -167,7 +166,7 @@ private: bool is_simpler(equation * eq1, equation * eq2); void del_equations(unsigned old_size); void del_equation(equation * eq); - void init_equation(equation* eq, nex*, common::ci_dependency* d); + void init_equation(equation* eq, nex*, u_dependency* d); void insert_to_simplify(equation *eq) { TRACE("grobner", display_equation(tout, *eq);); @@ -193,7 +192,7 @@ private: void update_stats_max_degree_and_size(const equation*); std::ostream& print_stats(std::ostream&) const; - std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const; + std::ostream& display_dependency(std::ostream& out, u_dependency*) const; bool equation_is_too_complex(const equation* eq) const { return eq->expr()->size() > m_params.m_expr_size_limit; } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index c5b38b90d..10345ee58 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -66,7 +66,7 @@ const nex* intervals::get_zero_interval_child(const nex_mul& e) const { return nullptr; } -std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream& out) const { +std::ostream & intervals::print_dependencies(u_dependency* deps , std::ostream& out) const { svector expl; m_dep_manager.linearize(deps, expl); { @@ -82,7 +82,7 @@ std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream& } // return true iff the interval of n is does not contain 0 -bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) { +bool intervals::check_nex(const nex* n, u_dependency* initial_deps) { m_core->lp_settings().stats().m_cross_nested_forms++; auto i = interval_of_expr(n, 1); if (!separated_from_zero(i)) { @@ -221,13 +221,13 @@ bool intervals::separated_from_zero_on_upper(const interval& i) const { return true; } -bool intervals::check_interval_for_conflict_on_zero(const interval & i, ci_dependency* dep) { +bool intervals::check_interval_for_conflict_on_zero(const interval & i, u_dependency* dep) { return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep); } bool intervals::check_interval_for_conflict_on_zero_upper( const interval & i, - ci_dependency* dep) { + u_dependency* dep) { if (!separated_from_zero_on_upper(i)) return false; @@ -241,7 +241,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper( return true; } -bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) { +bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, u_dependency* dep) { if (!separated_from_zero_on_lower(i)) { return false; } @@ -255,12 +255,12 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci return true; } -common::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { +u_dependency *intervals::mk_dep(lp::constraint_index ci) const { return m_dep_manager.mk_leaf(ci); } -common::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const { - intervals::ci_dependency * r = nullptr; +u_dependency *intervals::mk_dep(const lp::explanation& expl) const { + u_dependency * r = nullptr; for (auto p : expl) { if (r == nullptr) { r = m_dep_manager.mk_leaf(p.second); diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 4ac0540e3..ba55309e0 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -12,7 +12,7 @@ Author: Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) - + Revision History: @@ -29,12 +29,9 @@ namespace nla { class core; class intervals { - typedef common::ci_dependency_manager ci_dependency_manager; - typedef ci_dependency_manager::dependency ci_dependency; - class im_config { unsynch_mpq_manager& m_manager; - common::ci_dependency_manager& m_dep_manager; + u_dependency_manager& m_dep_manager; public: typedef unsynch_mpq_manager numeral_manager; @@ -52,8 +49,8 @@ class intervals { unsigned m_upper_open : 1; unsigned m_lower_inf : 1; unsigned m_upper_inf : 1; - ci_dependency* m_lower_dep; // justification for the lower bound - ci_dependency* m_upper_dep; // justification for the upper bound + u_dependency* m_lower_dep; // justification for the lower bound + u_dependency* m_upper_dep; // justification for the upper bound }; void add_deps(interval const& a, interval const& b, @@ -105,10 +102,10 @@ class intervals { // Reference to numeral manager numeral_manager& m() const { return m_manager; } - im_config(numeral_manager& m, ci_dependency_manager& d) :m_manager(m), m_dep_manager(d) {} + im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {} private: - ci_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const { - ci_dependency* dep = nullptr; + u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const { + u_dependency* dep = nullptr; if (dep_in_lower1(bd)) { dep = m_dep_manager.mk_join(dep, a.m_lower_dep); } @@ -124,8 +121,8 @@ class intervals { return dep; } - ci_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const { - ci_dependency* dep = nullptr; + u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const { + u_dependency* dep = nullptr; if (dep_in_lower1(bd)) { dep = m_dep_manager.mk_join(dep, a.m_lower_dep); } @@ -140,17 +137,17 @@ class intervals { region m_alloc; common::ci_value_manager m_val_manager; mutable unsynch_mpq_manager m_num_manager; - mutable ci_dependency_manager m_dep_manager; + mutable u_dependency_manager m_dep_manager; im_config m_config; mutable interval_manager m_imanager; core* m_core; public: - ci_dependency_manager& dep_manager() { return m_dep_manager; } + u_dependency_manager& dep_manager() { return m_dep_manager; } typedef interval_manager::interval interval; private: - ci_dependency* mk_dep(lp::constraint_index ci) const; - ci_dependency* mk_dep(lp::explanation const&) const; + u_dependency* mk_dep(lp::constraint_index ci) const; + u_dependency* mk_dep(lp::explanation const&) const; lp::lar_solver& ls(); const lp::lar_solver& ls() const; public: @@ -158,15 +155,15 @@ public: intervals(core* c, reslimit& lim) : m_alloc(), - m_dep_manager(m_val_manager, m_alloc), + m_dep_manager(), m_config(m_num_manager, m_dep_manager), m_imanager(lim, im_config(m_num_manager, m_dep_manager)), m_core(c) {} - ci_dependency* mk_join(ci_dependency* a, ci_dependency* b) { return m_dep_manager.mk_join(a, b); } - ci_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci); } + u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); } + u_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci); } - std::ostream& print_dependencies(ci_dependency*, std::ostream&) const; + std::ostream& print_dependencies(u_dependency*, std::ostream&) const; std::ostream& display(std::ostream& out, const intervals::interval& i) const; void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); } void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); } @@ -345,9 +342,9 @@ public: return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i); } - bool check_interval_for_conflict_on_zero(const interval& i, ci_dependency*); - bool check_interval_for_conflict_on_zero_lower(const interval& i, ci_dependency*); - bool check_interval_for_conflict_on_zero_upper(const interval& i, ci_dependency*); + bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*); + bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*); + bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*); mpq const& lower(interval const& a) const { return m_config.lower(a); } mpq const& upper(interval const& a) const { return m_config.upper(a); } inline bool is_empty(interval const& a) const { @@ -362,7 +359,7 @@ public: return false; } void reset() { m_alloc.reset(); } - bool check_nex(const nex*, ci_dependency*); + bool check_nex(const nex*, u_dependency*); typedef interval interv; void set_interval_for_scalar(interv&, const rational&); const nex* get_zero_interval_child(const nex_mul&) const;