mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

use CASSERT instead of lp_assert for static_matrix

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-07-30 14:34:03 -07:00
parent 181bb60e36
commit 0ee68220e1
5 changed files with 9 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/lar_solver.cpp
View file

@ -1373,7 +1373,7 @@ void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) {
lp_assert(A_r().m_columns[j].live_size() == 0); lp_assert(A_r().m_columns[j].live_size() == 0);
A_r().m_rows.pop_back(); A_r().m_rows.pop_back();
A_r().m_columns.pop_back(); A_r().m_columns.pop_back();
lp_assert(A_r().is_correct()); CASSERT("check_static_matrix", A_r().is_correct());
slv.m_b.pop_back(); slv.m_b.pop_back();
} }

2
src/util/lp/lp_core_solver_base.h
View file

@ -230,7 +230,7 @@ public:
bool reduced_costs_are_correct_tableau() const { bool reduced_costs_are_correct_tableau() const {
if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows)
return true; return true;
lp_assert(m_A.is_correct()); CASSERT("check_static_matrix", m_A.is_correct());
if (m_using_infeas_costs) { if (m_using_infeas_costs) {
if (infeasibility_costs_are_correct() == false) { if (infeasibility_costs_are_correct() == false) {
return false; return false;

6
src/util/lp/lp_core_solver_base_def.h
View file

@ -616,7 +616,7 @@ divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
} }
} }
coeff = one_of_type<T>(); coeff = one_of_type<T>();
lp_assert(m_A.is_correct()); CASSERT("check_static_matrix", m_A.is_correct());
return true; return true;
} }
template <typename T, typename X> bool lp_core_solver_base<T, X>:: template <typename T, typename X> bool lp_core_solver_base<T, X>::
@ -639,7 +639,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
if (pivot_col_cell_index != 0) if (pivot_col_cell_index != 0)
m_A.swap_with_head_cell(j, pivot_col_cell_index); m_A.swap_with_head_cell(j, pivot_col_cell_index);
lp_assert(m_A.is_correct()); CASSERT("check_static_matrix", m_A.is_correct());
while (column.live_size() > 1) { while (column.live_size() > 1) {
auto & c = column.back(); auto & c = column.back();
if (c.dead()) { if (c.dead()) {
@ -655,7 +655,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
} }
m_A.compress_column_if_needed(j); m_A.compress_column_if_needed(j);
lp_assert(column.live_size() == 1); lp_assert(column.live_size() == 1);
lp_assert(m_A.is_correct()); CASSERT("check_static_matrix", m_A.is_correct());
if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs) if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)
pivot_to_reduced_costs_tableau(piv_row_index, j); pivot_to_reduced_costs_tableau(piv_row_index, j);

8
src/util/lp/static_matrix.h
View file

@ -184,7 +184,7 @@ public:
c.next_dead_index() = m_first_dead; c.next_dead_index() = m_first_dead;
m_first_dead = j; m_first_dead = j;
} }
lp_assert(is_correct()); CASSERT("check_static_matrix", is_correct());
} }
bool is_correct() const { bool is_correct() const {
@ -264,7 +264,7 @@ public:
c.next_dead_index() = m_first_dead; c.next_dead_index() = m_first_dead;
m_first_dead = j; m_first_dead = j;
} }
lp_assert(is_correct()); CASSERT("check_static_matrix", is_correct());
} }
const column_cell& operator[] (unsigned i) const { return m_cells[i];} const column_cell& operator[] (unsigned i) const { return m_cells[i];}
@ -330,7 +330,7 @@ public:
} }
m_cells[0] = m_cells[i]; m_cells[0] = m_cells[i];
m_cells[i] = head_copy; m_cells[i] = head_copy;
lp_assert(is_correct()); CASSERT("check_static_matrix", is_correct());
} }
column_cell & add_cell(unsigned i, unsigned & index) { column_cell & add_cell(unsigned i, unsigned & index) {
@ -580,7 +580,7 @@ public:
m_columns.pop_back(); // delete the last column m_columns.pop_back(); // delete the last column
m_stack.pop(); m_stack.pop();
} }
lp_assert(is_correct()); CASSERT("check_static_matrix", is_correct());
} }
void multiply_row(unsigned row, T const & alpha) { void multiply_row(unsigned row, T const & alpha) {

2
src/util/lp/static_matrix_def.h
View file

@ -293,8 +293,6 @@ template <typename T, typename X> T static_matrix<T, X>::get_row_balance(unsi
} }
template <typename T, typename X> bool static_matrix<T, X>::is_correct() const { template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
if (m_rows.size() > 100 || m_columns.size() > 100)
return true;
for (unsigned i = 0; i < m_rows.size(); i++) { for (unsigned i = 0; i < m_rows.size(); i++) {
auto &r = m_rows[i]; auto &r = m_rows[i];
std::unordered_set<unsigned> s; std::unordered_set<unsigned> s;