From 1fff7bb51da144635228ff114589efd50e3fcf92 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Dec 2019 17:58:56 -0800 Subject: [PATCH] use u_map in lar_term Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 12 ++++---- src/test/lp/gomory_test.h | 4 +-- src/util/lp/lar_solver.cpp | 42 +++++++++++++-------------- src/util/lp/lar_solver.h | 14 ++++----- src/util/lp/lar_term.h | 58 +++++++++++++++++++++++--------------- 5 files changed, 70 insertions(+), 60 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9e7a3a5ba..eb0f6b9f3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2708,21 +2708,21 @@ public: lp::var_index vi = m_theory_var2var_index[v]; SASSERT(m_solver->is_term(vi)); lp::lar_term const& term = m_solver->get_term(vi); - for (auto const & coeff : term.m_coeffs) { - lp::var_index wi = coeff.first; + for (auto const mono : term) { + lp::var_index wi = mono.var(); lp::constraint_index ci; rational value; bool is_strict; if (m_solver->is_term(wi)) { return false; } - if (coeff.second.is_neg() == is_lub) { + if (mono.coeff().is_neg() == is_lub) { // -3*x ... <= lub based on lower bound for x. if (!m_solver->has_lower_bound(wi, ci, value, is_strict)) { return false; } if (is_strict) { - r += inf_rational(rational::zero(), coeff.second.is_pos()); + r += inf_rational(rational::zero(), mono.coeff().is_pos()); } } else { @@ -2730,10 +2730,10 @@ public: return false; } if (is_strict) { - r += inf_rational(rational::zero(), coeff.second.is_pos()); + r += inf_rational(rational::zero(), mono.coeff().is_pos()); } } - r += value * coeff.second; + r += value * mono.coeff(); set_evidence(ci); } TRACE("arith_verbose", tout << (is_lub?"lub":"glb") << " is " << r << "\n";); diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 0ac55406c..37817d0c7 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -186,8 +186,8 @@ struct gomory_test { void print_term(lar_term & t, std::ostream & out) { vector> row; - for (auto p : t.m_coeffs) - row.push_back(std::make_pair(p.second, p.first)); + for (auto p : t) + row.push_back(std::make_pair(p.coeff(), p.var())); print_row(out, row); } diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 59a4b957b..7a416741e 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -128,18 +128,18 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, } rs_of_evidence /= ratio; } else { - const lar_term * t = m_terms[adjust_term_index(be.m_j)]; - const auto first_coeff = *t->m_coeffs.begin(); - unsigned j = first_coeff.first; + lar_term & t = *m_terms[adjust_term_index(be.m_j)]; + auto first_coeff = t.begin(); + unsigned j = (*first_coeff).var(); auto it = coeff_map.find(j); if (it == coeff_map.end()) return false; - mpq ratio = it->second / first_coeff.second; - for (auto & p : t->m_coeffs) { - it = coeff_map.find(p.first); + mpq ratio = it->second / (*first_coeff).coeff(); + for (auto p : t) { + it = coeff_map.find(p.var()); if (it == coeff_map.end()) return false; - if (p.second * ratio != it->second) + if (p.coeff() * ratio != it->second) return false; } if (ratio < zero_of_type()) { @@ -686,8 +686,8 @@ void lar_solver::substitute_terms_in_linear_expression(const vector> & A, lp_assert(A.column_count() > 0); unsigned last_row = A.row_count() - 1; lp_assert(A.m_rows[last_row].size() == 0); - for (auto & t : ls->m_coeffs) { - lp_assert(!is_zero(t.second)); - var_index j = t.first; - A.set(last_row, j, - t.second); + for (auto t : *ls) { + lp_assert(!is_zero(t.coeff())); + var_index j = t.var(); + A.set(last_row, j, - t.coeff()); } unsigned basis_j = A.column_count() - 1; A.set(last_row, basis_j, mpq(1)); @@ -1364,8 +1364,8 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v for (unsigned i = 0; i < sz; i++) { var_index var = vars[i]; if (var >= m_terms_start_index) { // handle the term - for (auto & it : m_terms[var - m_terms_start_index]->m_coeffs) { - column_list.push_back(it.first); + for (auto it : *m_terms[var - m_terms_start_index]) { + column_list.push_back(it.var()); } } else { column_list.push_back(var); @@ -1560,8 +1560,8 @@ bool lar_solver::model_is_int_feasible() const { } bool lar_solver::term_is_int(const lar_term * t) const { - for (auto const & p : t->m_coeffs) - if (! (column_is_int(p.first) && p.second.is_int())) + for (auto const p : *t) + if (! (column_is_int(p.var()) && p.coeff().is_int())) return false; return true; } @@ -1920,10 +1920,10 @@ void lar_solver::fill_last_row_of_A_d(static_matrix & A, const l unsigned last_row = A.row_count() - 1; lp_assert(A.m_rows[last_row].empty()); - for (auto & t : ls->m_coeffs) { - lp_assert(!is_zero(t.second)); - var_index j = t.first; - A.set(last_row, j, -t.second.get_double()); + for (auto t : *ls) { + lp_assert(!is_zero(t.coeff())); + var_index j = t.var(); + A.set(last_row, j, -t.coeff().get_double()); } unsigned basis_j = A.column_count() - 1; diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f3aab29b2..f70d9e94a 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -545,17 +545,13 @@ public: void subs_term_columns(lar_term& t) { vector> columns_to_subs; - for (const auto & m : t.m_coeffs) { - unsigned tj = adjust_column_index_to_term_index(m.first); - if (tj == m.first) continue; - columns_to_subs.push_back(std::make_pair(m.first, tj)); + for (const auto & m : t) { + unsigned tj = adjust_column_index_to_term_index(m.var()); + if (tj == m.var()) continue; + columns_to_subs.push_back(std::make_pair(m.var(), tj)); } for (const auto & p : columns_to_subs) { - auto it = t.m_coeffs.find(p.first); - lp_assert(it != t.m_coeffs.end()); - mpq v = it->second; - t.m_coeffs.erase(it); - t.m_coeffs[p.second] = v; + t.subst_index(p.first, p.second); } } diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 64243f4e2..d3cb3293a 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -19,20 +19,23 @@ --*/ #pragma once #include "util/lp/indexed_vector.h" +#include "util/map.h" + namespace lp { -struct lar_term { +class lar_term { // the term evaluates to sum of m_coeffs - std::unordered_map m_coeffs; + u_map m_coeffs; // mpq m_v; +public: lar_term() {} void add_monomial(const mpq& c, unsigned j) { - auto it = m_coeffs.find(j); - if (it == m_coeffs.end()) { - m_coeffs.emplace(j, c); + auto *e = m_coeffs.find_core(j); + if (e == nullptr) { + m_coeffs.insert(j, c); } else { - it->second += c; - if (is_zero(it->second)) - m_coeffs.erase(it); + e->get_data().m_value += c; + if (e->get_data().m_value.is_zero()) + m_coeffs.erase(j); } } @@ -41,8 +44,9 @@ struct lar_term { } unsigned size() const { return static_cast(m_coeffs.size()); } - - const std::unordered_map & coeffs() const { + + template + const T & coeffs() const { return m_coeffs; } @@ -59,42 +63,51 @@ struct lar_term { vector> coeffs_as_vector() const { vector> ret; for (const auto & p : m_coeffs) { - ret.push_back(std::make_pair(p.second, p.first)); + ret.push_back(std::make_pair(p.m_value, p.m_key)); } return ret; } // j is the basic variable to substitute void subst(unsigned j, indexed_vector & li) { - auto it = m_coeffs.find(j); - if (it == m_coeffs.end()) return; - const mpq & b = it->second; + auto* it = m_coeffs.find_core(j); + if (it == nullptr) return; + const mpq & b = it->get_data().m_value; for (unsigned it_j :li.m_index) { add_monomial(- b * li.m_data[it_j], it_j); } - m_coeffs.erase(it); + m_coeffs.erase(j); + } + + // the monomial ax[j] is substituted by ax[k] + void subst_index(unsigned j, unsigned k) { + auto* it = m_coeffs.find_core(j); + if (it == nullptr) return; + mpq b = it->get_data().m_value; + m_coeffs.erase(j); + m_coeffs.insert(k, b); } bool contains(unsigned j) const { - return m_coeffs.find(j) != m_coeffs.end(); + return m_coeffs.contains(j); } void negate() { for (auto & t : m_coeffs) - t.second.neg(); + t.m_value.neg(); } template T apply(const vector& x) const { T ret(0); for (const auto & t : m_coeffs) { - ret += t.second * x[t.first]; + ret += t.m_value * x[t.m_key]; } return ret; } void clear() { - m_coeffs.clear(); + m_coeffs.reset(); } struct ival { @@ -108,7 +121,7 @@ struct lar_term { struct const_iterator { //fields - std::unordered_map::const_iterator m_it; + u_map< mpq>::iterator m_it; typedef const_iterator self_type; typedef ival value_type; @@ -118,19 +131,20 @@ struct lar_term { typedef std::forward_iterator_tag iterator_category; reference operator*() const { - return ival(m_it->first, m_it->second); + return ival(m_it->m_key, m_it->m_value); } self_type operator++() { self_type i = *this; m_it++; return i; } self_type operator++(int) { m_it++; return *this; } - const_iterator(std::unordered_map::const_iterator it) : m_it(it) {} + const_iterator(u_map::iterator it) : m_it(it) {} bool operator==(const self_type &other) const { return m_it == other.m_it; } bool operator!=(const self_type &other) const { return !(*this == other); } }; + const_iterator begin() const { return m_coeffs.begin();} const_iterator end() const { return m_coeffs.end(); } };