From 6366f8f6b27698d3b4d31c6a632300e8a1c4486c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Aug 2023 14:05:07 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/for_each_expr.cpp | 6 +++--- src/ast/for_each_expr.h | 6 +++--- src/math/lp/lar_solver.cpp | 15 +++++---------- src/math/lp/lar_solver.h | 2 +- src/math/lp/var_register.h | 12 +++--------- src/util/util.h | 4 ++-- 6 files changed, 17 insertions(+), 28 deletions(-) diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 832c1d0bc..8feb217db 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -109,9 +109,9 @@ bool has_skolem_functions(expr * n) { subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {} subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); } -subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); } -subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); } -subterms::iterator::iterator(subterms& f, ptr_vector* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) { +subterms::iterator subterms::begin() const { return iterator(* this, m_esp, m_vp, true); } +subterms::iterator subterms::end() const { return iterator(*this, nullptr, nullptr, false); } +subterms::iterator::iterator(subterms const& f, ptr_vector* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) { if (!esp) m_esp = &m_es; else diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index 0ba0dc992..77b01e939 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -186,7 +186,7 @@ public: expr_mark m_visited; expr_mark* m_visitedp = nullptr; public: - iterator(subterms& f, ptr_vector* esp, expr_mark* vp, bool start); + iterator(subterms const& f, ptr_vector* esp, expr_mark* vp, bool start); expr* operator*(); iterator operator++(int); iterator& operator++(); @@ -198,8 +198,8 @@ public: static subterms ground(expr_ref const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); } static subterms all(expr_ref_vector const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); } static subterms ground(expr_ref_vector const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); } - iterator begin(); - iterator end(); + iterator begin() const; + iterator end() const; }; class subterms_postorder { diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 852c47397..ddfdb1437 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -258,7 +258,7 @@ namespace lp { m_crossed_bounds_column.pop(k); unsigned n = m_columns_to_ul_pairs.peek_size(k); m_var_register.shrink(n); - pop_tableau(); + pop_tableau(n); lp_assert(A_r().column_count() == n); TRACE("lar_solver_details", for (unsigned j = 0; j < n; j++) { @@ -1326,15 +1326,15 @@ namespace lp { lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); } - void lar_solver::pop_tableau() { + void lar_solver::pop_tableau(unsigned old_size) { lp_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); lp_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); // We remove last variables starting from m_column_names.size() to m_vec_of_canonic_left_sides.size(). // At this moment m_column_names is already popped - unsigned size = m_var_register.size(); - while (A_r().column_count() > size) + + while (A_r().column_count() > old_size) remove_last_column_from_tableau(); lp_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); @@ -1544,12 +1544,7 @@ namespace lp { // terms bool lar_solver::all_vars_are_registered(const vector>& coeffs) { - for (const auto& p : coeffs) { - if (p.second >= m_var_register.size()) { - return false; - } - } - return true; + return all_of(coeffs, [&](const auto& p) { return p.second < m_var_register.size(); }); } void lar_solver::subst_known_terms(lar_term* t) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 9faa40979..7c1f9575b 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -225,7 +225,7 @@ class lar_solver : public column_namer { void remove_last_column_from_basis_tableau(unsigned j); void remove_last_column_from_tableau(); - void pop_tableau(); + void pop_tableau(unsigned old_size); void clean_inf_heap_of_r_solver_after_pop(); inline bool column_value_is_integer(unsigned j) const { return get_column_value(j).is_int(); } bool model_is_int_feasible() const; diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index 49767274d..3b326788b 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -72,9 +72,8 @@ public: svector vars() const { svector ret; - for (const auto& p : m_local_to_external) { + for (const auto& p : m_local_to_external) ret.push_back(p.external_j()); - } return ret; } @@ -126,11 +125,7 @@ public: } bool has_int_var() const { - for (const auto & vi : m_local_to_external) { - if (vi.is_integer()) - return true; - } - return false; + return any_of(m_local_to_external, [&](const auto& vi) { return vi.is_integer(); }); } bool local_is_int(unsigned j) const { @@ -138,9 +133,8 @@ public: } void shrink(unsigned shrunk_size) { - for (unsigned j = size(); j-- > shrunk_size;) { + for (unsigned j = size(); j-- > shrunk_size;) m_external_to_local.erase(m_local_to_external[j].external_j()); - } m_local_to_external.resize(shrunk_size); } diff --git a/src/util/util.h b/src/util/util.h index 6d4efb671..1e2310eb3 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -363,7 +363,7 @@ void set_fatal_error_handler(void (*pfn)(int error_code)); template -bool any_of(S& set, T const& p) { +bool any_of(S const& set, T const& p) { for (auto const& s : set) if (p(s)) return true; @@ -371,7 +371,7 @@ bool any_of(S& set, T const& p) { } template -bool all_of(S& set, T const& p) { +bool all_of(S const& set, T const& p) { for (auto const& s : set) if (!p(s)) return false;