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

remove some lp_asserts

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-07-30 12:54:53 -07:00
parent 9cb713879e
commit 181bb60e36
4 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -209,7 +209,6 @@ public:
bool need_to_pivot_to_basis_tableau() const { bool need_to_pivot_to_basis_tableau() const {
lp_assert(m_A.is_correct());
unsigned m = m_A.row_count(); unsigned m = m_A.row_count();
for (unsigned i = 0; i < m; i++) { for (unsigned i = 0; i < m; i++) {
unsigned bj = m_basis[i]; unsigned bj = m_basis[i];

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

@ -621,7 +621,6 @@ divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
} }
template <typename T, typename X> bool lp_core_solver_base<T, X>:: template <typename T, typename X> bool lp_core_solver_base<T, X>::
pivot_column_tableau(unsigned j, unsigned piv_row_index) { pivot_column_tableau(unsigned j, unsigned piv_row_index) {
lp_assert(m_A.is_correct());
m_A.compress_row_if_needed(piv_row_index); m_A.compress_row_if_needed(piv_row_index);
if (!divide_row_by_pivot(piv_row_index, j)) if (!divide_row_by_pivot(piv_row_index, j))
return false; return false;

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

@ -790,12 +790,10 @@ public:
void compress_row_if_needed(unsigned i) { void compress_row_if_needed(unsigned i) {
compress_cells(m_rows[i], m_columns); compress_cells(m_rows[i], m_columns);
lp_assert(is_correct());
} }
void compress_column_if_needed(unsigned j) { void compress_column_if_needed(unsigned j) {
compress_cells(m_columns[j], m_rows); compress_cells(m_columns[j], m_rows);
lp_assert(is_correct());
} }
ref_row operator[](unsigned i) const { return ref_row(*this, i);} ref_row operator[](unsigned i) const { return ref_row(*this, i);}

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

@ -44,7 +44,6 @@ template <typename T, typename X> void static_matrix<T, X>::scan_row_ii_to_offse
template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, column_cell & c, unsigned pivot_col) { template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, column_cell & c, unsigned pivot_col) {
lp_assert(is_correct());
unsigned ii = c.var(); unsigned ii = c.var();
lp_assert(i < row_count() && ii < column_count() && i != ii); lp_assert(i < row_count() && ii < column_count() && i != ii);
T alpha = -get_val(c); T alpha = -get_val(c);
@ -83,7 +82,6 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
if (is_zero(c.coeff())) if (is_zero(c.coeff()))
remove_element(c); remove_element(c);
} }
lp_assert(is_correct());
return !rowii.empty(); return !rowii.empty();
} }
@ -295,6 +293,8 @@ 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;