mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

change type of m_ibounds to std::vector

Browse source
This commit is contained in:
Lev Nachmanson 2023-09-17 11:00:48 -07:00
parent 30b743d7b3
commit 66f6a0327f
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/math/lp/lp_bound_propagator.h
View file

@ -18,7 +18,7 @@ class lp_bound_propagator {
std::unordered_map<unsigned, unsigned> m_improved_upper_bounds; std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
T& m_imp; T& m_imp;
vector<implied_bound> m_ibounds; std::vector<implied_bound> m_ibounds;
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row; map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
// works for rows of the form x + y + sum of fixed = 0 // works for rows of the form x + y + sum of fixed = 0
@ -109,12 +109,12 @@ private:
public: public:
lp_bound_propagator(T& imp) : m_imp(imp) {} lp_bound_propagator(T& imp) : m_imp(imp) {}
const vector<implied_bound>& ibounds() const { return m_ibounds; } const std::vector<implied_bound>& ibounds() const { return m_ibounds; }
void init() { void init() {
m_improved_upper_bounds.clear(); m_improved_upper_bounds.clear();
m_improved_lower_bounds.clear(); m_improved_lower_bounds.clear();
m_ibounds.reset(); m_ibounds.clear();
m_column_types = &lp().get_column_types(); m_column_types = &lp().get_column_types();
} }
@ -151,7 +151,7 @@ private:
TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;); TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;);
j = lp().column_to_reported_index(j); j = lp().column_to_reported_index(j);
if (!try_get_value(m_improved_lower_bounds, j, k)) { if (!try_get_value(m_improved_lower_bounds, j, k)) {
m_improved_lower_bounds[j] = m_ibounds.size(); m_improved_lower_bounds[j] = static_cast<unsigned>(m_ibounds.size());
m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep)); m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep));
} else { } else {
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
@ -166,7 +166,7 @@ private:
j = lp().column_to_reported_index(j); j = lp().column_to_reported_index(j);
unsigned k; unsigned k;
if (!try_get_value(m_improved_upper_bounds, j, k)) { if (!try_get_value(m_improved_upper_bounds, j, k)) {
m_improved_upper_bounds[j] = m_ibounds.size(); m_improved_upper_bounds[j] = static_cast<unsigned>(m_ibounds.size());
m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound)); m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound));
} else { } else {
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
@ -333,7 +333,7 @@ private:
TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
} }
} else { } else {
m_improved_lower_bounds[j] = m_ibounds.size(); m_improved_lower_bounds[j] = static_cast<unsigned>(m_ibounds.size());
m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound));
TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout);); TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
} }
@ -347,7 +347,7 @@ private:
TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
} }
} else { } else {
m_improved_upper_bounds[j] = m_ibounds.size(); m_improved_upper_bounds[j] = static_cast<unsigned>(m_ibounds.size());
m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound));
TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout);); TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
} }