From 8035edbe65f295c43d5dd7bcce84c6d458d2f70a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Apr 2025 11:10:26 -0700 Subject: [PATCH] remove lp_assert --- src/math/lp/bound_analyzer_on_row.h | 6 +- src/math/lp/core_solver_pretty_printer_def.h | 4 +- src/math/lp/dense_matrix.h | 2 +- src/math/lp/dense_matrix_def.h | 2 +- src/math/lp/general_matrix.h | 16 +- src/math/lp/gomory.cpp | 16 +- src/math/lp/hnf.h | 50 +++--- src/math/lp/hnf_cutter.cpp | 6 +- src/math/lp/incremental_vector.h | 8 +- src/math/lp/indexed_vector_def.h | 2 +- src/math/lp/int_branch.cpp | 2 +- src/math/lp/int_cube.cpp | 4 +- src/math/lp/int_solver.cpp | 20 +-- src/math/lp/lar_core_solver.h | 20 +-- src/math/lp/lar_core_solver_def.h | 14 +- src/math/lp/lar_solver.cpp | 151 +++++++++--------- src/math/lp/lar_solver.h | 4 +- src/math/lp/lp_bound_propagator.h | 28 ++-- src/math/lp/lp_core_solver_base.h | 22 +-- src/math/lp/lp_core_solver_base_def.h | 20 +-- src/math/lp/lp_primal_core_solver.h | 38 ++--- src/math/lp/lp_primal_core_solver_def.h | 8 +- .../lp/lp_primal_core_solver_tableau_def.h | 28 ++-- src/math/lp/lp_settings.h | 4 +- src/math/lp/lp_utils.h | 1 - src/math/lp/permutation_matrix.h | 2 +- src/math/lp/permutation_matrix_def.h | 4 +- src/math/lp/stacked_vector.h | 14 +- src/math/lp/static_matrix.h | 16 +- src/math/lp/static_matrix_def.h | 2 +- src/math/lp/test_bound_analyzer.h | 4 +- src/math/lp/var_register.h | 2 +- src/test/lp/gomory_test.h | 20 +-- src/test/lp/lp.cpp | 95 +++++------ src/test/lp/smt_reader.h | 26 +-- 35 files changed, 332 insertions(+), 329 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index b80702e17..cbe640399 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -92,12 +92,12 @@ namespace lp { } const impq & ub(unsigned j) const { - lp_assert(upper_bound_is_available(j)); + SASSERT(upper_bound_is_available(j)); return get_upper_bound(j); } const impq & lb(unsigned j) const { - lp_assert(lower_bound_is_available(j)); + SASSERT(lower_bound_is_available(j)); return get_lower_bound(j); } @@ -287,7 +287,7 @@ namespace lp { // mpq a; unsigned j; // while (it->next(a, j)) { // if (be.m_j == j) continue; - // lp_assert(bound_is_available(j, is_neg(a) ? lower_bound : !lower_bound)); + // SASSERT(bound_is_available(j, is_neg(a) ? lower_bound : !lower_bound)); // be.m_vector_of_bound_signatures.emplace_back(a, j, numeric_traits:: // is_neg(a)? lower_bound: !lower_bound); // } diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index 6d35273af..cdd99932a 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -326,7 +326,7 @@ template void core_solver_pretty_printer::print_g if (m_squash_blanks && string_is_trivial(s)) continue; int number_of_blanks = width - static_cast(s.size()); - lp_assert(number_of_blanks >= 0); + SASSERT(number_of_blanks >= 0); m_out << signs[col] << ' '; print_blanks_local(number_of_blanks, m_out); m_out << s << ' '; @@ -335,7 +335,7 @@ template void core_solver_pretty_printer::print_g string rs = T_to_string(rst); int nb = m_rs_width - static_cast(rs.size()); - lp_assert(nb >= 0); + SASSERT(nb >= 0); print_blanks_local(nb + 1, m_out); m_out << rs << std::endl; } diff --git a/src/math/lp/dense_matrix.h b/src/math/lp/dense_matrix.h index 6b039a920..ab1d92229 100644 --- a/src/math/lp/dense_matrix.h +++ b/src/math/lp/dense_matrix.h @@ -47,7 +47,7 @@ public: dense_matrix(unsigned m, unsigned n); dense_matrix operator*=(matrix const & a) { - lp_assert(column_count() == a.row_count()); + SASSERT(column_count() == a.row_count()); dense_matrix c(row_count(), a.column_count()); for (unsigned i = 0; i < row_count(); i++) { for (unsigned j = 0; j < a.column_count(); j++) { diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h index e850a9acd..858d10eaa 100644 --- a/src/math/lp/dense_matrix_def.h +++ b/src/math/lp/dense_matrix_def.h @@ -175,7 +175,7 @@ template void dense_matrix::multiply_row_by_const template dense_matrix operator* (matrix & a, matrix & b){ - lp_assert(a.column_count() == b.row_count()); + SASSERT(a.column_count() == b.row_count()); dense_matrix ret(a.row_count(), b.column_count()); for (unsigned i = 0; i < ret.m_m; i++) for (unsigned j = 0; j< ret.m_n; j++) { diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h index e42f01ad7..87a79ec27 100644 --- a/src/math/lp/general_matrix.h +++ b/src/math/lp/general_matrix.h @@ -98,16 +98,16 @@ public: void clear() { m_data.clear(); } bool row_is_initialized_correctly(const vector& row) { - lp_assert(row.size() == column_count()); + SASSERT(row.size() == column_count()); for (unsigned j = 0; j < row.size(); j ++) - lp_assert(is_zero(row[j])); + SASSERT(is_zero(row[j])); return true; } template void init_row_from_container(int i, const T & c, std::function column_fix, const mpq& sign) { auto & row = m_data[adjust_row(i)]; - lp_assert(row_is_initialized_correctly(row)); + SASSERT(row_is_initialized_correctly(row)); for (lp::lar_term::ival p : c) { unsigned j = adjust_column(column_fix(p.j())); row[j] = sign * p.coeff(); @@ -115,7 +115,7 @@ public: } general_matrix operator*(const general_matrix & m) const { - lp_assert(m.row_count() == column_count()); + SASSERT(m.row_count() == column_count()); general_matrix ret(row_count(), m.column_count()); for (unsigned i = 0; i < row_count(); i ++) { for (unsigned j = 0; j < m.column_count(); j++) { @@ -158,7 +158,7 @@ public: vector operator*(const vector & x) const { vector r; - lp_assert(x.size() == column_count()); + SASSERT(x.size() == column_count()); for (unsigned i = 0; i < row_count(); i++) { mpq v(0); for (unsigned j = 0; j < column_count(); j++) { @@ -171,12 +171,12 @@ public: void transpose_rows(unsigned i, unsigned l) { - lp_assert(i != l); + SASSERT(i != l); m_row_permutation.transpose_from_right(i, l); } void transpose_columns(unsigned j, unsigned k) { - lp_assert(j != k); + SASSERT(j != k); m_column_permutation.transpose_from_left(j, k); } @@ -210,7 +210,7 @@ public: // used for debug only general_matrix take_first_n_columns(unsigned n) const { - lp_assert(n <= column_count()); + SASSERT(n <= column_count()); if (n == column_count()) return *this; general_matrix ret(row_count(), n); diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index c6f9a4123..d5db5093d 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -58,7 +58,7 @@ struct create_cut { } void int_case_in_gomory_cut(unsigned j) { - lp_assert(is_int(j) && m_fj.is_pos()); + SASSERT(is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", tout << " k = " << m_k; tout << ", fj: " << m_fj << ", "; @@ -68,15 +68,15 @@ struct create_cut { if (at_lower(j)) { // here we have the product of new_a*(xj - lb(j)), so new_a*lb(j) is added to m_k new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); - lp_assert(new_a.is_pos()); + SASSERT(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); push_explanation(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(j)); + SASSERT(at_upper(j)); // here we have the expression new_a*(xj - ub), so new_a*ub(j) is added to m_k new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); - lp_assert(new_a.is_neg()); + SASSERT(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); push_explanation(column_upper_bound_constraint(j)); } @@ -111,7 +111,7 @@ struct create_cut { push_explanation(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(j)); + SASSERT(at_upper(j)); if (a.is_pos()) { // the delta is works again m_f new_a = - a / m_f; @@ -134,7 +134,7 @@ struct create_cut { } lia_move report_conflict_from_gomory_cut() { - lp_assert(m_k.is_pos()); + SASSERT(m_k.is_pos()); // conflict 0 >= k where k is positive return lia_move::conflict; } @@ -204,7 +204,7 @@ struct create_cut { else if (at_lower(j)) dump_lower_bound_expl(out, j); else { - lp_assert(at_upper(j)); + SASSERT(at_upper(j)); dump_upper_bound_expl(out, j); } } @@ -259,7 +259,7 @@ public: m_found_big = false; TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f << "\n";); - lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); + SASSERT(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); auto set_polarity_for_int = [&](const mpq & a, lpvar j) { if (a.is_pos()) { if (at_lower(j)) diff --git a/src/math/lp/hnf.h b/src/math/lp/hnf.h index 75a69393f..d48c81f34 100644 --- a/src/math/lp/hnf.h +++ b/src/math/lp/hnf.h @@ -78,31 +78,31 @@ void extended_gcd_minimal_uv(const mpq & a, const mpq & b, mpq & d, mpq & u, mpq k -= one_of_type(); } - lp_assert(v == k * a_over_d + r); + SASSERT(v == k * a_over_d + r); if (is_pos(b)) { v = r - a_over_d; // v -= (k + 1) * a_over_d; - lp_assert(- a_over_d < v && v <= zero_of_type()); + SASSERT(- a_over_d < v && v <= zero_of_type()); if (is_pos(a)) { u += (k + 1) * (b / d); - lp_assert( one_of_type() <= u && u <= abs(b)/d); + SASSERT( one_of_type() <= u && u <= abs(b)/d); } else { u -= (k + 1) * (b / d); - lp_assert( one_of_type() <= -u && -u <= abs(b)/d); + SASSERT( one_of_type() <= -u && -u <= abs(b)/d); } } else { v = r; // v -= k * a_over_d; - lp_assert(- a_over_d < -v && -v <= zero_of_type()); + SASSERT(- a_over_d < -v && -v <= zero_of_type()); if (is_pos(a)) { u += k * (b / d); - lp_assert( one_of_type() <= u && u <= abs(b)/d); + SASSERT( one_of_type() <= u && u <= abs(b)/d); } else { u -= k * (b / d); - lp_assert( one_of_type() <= -u && -u <= abs(b)/d); + SASSERT( one_of_type() <= -u && -u <= abs(b)/d); } } - lp_assert(d == u * a + v * b); + SASSERT(d == u * a + v * b); } @@ -127,7 +127,7 @@ bool prepare_pivot_for_lower_triangle(M &m, unsigned r) { template void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & big_number) { - lp_assert(!is_zero(m[r][r])); + SASSERT(!is_zero(m[r][r])); for (unsigned j = r + 1; j < m.column_count(); j++) { for (unsigned i = r + 1; i < m.row_count(); i++) { if ( @@ -137,7 +137,7 @@ void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & overflow = true; return; } - lp_assert(is_integer(m[i][j])); + SASSERT(is_integer(m[i][j])); } } } @@ -154,7 +154,7 @@ unsigned to_lower_triangle_non_fractional(M &m, bool & overflow, const mpq& big_ if (overflow) return 0; } - lp_assert(i == m.row_count()); + SASSERT(i == m.row_count()); return i; } @@ -168,7 +168,7 @@ mpq gcd_of_row_starting_from_diagonal(const M& m, unsigned i) { if (!is_zero(t)) g = abs(t); } - lp_assert(!is_zero(g)); + SASSERT(!is_zero(g)); for (; j < m.column_count(); j++) { const auto & t = m[i][j]; if (!is_zero(t)) @@ -249,7 +249,7 @@ class hnf { } void buffer_p_col_i_plus_q_col_j_W_modulo(const mpq & p, const mpq & q) { - lp_assert(zeros_in_column_W_above(m_i)); + SASSERT(zeros_in_column_W_above(m_i)); for (unsigned k = m_i; k < m_m; k++) { m_buffer[k] = mod_R_balanced(mod_R_balanced(p * m_W[k][m_i]) + mod_R_balanced(q * m_W[k][m_j])); } @@ -262,7 +262,7 @@ class hnf { } void pivot_column_i_to_column_j_H(mpq u, unsigned i, mpq v, unsigned j) { - lp_assert(is_zero(u * m_H[i][i] + v * m_H[i][j])); + SASSERT(is_zero(u * m_H[i][i] + v * m_H[i][j])); m_H[i][j] = zero_of_type(); for (unsigned k = i + 1; k < m_m; k ++) m_H[k][j] = u * m_H[k][i] + v * m_H[k][j]; @@ -270,7 +270,7 @@ class hnf { } #endif void pivot_column_i_to_column_j_W_modulo(mpq u, mpq v) { - lp_assert(is_zero((u * m_W[m_i][m_i] + v * m_W[m_i][m_j]) % m_R)); + SASSERT(is_zero((u * m_W[m_i][m_i] + v * m_W[m_i][m_j]) % m_R)); m_W[m_i][m_j] = zero_of_type(); for (unsigned k = m_i + 1; k < m_m; k ++) m_W[k][m_j] = mod_R_balanced(mod_R_balanced(u * m_W[k][m_i]) + mod_R_balanced(v * m_W[k][m_j])); @@ -364,14 +364,14 @@ class hnf { } void replace_column_j_by_j_minus_u_col_i_H(unsigned i, unsigned j, const mpq & u) { - lp_assert(j < i); + SASSERT(j < i); for (unsigned k = i; k < m_m; k++) { m_H[k][j] -= u * m_H[k][i]; } } void replace_column_j_by_j_minus_u_col_i_U(unsigned i, unsigned j, const mpq & u) { - lp_assert(j < i); + SASSERT(j < i); for (unsigned k = 0; k < m_n; k++) { m_U[k][j] -= u * m_U[k][i]; } @@ -405,7 +405,7 @@ class hnf { process_row_column(i, j); } if (i >= m_n) { - lp_assert(m_H == m_A_orig * m_U); + SASSERT(m_H == m_A_orig * m_U); return; } if (is_neg(m_H[i][i])) @@ -427,7 +427,7 @@ class hnf { m_U_reverse = m_U; - lp_assert(m_H == m_A_orig * m_U); + SASSERT(m_H == m_A_orig * m_U); } bool row_is_correct_form(unsigned i) const { @@ -489,7 +489,7 @@ private: } void replace_column_j_by_j_minus_u_col_i_W(unsigned j, const mpq & u) { - lp_assert(j < m_i); + SASSERT(j < m_i); for (unsigned k = m_i; k < m_m; k++) { m_W[k][j] -= u * m_W[k][m_i]; // m_W[k][j] = mod_R_balanced(m_W[k][j]); @@ -546,7 +546,7 @@ private: if (is_zero(mii)) mii = d; - lp_assert(is_pos(mii)); + SASSERT(is_pos(mii)); // adjust column m_i for (unsigned k = m_i + 1; k < m_m; k++) { @@ -554,7 +554,7 @@ private: m_W[k][m_i] = mod_R_balanced(m_W[k][m_i]); } - lp_assert(is_pos(mii)); + SASSERT(is_pos(mii)); for (unsigned j = 0; j < m_i; j++) { const mpq & mij = m_W[m_i][j]; if (!is_pos(mij) && - mij < mii) @@ -575,9 +575,9 @@ private: void calculate_by_modulo() { for (m_i = 0; m_i < m_m; m_i ++) { process_row_modulo(); - lp_assert(is_pos(m_W[m_i][m_i])); + SASSERT(is_pos(m_W[m_i][m_i])); m_R /= m_W[m_i][m_i]; - lp_assert(is_integer(m_R)); + SASSERT(is_integer(m_R)); m_half_R = floor(m_R / 2); } } @@ -609,7 +609,7 @@ public: tout << "A = "; m_A_orig.print(tout, 4); tout << std::endl; tout << "H = "; m_H.print(tout, 4); tout << std::endl; tout << "W = "; m_W.print(tout, 4); tout << std::endl;); - lp_assert (m_H == m_W); + SASSERT (m_H == m_W); #endif } diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 192be557d..294467177 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -99,7 +99,7 @@ namespace lp { if (is_integer(b[i])) continue; if (n == 0) { - lp_assert(ret == -1); + SASSERT(ret == -1); n = 1; ret = i; } @@ -202,7 +202,7 @@ branch y_i >= ceil(y0_i) is impossible. hnf h(m_A, d); vector b = create_b(basis_rows); #ifdef Z3DEBUG - lp_assert(m_A * x0 == b); + SASSERT(m_A * x0 == b); #endif find_h_minus_1_b(h.W(), b); @@ -274,7 +274,7 @@ branch y_i >= ceil(y0_i) is impossible. for (auto ci : lra.flatten(dep)) lra.constraints().display(tout, ci); ); - lp_assert(lia.current_solution_is_inf_on_cut()); + SASSERT(lia.current_solution_is_inf_on_cut()); lia.settings().stats().m_hnf_cuts++; lia.expl()->clear(); for (u_dependency* dep : constraints_for_explanation()) diff --git a/src/math/lp/incremental_vector.h b/src/math/lp/incremental_vector.h index 0bb2829eb..50a0a6f96 100644 --- a/src/math/lp/incremental_vector.h +++ b/src/math/lp/incremental_vector.h @@ -43,7 +43,7 @@ public: template void pop_tail(vector & v, unsigned k) { - lp_assert(v.size() >= k); + SASSERT(v.size() >= k); v.shrink(v.size() - k); } @@ -53,8 +53,8 @@ public: } void pop_scope(unsigned k) { - lp_assert(m_stack_of_vector_sizes.size() >= k); - lp_assert(k > 0); + SASSERT(m_stack_of_vector_sizes.size() >= k); + SASSERT(k > 0); m_vector.shrink(peek_size(k)); unsigned new_st_size = m_stack_of_vector_sizes.size() - k; m_stack_of_vector_sizes.shrink(new_st_size); @@ -65,7 +65,7 @@ public: } unsigned peek_size(unsigned k) const { - lp_assert(k > 0 && k <= m_stack_of_vector_sizes.size()); + SASSERT(k > 0 && k <= m_stack_of_vector_sizes.size()); return m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]; } }; diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h index 1bb05ce84..724a08c28 100644 --- a/src/math/lp/indexed_vector_def.h +++ b/src/math/lp/indexed_vector_def.h @@ -39,7 +39,7 @@ void indexed_vector::resize(unsigned data_size) { template void indexed_vector::set_value(const T& value, unsigned index) { m_data[index] = value; - lp_assert(std::find(m_index.begin(), m_index.end(), index) == m_index.end()); + SASSERT(std::find(m_index.begin(), m_index.end(), index) == m_index.end()); m_index.push_back(index); } diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 3e3b9e555..a5ce3c291 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -33,7 +33,7 @@ lia_move int_branch::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); lia.get_term().clear(); - lp_assert(j != -1); + SASSERT(j != -1); lia.get_term().add_monomial(mpq(1), j); if (lia.is_free(j)) { lia.is_upper() = lia.settings().random_next() % 2; diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index c8488ca37..fc9d5678b 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -50,7 +50,7 @@ namespace lp { lra.pop(); lra.round_to_integer_solution(); lra.set_status(lp_status::FEASIBLE); - lp_assert(lia.settings().get_cancel_flag() || lia.is_feasible()); + SASSERT(lia.settings().get_cancel_flag() || lia.is_feasible()); TRACE("cube", tout << "success";); lia.settings().stats().m_cube_success++; return lia_move::sat; @@ -78,7 +78,7 @@ namespace lp { void int_cube::find_feasible_solution() { lra.find_feasible_solution(); - lp_assert(lp_status::OPTIMAL == lra.get_status() || lp_status::FEASIBLE == lra.get_status()); + SASSERT(lp_status::OPTIMAL == lra.get_status() || lp_status::FEASIBLE == lra.get_status()); } impq int_cube::get_cube_delta_for_term(const lar_term& t) const { diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 11648f7bd..4bc9b2fb3 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -113,7 +113,7 @@ namespace lp { } // if bj == v, then, because we are patching the lra.get_value(v), // we just need to assert that the lra.get_value(v) would be integral. - lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int()); + SASSERT(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int()); } lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta)); @@ -142,8 +142,8 @@ namespace lp { return false; mpq a = fractional_part(c.coeff()); mpq r = fractional_part(lra.get_value(v)); - lp_assert(0 < r && r < 1); - lp_assert(0 < a && a < 1); + SASSERT(0 < r && r < 1); + SASSERT(0 < a && a < 1); mpq delta_plus, delta_minus; if (!get_patching_deltas(r, a, delta_plus, delta_minus)) return false; @@ -159,7 +159,7 @@ namespace lp { lia_move patch_basic_columns() { lia.settings().stats().m_patches++; lra.remove_fixed_vars_from_base(); - lp_assert(lia.is_feasible()); + SASSERT(lia.is_feasible()); for (unsigned j : lra.r_basis()) if (!lra.get_value(j).is_int() && lra.column_is_int(j) && !lia.is_fixed(j)) patch_basic_column(j); @@ -405,16 +405,16 @@ namespace lp { // coprime. We can find u and v such that u*a1 + v*x2 = 1. rational u, v; gcd(a1, x2, u, v); - lp_assert(gcd(a1, x2, u, v).is_one()); - lp_assert((x + (a1 / a2) * (-u * t) * x1).is_int()); + SASSERT(gcd(a1, x2, u, v).is_one()); + SASSERT((x + (a1 / a2) * (-u * t) * x1).is_int()); // 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l. rational d = u * t * x1; // We can prove that x+alpha*d is integral, // and any other delta, satisfying x+alpha*delta, is equal to d modulo a2. delta_plus = mod(d, a2); - lp_assert(delta_plus > 0); + SASSERT(delta_plus > 0); delta_minus = delta_plus - a2; - lp_assert(delta_minus < 0); + SASSERT(delta_minus < 0); return true; } @@ -551,7 +551,7 @@ namespace lp { const mpq & a = c.coeff(); unsigned i = lrac.m_r_basis[row_index]; impq const & xi = get_value(i); - lp_assert(lrac.m_r_solver.column_is_feasible(i)); + SASSERT(lrac.m_r_solver.column_is_feasible(i)); if (column_is_int(i) && !a.is_int() && xi.is_int()) m = lcm(m, denominator(a)); @@ -591,7 +591,7 @@ namespace lp { bool int_solver::is_feasible() const { - lp_assert( + SASSERT( lrac.m_r_solver.calc_current_x_is_feasible_include_non_basis() == lrac.m_r_solver.current_x_is_feasible()); return lrac.m_r_solver.current_x_is_feasible(); diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 8e727bce9..b0252b624 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -117,8 +117,8 @@ public: void fill_not_improvable_zero_sum(); void push() { - lp_assert(m_r_solver.basis_heading_is_correct()); - lp_assert(m_column_types.size() == m_r_A.column_count()); + SASSERT(m_r_solver.basis_heading_is_correct()); + SASSERT(m_column_types.size() == m_r_A.column_count()); m_stacked_simplex_strategy = settings().simplex_strategy(); m_stacked_simplex_strategy.push(); m_column_types.push(); @@ -140,20 +140,20 @@ public: m_stacked_simplex_strategy.pop(k); m_r_solver.m_settings.simplex_strategy() = m_stacked_simplex_strategy; m_infeasible_linear_combination.reset(); - lp_assert(m_r_solver.basis_heading_is_correct()); + SASSERT(m_r_solver.basis_heading_is_correct()); } bool r_basis_is_OK() const { #ifdef Z3DEBUG for (unsigned j : m_r_solver.m_basis) { - lp_assert(m_r_solver.m_A.m_columns[j].size() == 1); + SASSERT(m_r_solver.m_A.m_columns[j].size() == 1); } for (unsigned j =0; j < m_r_solver.m_basis_heading.size(); j++) { if (m_r_solver.m_basis_heading[j] >= 0) continue; if (m_r_solver.m_column_types[j] == column_type::fixed) continue; - lp_assert(static_cast(- m_r_solver.m_basis_heading[j] - 1) < m_r_solver.m_column_types.size()); - lp_assert( m_r_solver.m_basis_heading[j] <= -1); + SASSERT(static_cast(- m_r_solver.m_basis_heading[j] - 1) < m_r_solver.m_column_types.size()); + SASSERT( m_r_solver.m_basis_heading[j] <= -1); } #endif return true; @@ -191,14 +191,14 @@ public: } void update_delta(mpq& delta, numeric_pair const& l, numeric_pair const& u) const { - lp_assert(l <= u); + SASSERT(l <= u); if (l.x < u.x && l.y > u.y) { mpq delta1 = (u.x - l.x) / (l.y - u.y); if (delta1 < delta) { delta = delta1; } } - lp_assert(l.x + delta * l.y <= u.x + delta * u.y); + SASSERT(l.x + delta * l.y <= u.x + delta * u.y); } @@ -234,14 +234,14 @@ public: const impq & lower_bound(unsigned j) const { - lp_assert(m_column_types()[j] == column_type::fixed || + SASSERT(m_column_types()[j] == column_type::fixed || m_column_types()[j] == column_type::boxed || m_column_types()[j] == column_type::lower_bound); return m_r_lower_bounds[j]; } const impq & upper_bound(unsigned j) const { - lp_assert(m_column_types()[j] == column_type::fixed || + SASSERT(m_column_types()[j] == column_type::fixed || m_column_types()[j] == column_type::boxed || m_column_types()[j] == column_type::upper_bound); return m_r_upper_bounds[j]; diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 8fc98db1d..5dbd32cb5 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -84,8 +84,8 @@ unsigned lar_core_solver::get_number_of_non_ints() const { void lar_core_solver::solve() { TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";); - lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); - lp_assert(m_r_solver.inf_heap_is_correct()); + SASSERT(m_r_solver.non_basic_columns_are_set_correctly()); + SASSERT(m_r_solver.inf_heap_is_correct()); TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.inf_heap_size() << ", int_infs = " << get_number_of_non_ints() << std::endl;); if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) { m_r_solver.set_status(lp_status::OPTIMAL); @@ -93,14 +93,14 @@ void lar_core_solver::solve() { return; } ++m_r_solver.m_settings.stats().m_need_to_solve_inf; - lp_assert( r_basis_is_OK()); + SASSERT( r_basis_is_OK()); if (m_r_solver.m_look_for_feasible_solution_only) //todo : should it be set? m_r_solver.find_feasible_solution(); else m_r_solver.solve(); - lp_assert(r_basis_is_OK()); + SASSERT(r_basis_is_OK()); switch (m_r_solver.get_status()) { @@ -114,9 +114,9 @@ void lar_core_solver::solve() { m_r_solver.set_status(lp_status::OPTIMAL); break; } - lp_assert(r_basis_is_OK()); - lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); - lp_assert(m_r_solver.inf_heap_is_correct()); + SASSERT(r_basis_is_OK()); + SASSERT(m_r_solver.non_basic_columns_are_set_correctly()); + SASSERT(m_r_solver.inf_heap_is_correct()); TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index df5cf9524..767b5b4a1 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -43,9 +43,9 @@ namespace lp { } bool lar_solver::sizes_are_correct() const { - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); return true; } @@ -90,7 +90,7 @@ namespace lp { else if (kind == LE || kind == LT) n_of_L++; rs_of_evidence += coeff * constr.rhs(); } - lp_assert(n_of_G == 0 || n_of_L == 0); + SASSERT(n_of_G == 0 || n_of_L == 0); lconstraint_kind kind = n_of_G ? GE : (n_of_L ? LE : EQ); if (strict) kind = static_cast((static_cast(kind) / 2)); @@ -221,10 +221,10 @@ namespace lp { unsigned n = m_columns.size(); m_var_register.shrink(n); - 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()); - lp_assert(A_r().column_count() == n); + SASSERT(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); + SASSERT(A_r().column_count() == n); TRACE("lar_solver_details", for (unsigned j = 0; j < n; j++) print_column_info(j, tout) << "\n";); m_mpq_lar_core_solver.pop(k); @@ -242,8 +242,8 @@ namespace lp { m_constraints.pop(k); m_simplex_strategy.pop(k); m_settings.simplex_strategy() = m_simplex_strategy; - lp_assert(sizes_are_correct()); - lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + SASSERT(sizes_are_correct()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); m_usage_in_terms.pop(k); m_dependencies.pop_scope(k); // init the nbasis sorting @@ -351,13 +351,13 @@ namespace lp { bool lar_solver::costs_are_zeros_for_r_solver() const { for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_costs.size(); j++) { - lp_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_costs[j])); + SASSERT(is_zero(m_mpq_lar_core_solver.m_r_solver.m_costs[j])); } return true; } bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const { for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_d.size(); j++) { - lp_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_d[j])); + SASSERT(is_zero(m_mpq_lar_core_solver.m_r_solver.m_d[j])); } return true; } @@ -377,15 +377,15 @@ namespace lp { d[rc.var()] = zero_of_type(); } - lp_assert(reduced_costs_are_zeroes_for_r_solver()); - lp_assert(costs_are_zeros_for_r_solver()); + SASSERT(reduced_costs_are_zeroes_for_r_solver()); + SASSERT(costs_are_zeros_for_r_solver()); } void lar_solver::prepare_costs_for_r_solver(const lar_term& term) { TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); auto& rslv = m_mpq_lar_core_solver.m_r_solver; - lp_assert(costs_are_zeros_for_r_solver()); - lp_assert(reduced_costs_are_zeroes_for_r_solver()); + SASSERT(costs_are_zeros_for_r_solver()); + SASSERT(reduced_costs_are_zeroes_for_r_solver()); move_non_basic_columns_to_bounds(); rslv.m_costs.resize(A_r().column_count(), zero_of_type()); for (lar_term::ival p : term) { @@ -398,7 +398,7 @@ namespace lp { } if (settings().backup_costs) rslv.m_costs_backup = rslv.m_costs; - lp_assert(rslv.reduced_costs_are_correct_tableau()); + SASSERT(rslv.reduced_costs_are_correct_tableau()); } void lar_solver::move_non_basic_columns_to_bounds() { @@ -457,7 +457,7 @@ namespace lp { } void lar_solver::set_value_for_nbasic_column(unsigned j, const impq& new_val) { - lp_assert(!is_base(j)); + SASSERT(!is_base(j)); auto& x = m_mpq_lar_core_solver.r_x(j); auto delta = new_val - x; x = new_val; @@ -493,7 +493,7 @@ namespace lp { // returns true iff the row of j has a non-fixed column different from j bool lar_solver::remove_from_basis(unsigned j) { - lp_assert(is_base(j)); + SASSERT(is_base(j)); unsigned i = row_of_basic_column(j); for (const auto & c : A_r().m_rows[i]) if (j != c.var() && !column_is_fixed(c.var())) @@ -783,14 +783,14 @@ namespace lp { continue; } - lp_assert(is_base(j) && column_is_fixed(j)); + SASSERT(is_base(j) && column_is_fixed(j)); auto const& r = basic2row(j); for (auto const& c : r) { unsigned j_entering = c.var(); if (!column_is_fixed(j_entering)) { pivot(j_entering, j); to_remove.push_back(j); - lp_assert(is_base(j_entering)); + SASSERT(is_base(j_entering)); break; } } @@ -798,7 +798,7 @@ namespace lp { for (unsigned j : to_remove) { m_fixed_base_var_set.remove(j); } - lp_assert(fixed_base_removed_correctly()); + SASSERT(fixed_base_removed_correctly()); } #ifdef Z3DEBUG bool lar_solver::fixed_base_removed_correctly() const { @@ -912,7 +912,7 @@ namespace lp { update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); m_mpq_lar_core_solver.solve(); set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lp_assert(((stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); + SASSERT(((stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); } @@ -1006,7 +1006,7 @@ namespace lp { bool lar_solver::the_left_sides_sum_to_zero(const vector>& evidence) const { std::unordered_map coeff_map; for (auto const & [coeff, con_ind] : evidence) { - lp_assert(m_constraints.valid_index(con_ind)); + SASSERT(m_constraints.valid_index(con_ind)); register_in_map(coeff_map, m_constraints[con_ind], coeff); } @@ -1024,18 +1024,18 @@ namespace lp { // disabled: kind is uninitialized #ifdef Z3DEBUG lconstraint_kind kind; - lp_assert(the_left_sides_sum_to_zero(explanation)); + SASSERT(the_left_sides_sum_to_zero(explanation)); mpq rs = sum_of_right_sides_of_explanation(explanation); switch (kind) { - case LE: lp_assert(rs < zero_of_type()); + case LE: SASSERT(rs < zero_of_type()); break; - case LT: lp_assert(rs <= zero_of_type()); + case LT: SASSERT(rs <= zero_of_type()); break; - case GE: lp_assert(rs > zero_of_type()); + case GE: SASSERT(rs > zero_of_type()); break; - case GT: lp_assert(rs >= zero_of_type()); + case GT: SASSERT(rs >= zero_of_type()); break; - case EQ: lp_assert(rs != zero_of_type()); + case EQ: SASSERT(rs != zero_of_type()); break; default: UNREACHABLE(); @@ -1060,7 +1060,7 @@ namespace lp { for (auto it : exp) { mpq coeff = it.coeff(); constraint_index con_ind = it.ci(); - lp_assert(m_constraints.valid_index(con_ind)); + SASSERT(m_constraints.valid_index(con_ind)); ret += (m_constraints[con_ind].rhs() - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff; } return ret; @@ -1142,7 +1142,7 @@ namespace lp { int inf_sign; auto inf_row = m_mpq_lar_core_solver.get_infeasibility_info(inf_sign); get_infeasibility_explanation_for_inf_sign(exp, inf_row, inf_sign); - lp_assert(explanation_is_correct(exp)); + SASSERT(explanation_is_correct(exp)); } void lar_solver::get_infeasibility_explanation_for_inf_sign( @@ -1161,7 +1161,7 @@ namespace lp { svector deps; m_dependencies.linearize(bound_constr_i, deps); for (auto d : deps) { - lp_assert(m_constraints.valid_index(d)); + SASSERT(m_constraints.valid_index(d)); exp.add_pair(d, coeff); } } @@ -1184,9 +1184,10 @@ namespace lp { bool lar_solver::init_model() const { auto& rslv = m_mpq_lar_core_solver.m_r_solver; - lp_assert(A_r().column_count() == rslv.m_costs.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); - lp_assert(A_r().column_count() == rslv.m_d.size()); + (void)rslv; + SASSERT(A_r().column_count() == rslv.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); + SASSERT(A_r().column_count() == rslv.m_d.size()); CTRACE("lar_solver_model",!m_columns_with_changed_bounds.empty(), tout << "non-empty changed bounds\n"); TRACE("lar_solver_model", tout << get_status() << "\n"); auto status = get_status(); @@ -1331,7 +1332,7 @@ namespace lp { for (auto& it : cns.coeffs()) { lpvar j = it.second; auto vi = var_map.find(j); - lp_assert(vi != var_map.end()); + SASSERT(vi != var_map.end()); ret += it.first * vi->second; } return ret; @@ -1376,7 +1377,7 @@ namespace lp { void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) { // i, j - is the indices of the bottom-right element of the tableau - lp_assert(A_r().row_count() == i + 1 && A_r().column_count() == j + 1); + SASSERT(A_r().row_count() == i + 1 && A_r().column_count() == j + 1); auto& last_column = A_r().m_columns[j]; int non_zero_column_cell_index = -1; for (unsigned k = static_cast(last_column.size()); k-- > 0;) { @@ -1386,13 +1387,13 @@ namespace lp { non_zero_column_cell_index = k; } - lp_assert(non_zero_column_cell_index != -1); - lp_assert(static_cast(non_zero_column_cell_index) != i); + SASSERT(non_zero_column_cell_index != -1); + SASSERT(static_cast(non_zero_column_cell_index) != i); m_mpq_lar_core_solver.m_r_solver.transpose_rows_tableau(last_column[non_zero_column_cell_index].var(), i); } void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) { - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); auto& slv = m_mpq_lar_core_solver.m_r_solver; unsigned i = A_r().row_count() - 1; //last row index make_sure_that_the_bottom_right_elem_not_zero_in_tableau(i, j); @@ -1410,8 +1411,8 @@ namespace lp { } A_r().remove_element(last_row, rc); } - lp_assert(last_row.size() == 0); - lp_assert(A_r().m_columns[j].size() == 0); + SASSERT(last_row.size() == 0); + SASSERT(A_r().m_columns[j].size() == 0); A_r().m_rows.pop_back(); A_r().m_columns.pop_back(); CASSERT("check_static_matrix", A_r().is_correct()); @@ -1419,7 +1420,7 @@ namespace lp { void lar_solver::remove_last_column_from_A() { // the last column has to be empty - lp_assert(A_r().m_columns.back().size() == 0); + SASSERT(A_r().m_columns.back().size() == 0); A_r().m_columns.pop_back(); } @@ -1428,7 +1429,7 @@ namespace lp { int i = rslv.m_basis_heading[j]; if (i >= 0) { // j is a basic var int last_pos = static_cast(rslv.m_basis.size()) - 1; - lp_assert(last_pos >= 0); + SASSERT(last_pos >= 0); if (i != last_pos) { unsigned j_at_last_pos = rslv.m_basis[last_pos]; rslv.m_basis[i] = j_at_last_pos; @@ -1438,7 +1439,7 @@ namespace lp { } else { int last_pos = static_cast(rslv.m_nbasis.size()) - 1; - lp_assert(last_pos >= 0); + SASSERT(last_pos >= 0); i = -1 - i; if (i != last_pos) { unsigned j_at_last_pos = rslv.m_nbasis[last_pos]; @@ -1448,14 +1449,14 @@ namespace lp { rslv.m_nbasis.pop_back(); // remove j from the basis } rslv.m_basis_heading.pop_back(); - lp_assert(rslv.m_basis.size() == A_r().row_count()); - lp_assert(rslv.basis_heading_is_correct()); + SASSERT(rslv.m_basis.size() == A_r().row_count()); + SASSERT(rslv.basis_heading_is_correct()); } void lar_solver::remove_last_column_from_tableau() { auto& rslv = m_mpq_lar_core_solver.m_r_solver; unsigned j = A_r().column_count() - 1; - lp_assert(A_r().column_count() == rslv.m_costs.size()); + SASSERT(A_r().column_count() == rslv.m_costs.size()); if (column_represents_row_in_tableau(j)) { remove_last_row_and_column_from_tableau(j); if (rslv.m_basis_heading[j] < 0) @@ -1469,10 +1470,10 @@ namespace lp { rslv.m_costs.pop_back(); remove_last_column_from_basis_tableau(j); - lp_assert(m_mpq_lar_core_solver.r_basis_is_OK()); - lp_assert(A_r().column_count() == rslv.m_costs.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); - lp_assert(A_r().column_count() == rslv.m_d.size()); + SASSERT(m_mpq_lar_core_solver.r_basis_is_OK()); + SASSERT(A_r().column_count() == rslv.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); + SASSERT(A_r().column_count() == rslv.m_d.size()); } @@ -1496,14 +1497,14 @@ namespace lp { } for (unsigned j : became_feas) { - lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); + SASSERT(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); m_mpq_lar_core_solver.m_r_solver.m_d[j] -= m_mpq_lar_core_solver.m_r_solver.m_costs[j]; m_mpq_lar_core_solver.m_r_solver.m_costs[j] = zero_of_type(); m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_heap(j); } became_feas.clear(); for (unsigned j : m_mpq_lar_core_solver.m_r_solver.inf_heap()) { - lp_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0); + SASSERT(m_mpq_lar_core_solver.m_r_heading[j] >= 0); if (column_is_feasible(j)) became_feas.push_back(j); } @@ -1586,14 +1587,14 @@ namespace lp { lpvar local_j; if (m_var_register.external_is_used(ext_j, local_j)) return local_j; - lp_assert(m_columns.size() == A_r().column_count()); + SASSERT(m_columns.size() == A_r().column_count()); local_j = A_r().column_count(); m_columns.push_back(column()); m_trail.push(undo_add_column(*this)); while (m_usage_in_terms.size() <= local_j) m_usage_in_terms.push_back(0); add_non_basic_var_to_core_fields(ext_j, is_int); - lp_assert(sizes_are_correct()); + SASSERT(sizes_are_correct()); return local_j; } @@ -1602,7 +1603,7 @@ namespace lp { } void lar_solver::register_new_external_var(unsigned ext_v, bool is_int) { - lp_assert(!m_var_register.external_is_used(ext_v)); + SASSERT(!m_var_register.external_is_used(ext_v)); m_var_register.add_var(ext_v, is_int); } @@ -1620,8 +1621,8 @@ namespace lp { unsigned j = A_r().column_count(); TRACE("add_var", tout << "j = " << j << std::endl;); A_r().add_column(); - lp_assert(m_mpq_lar_core_solver.r_x().size() == j); - // lp_assert(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later + SASSERT(m_mpq_lar_core_solver.r_x().size() == j); + // SASSERT(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later m_mpq_lar_core_solver.resize_x(j + 1); auto& rslv = m_mpq_lar_core_solver.m_r_solver; m_mpq_lar_core_solver.m_r_lower_bounds.increase_size_by_one(); @@ -1629,7 +1630,7 @@ namespace lp { rslv.inf_heap_increase_size_by_one(); rslv.m_costs.resize(j + 1); rslv.m_d.resize(j + 1); - lp_assert(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method + SASSERT(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method if (register_in_basis) { A_r().add_row(); m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); @@ -1704,7 +1705,7 @@ namespace lp { lpvar ret = A_r().column_count(); add_row_from_term_no_constraint(t, ext_i); - lp_assert(m_var_register.size() == A_r().column_count()); + SASSERT(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) register_normalized_term(*t, A_r().column_count() - 1); if (m_add_term_callback) @@ -1850,13 +1851,13 @@ namespace lp { constraint_index ci; if (!column_has_term(j)) { mpq rs = adjust_bound_for_int(j, kind, right_side); - lp_assert(bound_is_integer_for_integer_column(j, rs)); + SASSERT(bound_is_integer_for_integer_column(j, rs)); ci = m_constraints.add_var_constraint(j, kind, rs); } else { ci = add_var_bound_on_constraint_for_term(j, kind, right_side); } - lp_assert(sizes_are_correct()); + SASSERT(sizes_are_correct()); return ci; } @@ -2061,8 +2062,8 @@ namespace lp { } void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j)); - lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || + SASSERT(column_has_lower_bound(j) && column_has_upper_bound(j)); + SASSERT(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed); mpq y_of_bound(0); @@ -2129,8 +2130,8 @@ namespace lp { } void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j)); - lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); + SASSERT(column_has_lower_bound(j) && !column_has_upper_bound(j)); + SASSERT(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); mpq y_of_bound(0); switch (kind) { @@ -2183,8 +2184,8 @@ namespace lp { } void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j)); - lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); + SASSERT(!column_has_lower_bound(j) && column_has_upper_bound(j)); + SASSERT(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); mpq y_of_bound(0); switch (kind) { case LT: @@ -2238,7 +2239,7 @@ namespace lp { } void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j)); + SASSERT(!column_has_lower_bound(j) && !column_has_upper_bound(j)); mpq y_of_bound(0); switch (kind) { @@ -2388,7 +2389,7 @@ namespace lp { } bool lar_solver::get_equality_and_right_side_for_term_on_current_x(lpvar j, mpq& rs, u_dependency*& ci, bool& upper_bound) const { - lp_assert(column_has_term(j)); + SASSERT(column_has_term(j)); if (!column_is_int(j)) // todo - allow for the next version of hnf return false; bool rs_is_calculated = false; @@ -2396,7 +2397,7 @@ namespace lp { bool is_strict; const lar_term& term = get_term(j); if (has_upper_bound(j, ci, b, is_strict) && !is_strict) { - lp_assert(b.is_int()); + SASSERT(b.is_int()); if (!sum_first_coords(term, rs)) return false; rs_is_calculated = true; @@ -2410,7 +2411,7 @@ namespace lp { if (!sum_first_coords(term, rs)) return false; } - lp_assert(b.is_int()); + SASSERT(b.is_int()); if (rs == b) { upper_bound = false; @@ -2471,7 +2472,7 @@ namespace lp { // a_j.second givis the column bool lar_solver::fetch_normalized_term_column(const lar_term& c, std::pair& a_j) const { TRACE("lar_solver_terms", print_term_as_indices(c, tout << "looking for term ") << "\n";); - lp_assert(c.is_normalized()); + SASSERT(c.is_normalized()); auto it = m_normalized_terms_to_columns.find(c); if (it != m_normalized_terms_to_columns.end()) { TRACE("lar_solver_terms", tout << "got " << it->second << "\n";); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 575184b4f..889476331 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -335,7 +335,7 @@ public: int sign = j_sign * a_sign; const column& ul = m_columns[j]; auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); - lp_assert(witness); + SASSERT(witness); for (auto ci : flatten(witness)) bp.consume(a, ci); } @@ -453,7 +453,7 @@ public: void set_value_for_nbasic_column_report(unsigned j, const impq& new_val, const ChangeReport& after) { - lp_assert(!is_base(j)); + SASSERT(!is_base(j)); auto& x = m_mpq_lar_core_solver.r_x(j); auto delta = new_val - x; x = new_val; diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 9da65db04..bfd728fc7 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -81,11 +81,11 @@ private: if (v1 == v2) return; #if Z3DEBUG - lp_assert(val(v1) == val(v2)); + SASSERT(val(v1) == val(v2)); unsigned debv1, debv2; - lp_assert(only_one_nfixed(r1, debv1) && only_one_nfixed(r2, debv2)); - lp_assert(debv1 == v1 && debv2 == v2); - lp_assert(ival(v1).y == ival(v2).y); + SASSERT(only_one_nfixed(r1, debv1) && only_one_nfixed(r2, debv2)); + SASSERT(debv1 == v1 && debv2 == v2); + SASSERT(ival(v1).y == ival(v2).y); #endif explanation ex; explain_fixed_in_row(r1, ex); @@ -214,8 +214,8 @@ public: } bool add_eq_on_columns(const explanation& exp, lpvar je, lpvar ke, bool is_fixed) { - lp_assert(je != ke && is_int(je) == is_int(ke)); - lp_assert(ival(je) == ival(ke)); + SASSERT(je != ke && is_int(je) == is_int(ke)); + SASSERT(ival(je) == ival(ke)); TRACE("eq", tout << "reported idx " << je << ", " << ke << "\n"; @@ -315,7 +315,7 @@ public: continue; if (++nf > 2) return nf; - lp_assert(is_not_set(y)); + SASSERT(is_not_set(y)); y = j; if (c.coeff().is_one()) { y_sign = 1; @@ -332,8 +332,8 @@ public: } void try_add_equation_with_lp_fixed_tables(unsigned row_index, unsigned v_j) { - lp_assert(lp().get_base_column_in_row(row_index) == v_j); - lp_assert(num_of_non_fixed_in_row(row_index) == 1 || column_is_fixed(v_j)); + SASSERT(lp().get_base_column_in_row(row_index) == v_j); + SASSERT(num_of_non_fixed_in_row(row_index) == 1 || column_is_fixed(v_j)); if (column_is_fixed(v_j)) { return; } @@ -366,7 +366,7 @@ public: if (nf == 0 || nf > 2) return; if (nf == 1) { - lp_assert(is_not_set(y)); + SASSERT(is_not_set(y)); try_add_equation_with_lp_fixed_tables(row_index, x); return; } @@ -374,8 +374,8 @@ public: // the coefficient before y is not 1 or -1 return; } - lp_assert(y_sign == -1 || y_sign == 1); - lp_assert(lp().is_base(y) == false); + SASSERT(y_sign == -1 || y_sign == 1); + SASSERT(lp().is_base(y) == false); auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg; table.insert(val(x), row_index); TRACE("eq", tout << "y = " << y << "\n";); @@ -391,8 +391,8 @@ public: if (nf != 2 || y_sign == 0) continue; - lp_assert(y_nb == y); - lp_assert(y_sign == 1 || y_sign == -1); + SASSERT(y_nb == y); + SASSERT(y_sign == 1 || y_sign == -1); auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg; const auto& v = val(x); unsigned found_i;; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 67f7ffb6c..1656545ea 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -38,7 +38,7 @@ struct lpvar_lt { typedef heap lpvar_heap; template X dot_product(const vector & a, const vector & b) { - lp_assert(a.size() == b.size()); + SASSERT(a.size() == b.size()); auto r = zero_of_type(); for (unsigned i = 0; i < a.size(); i++) { r += a[i] * b[i]; @@ -180,7 +180,7 @@ public: unsigned m = m_A.row_count(); for (unsigned i = 0; i < m; i++) { unsigned bj = m_basis[i]; - lp_assert(m_A.m_columns[bj].size() > 0); + SASSERT(m_A.m_columns[bj].size() > 0); if (m_A.m_columns[bj].size() > 1) return true; for (const auto & c : m_A.m_columns[bj]) { @@ -293,11 +293,11 @@ public: bool make_column_feasible(unsigned j, numeric_pair & delta) { bool ret = false; - lp_assert(m_basis_heading[j] < 0); + SASSERT(m_basis_heading[j] < 0); const auto & x = m_x[j]; switch (m_column_types[j]) { case column_type::fixed: - lp_assert(m_lower_bounds[j] == m_upper_bounds[j]); + SASSERT(m_lower_bounds[j] == m_upper_bounds[j]); if (x != m_lower_bounds[j]) { delta = m_lower_bounds[j] - x; ret = true; @@ -365,7 +365,7 @@ public: void change_basis_unconditionally(unsigned entering, unsigned leaving) { TRACE("lar_solver", tout << "entering = " << entering << ", leaving = " << leaving << "\n";); - lp_assert(m_basis_heading[entering] < 0); + SASSERT(m_basis_heading[entering] < 0); int place_in_non_basis = -1 - m_basis_heading[entering]; if (static_cast(place_in_non_basis) >= m_nbasis.size()) { // entering variable in not in m_nbasis, we need to put it back; @@ -385,8 +385,8 @@ public: void change_basis(unsigned entering, unsigned leaving) { TRACE("lar_solver", tout << "entering = " << entering << ", leaving = " << leaving << "\n";); - lp_assert(m_basis_heading[entering] < 0); - lp_assert(m_basis_heading[leaving] >= 0); + SASSERT(m_basis_heading[entering] < 0); + SASSERT(m_basis_heading[leaving] >= 0); int place_in_basis = m_basis_heading[leaving]; int place_in_non_basis = - m_basis_heading[entering] - 1; @@ -573,14 +573,14 @@ public: m_inf_heap.insert(j); TRACE("lar_solver_inf_heap", tout << "insert into inf_heap j = " << j << "\n";); } - lp_assert(!column_is_feasible(j)); + SASSERT(!column_is_feasible(j)); } void remove_column_from_inf_heap(unsigned j) { if (m_inf_heap.contains(j)) { TRACE("lar_solver_inf_heap", tout << "erase from heap j = " << j << "\n";); m_inf_heap.erase(j); } - lp_assert(column_is_feasible(j)); + SASSERT(column_is_feasible(j)); } void clear_inf_heap() { @@ -589,10 +589,10 @@ public: } bool costs_on_nbasis_are_zeros() const { - lp_assert(this->basis_heading_is_correct()); + SASSERT(this->basis_heading_is_correct()); for (unsigned j = 0; j < this->m_n(); j++) { if (this->m_basis_heading[j] < 0) - lp_assert(is_zero(this->m_costs[j])); + SASSERT(is_zero(this->m_costs[j])); } return true; } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 4c0e8fc3e..82afd7a27 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -60,7 +60,7 @@ lp_core_solver_base(static_matrix & A, m_tracing_basis_changes(false), m_touched_rows(nullptr), m_look_for_feasible_solution_only(false) { - lp_assert(bounds_for_boxed_are_set_correctly()); + SASSERT(bounds_for_boxed_are_set_correctly()); init(); init_basis_heading_and_non_basic_columns_vector(); } @@ -68,7 +68,7 @@ lp_core_solver_base(static_matrix & A, template void lp_core_solver_base:: allocate_basis_heading() { // the rest of initialization will be handled by the factorization class init_basis_heading_and_non_basic_columns_vector(); - lp_assert(basis_heading_is_correct()); + SASSERT(basis_heading_is_correct()); } template void lp_core_solver_base:: init() { @@ -267,7 +267,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { return false; if (pivot_col_cell_index != 0) { - lp_assert(column.size() > 1); + SASSERT(column.size() > 1); // swap the pivot column cell with the head cell auto c = column[0]; column[0] = column[pivot_col_cell_index]; @@ -278,7 +278,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { } while (column.size() > 1) { auto & c = column.back(); - lp_assert(c.var() != piv_row_index); + SASSERT(c.var() != piv_row_index); if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) { return false; } @@ -324,7 +324,7 @@ non_basis_is_correctly_represented_in_heading(std::list* non_basis_lis for (unsigned j = 0; j < m_A.column_count(); j++) if (m_basis_heading[j] >= 0) - lp_assert(static_cast(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j); + SASSERT(static_cast(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j); if (non_basis_list == nullptr) return true; @@ -361,9 +361,9 @@ template bool lp_core_solver_base:: if ( m_A.column_count() > 10 ) // for the performance reason return true; - lp_assert(m_basis_heading.size() == m_A.column_count()); - lp_assert(m_basis.size() == m_A.row_count()); - lp_assert(m_nbasis.size() <= m_A.column_count() - m_A.row_count()); // for the dual the size of non basis can be smaller + SASSERT(m_basis_heading.size() == m_A.column_count()); + SASSERT(m_basis.size() == m_A.row_count()); + SASSERT(m_nbasis.size() <= m_A.column_count() - m_A.row_count()); // for the dual the size of non basis can be smaller if (!basis_has_no_doubles()) return false; @@ -391,8 +391,8 @@ template void lp_core_solver_base::transpose_row } // entering is the new base column, leaving - the column leaving the basis template bool lp_core_solver_base::pivot_column_general(unsigned entering, unsigned leaving, indexed_vector & w) { - lp_assert(m_basis_heading[entering] < 0); - lp_assert(m_basis_heading[leaving] >= 0); + SASSERT(m_basis_heading[entering] < 0); + SASSERT(m_basis_heading[leaving] >= 0); unsigned row_index = m_basis_heading[leaving]; // the tableau case if (!pivot_column_tableau(entering, row_index)) diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index 0aa96a6f9..f925f74f3 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -56,7 +56,7 @@ namespace lp { int choose_entering_column_tableau(); bool needs_to_grow(unsigned bj) const { - lp_assert(!this->column_is_feasible(bj)); + SASSERT(!this->column_is_feasible(bj)); switch (this->m_column_types[bj]) { case column_type::free_column: return false; @@ -72,7 +72,7 @@ namespace lp { } int inf_sign_of_column(unsigned bj) const { - lp_assert(!this->column_is_feasible(bj)); + SASSERT(!this->column_is_feasible(bj)); switch (this->m_column_types[bj]) { case column_type::free_column: return 0; @@ -90,7 +90,7 @@ namespace lp { bool monoid_can_decrease(const row_cell &rc) const { unsigned j = rc.var(); - lp_assert(this->column_is_feasible(j)); + SASSERT(this->column_is_feasible(j)); switch (this->m_column_types[j]) { case column_type::free_column: return true; @@ -113,7 +113,7 @@ namespace lp { bool monoid_can_increase(const row_cell &rc) const { unsigned j = rc.var(); - lp_assert(this->column_is_feasible(j)); + SASSERT(this->column_is_feasible(j)); switch (this->m_column_types[j]) { case column_type::free_column: return true; @@ -247,25 +247,25 @@ namespace lp { void limit_theta_on_basis_column_for_inf_case_m_neg_upper_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m < 0 && this->m_column_types[j] == column_type::upper_bound); + SASSERT(m < 0 && this->m_column_types[j] == column_type::upper_bound); limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited); } void limit_theta_on_basis_column_for_inf_case_m_neg_lower_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m < 0 && this->m_column_types[j] == column_type::lower_bound); + SASSERT(m < 0 && this->m_column_types[j] == column_type::lower_bound); limit_inf_on_bound_m_neg(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited); } void limit_theta_on_basis_column_for_inf_case_m_pos_lower_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m > 0 && this->m_column_types[j] == column_type::lower_bound); + SASSERT(m > 0 && this->m_column_types[j] == column_type::lower_bound); limit_inf_on_lower_bound_m_pos(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited); } void limit_theta_on_basis_column_for_inf_case_m_pos_upper_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m > 0 && this->m_column_types[j] == column_type::upper_bound); + SASSERT(m > 0 && this->m_column_types[j] == column_type::upper_bound); limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited); }; @@ -294,7 +294,7 @@ namespace lp { if (this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) return false; - // lp_assert(calc_current_x_is_feasible() == + // SASSERT(calc_current_x_is_feasible() == // current_x_is_feasible()); return this->current_x_is_feasible() == this->using_infeas_costs(); } @@ -326,7 +326,7 @@ namespace lp { } void update_basis_and_x_tableau_rows(int entering, int leaving, X const &tt) { - lp_assert(entering != leaving); + SASSERT(entering != leaving); update_x_tableau_rows(entering, leaving, tt); this->pivot_column_tableau(entering, this->m_basis_heading[leaving]); this->change_basis(entering, leaving); @@ -346,7 +346,7 @@ namespace lp { } const X &get_val_for_leaving(unsigned j) const { - lp_assert(!this->column_is_feasible(j)); + SASSERT(!this->column_is_feasible(j)); switch (this->m_column_types[j]) { case column_type::fixed: case column_type::upper_bound: @@ -411,7 +411,7 @@ namespace lp { void limit_theta_on_basis_column_for_feas_case_m_neg_no_check( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m < 0); + SASSERT(m < 0); limit_theta((this->m_lower_bounds[j] - this->m_x[j]) / m, theta, unlimited); if (theta < zero_of_type()) theta = zero_of_type(); @@ -420,7 +420,7 @@ namespace lp { bool limit_inf_on_bound_m_neg(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets smaller - lp_assert(m < 0); + SASSERT(m < 0); if (this->below_bound(x, bound)) return false; if (this->above_bound(x, bound)) { @@ -435,7 +435,7 @@ namespace lp { bool limit_inf_on_bound_m_pos(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets larger - lp_assert(m > 0); + SASSERT(m > 0); if (this->above_bound(x, bound)) return false; if (this->below_bound(x, bound)) { @@ -451,7 +451,7 @@ namespace lp { void limit_inf_on_lower_bound_m_pos(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets larger - lp_assert(m > 0); + SASSERT(m > 0); if (this->below_bound(x, bound)) { limit_theta((bound - x) / m, theta, unlimited); } @@ -460,7 +460,7 @@ namespace lp { void limit_inf_on_upper_bound_m_neg(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets smaller - lp_assert(m < 0); + SASSERT(m < 0); if (this->above_bound(x, bound)) { limit_theta((bound - x) / m, theta, unlimited); } @@ -490,7 +490,7 @@ namespace lp { const T &m, X &theta, bool &unlimited) { - // lp_assert(m < 0 && this->m_column_type[j] == column_type::boxed); + // SASSERT(m < 0 && this->m_column_type[j] == column_type::boxed); const X &x = this->m_x[j]; const X &ubound = this->m_upper_bounds[j]; if (this->above_bound(x, ubound)) { @@ -508,7 +508,7 @@ namespace lp { void limit_theta_on_basis_column_for_feas_case_m_pos_no_check( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m > 0); + SASSERT(m > 0); limit_theta((this->m_upper_bounds[j] - this->m_x[j]) / m, theta, unlimited); if (theta < zero_of_type()) { theta = zero_of_type(); @@ -617,7 +617,7 @@ namespace lp { // the delta is between the old and the new cost (old - new) void update_reduced_cost_for_basic_column_cost_change(const T &delta, unsigned j) { - lp_assert(this->m_basis_heading[j] >= 0); + SASSERT(this->m_basis_heading[j] >= 0); unsigned i = static_cast(this->m_basis_heading[j]); for (const row_cell &rc : this->m_A.m_rows[i]) { unsigned k = rc.var(); diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index f14d268a3..74bbad1fc 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -179,7 +179,7 @@ lp_primal_core_solver::get_bound_on_variable_and_update_leaving_precisely( template void lp_primal_core_solver::check_Ax_equal_b() { dense_matrix d(this->m_A); T * ls = d.apply_from_left_with_different_dims(this->m_x); - lp_assert(vectors_are_equal(ls, this->m_b, this->m_m())); + SASSERT(vectors_are_equal(ls, this->m_b, this->m_m())); delete [] ls; } template void lp_primal_core_solver::check_the_bounds() { @@ -189,8 +189,8 @@ template void lp_primal_core_solver::check_the } template void lp_primal_core_solver::check_bound(unsigned i) { - lp_assert (!(this->column_has_lower_bound(i) && (numeric_traits::zero() > this->m_x[i]))); - lp_assert (!(this->column_has_upper_bound(i) && (this->m_upper_bounds[i] < this->m_x[i]))); + SASSERT (!(this->column_has_lower_bound(i) && (numeric_traits::zero() > this->m_x[i]))); + SASSERT (!(this->column_has_upper_bound(i) && (this->m_upper_bounds[i] < this->m_x[i]))); } template void lp_primal_core_solver::check_correctness() { @@ -231,7 +231,7 @@ template unsigned lp_primal_core_solver::get_num // calling it stage1 is too cryptic template void lp_primal_core_solver::find_feasible_solution() { this->m_look_for_feasible_solution_only = true; - lp_assert(this->non_basic_columns_are_set_correctly()); + SASSERT(this->non_basic_columns_are_set_correctly()); this->set_status(lp_status::UNKNOWN); solve(); } diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index 76012cdbf..1a1bf0553 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -30,7 +30,7 @@ template void lp_primal_core_solver::one_iteratio else { advance_on_entering_tableau(entering); } - lp_assert(this->inf_heap_is_correct()); + SASSERT(this->inf_heap_is_correct()); } template void lp_primal_core_solver::advance_on_entering_tableau(int entering) { @@ -116,7 +116,7 @@ unsigned lp_primal_core_solver::solve() { UNREACHABLE(); break; case lp_status::UNBOUNDED: - lp_assert (this->current_x_is_feasible()); + SASSERT (this->current_x_is_feasible()); break; case lp_status::UNSTABLE: @@ -143,7 +143,7 @@ unsigned lp_primal_core_solver::solve() { !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) ); - lp_assert( + SASSERT( this->get_status() == lp_status::CANCELLED || this->current_x_is_feasible() == false @@ -153,12 +153,12 @@ unsigned lp_primal_core_solver::solve() { } template void lp_primal_core_solver::advance_on_entering_and_leaving_tableau(int entering, int leaving, X & t) { - lp_assert(leaving >= 0 && entering >= 0); - lp_assert((this->m_settings.simplex_strategy() == + SASSERT(leaving >= 0 && entering >= 0); + SASSERT((this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) || m_non_basis_list.back() == static_cast(entering)); - lp_assert(!is_neg(t)); - lp_assert(entering != leaving || !is_zero(t)); // otherwise nothing changes + SASSERT(!is_neg(t)); + SASSERT(entering != leaving || !is_zero(t)); // otherwise nothing changes if (entering == leaving) { advance_on_entering_equal_leaving_tableau(entering, t); return; @@ -206,7 +206,7 @@ template int lp_primal_core_solver::find_leaving_ const column_cell & c = col[k]; unsigned i = c.var(); const T & ed = this->m_A.get_val(c); - lp_assert(!numeric_traits::is_zero(ed)); + SASSERT(!numeric_traits::is_zero(ed)); unsigned j = this->m_basis[i]; limit_theta_on_basis_column(j, - ed * m_sign_of_entering_delta, t, unlimited); if (!unlimited) { @@ -225,7 +225,7 @@ template int lp_primal_core_solver::find_leaving_ const column_cell & c = col[k]; unsigned i = c.var(); const T & ed = this->m_A.get_val(c); - lp_assert(!numeric_traits::is_zero(ed)); + SASSERT(!numeric_traits::is_zero(ed)); unsigned j = this->m_basis[i]; unlimited = true; limit_theta_on_basis_column(j, -ed * m_sign_of_entering_delta, ratio, unlimited); @@ -254,9 +254,9 @@ template int lp_primal_core_solver::find_leaving_ return m_leaving_candidates[k]; } template void lp_primal_core_solver::init_run_tableau() { - lp_assert(basis_columns_are_set_correctly()); + SASSERT(basis_columns_are_set_correctly()); this->iters_with_no_cost_growing() = 0; - lp_assert(this->inf_heap_is_correct()); + SASSERT(this->inf_heap_is_correct()); if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) return; if (this->m_settings.backup_costs) @@ -264,13 +264,13 @@ template void lp_primal_core_solver::init_run_tab if (this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) init_tableau_rows(); - lp_assert(this->reduced_costs_are_correct_tableau()); - lp_assert(!this->need_to_pivot_to_basis_tableau()); + SASSERT(this->reduced_costs_are_correct_tableau()); + SASSERT(!this->need_to_pivot_to_basis_tableau()); } template bool lp_primal_core_solver:: update_basis_and_x_tableau(int entering, int leaving, X const & tt) { - lp_assert(entering != leaving); + SASSERT(entering != leaving); update_x_tableau(entering, tt); this->pivot_column_tableau(entering, this->m_basis_heading[leaving]); this->change_basis(entering, leaving); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 8efff27bd..ab90fee38 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -376,7 +376,7 @@ inline void print_blanks(int n, std::ostream & out) { // after a push of the last element we ensure that the vector increases // we also suppose that before the last push the vector was increasing inline void ensure_increasing(vector & v) { - lp_assert(v.size() > 0); + SASSERT(v.size() > 0); unsigned j = v.size() - 1; for (; j > 0; j-- ) if (v[j] <= v[j - 1]) { @@ -392,7 +392,7 @@ inline void ensure_increasing(vector & v) { inline static bool is_rational(const impq & n) { return is_zero(n.y); } inline static mpq fractional_part(const impq & n) { - lp_assert(is_rational(n)); + SASSERT(is_rational(n)); return n.x - floor(n.x); } inline static mpq fractional_part(const mpq & n) { diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index d78ef080f..7e166f99e 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -151,7 +151,6 @@ inline void throw_exception(std::string && str) { } typedef z3_exception exception; -#define lp_assert(_x_) { SASSERT(_x_); } template inline X zero_of_type() { return numeric_traits::zero(); } template inline X one_of_type() { return numeric_traits::one(); } template inline bool is_zero(const X & v) { return numeric_traits::is_zero(v); } diff --git a/src/math/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h index df0897dbe..98d69ad1a 100644 --- a/src/math/lp/permutation_matrix.h +++ b/src/math/lp/permutation_matrix.h @@ -69,7 +69,7 @@ class permutation_matrix unsigned operator[](unsigned i) const { return m_permutation[i]; } void set_val(unsigned i, unsigned pi) { - lp_assert(i < size() && pi < size()); m_permutation[i] = pi; m_rev[pi] = i; } + SASSERT(i < size() && pi < size()); m_permutation[i] = pi; m_rev[pi] = i; } void transpose_from_left(unsigned i, unsigned j); diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h index c86fef4f4..5ab2651ac 100644 --- a/src/math/lp/permutation_matrix_def.h +++ b/src/math/lp/permutation_matrix_def.h @@ -60,7 +60,7 @@ template void permutation_matrix::print(std::ostr template void permutation_matrix::transpose_from_left(unsigned i, unsigned j) { // the result will be this = (i,j)*this - lp_assert(i < size() && j < size() && i != j); + SASSERT(i < size() && j < size() && i != j); auto pi = m_rev[i]; auto pj = m_rev[j]; set_val(pi, j); @@ -69,7 +69,7 @@ template void permutation_matrix::transpose_from_ template void permutation_matrix::transpose_from_right(unsigned i, unsigned j) { // the result will be this = this * (i,j) - lp_assert(i < size() && j < size() && i != j); + SASSERT(i < size() && j < size() && i != j); auto pi = m_permutation[i]; auto pj = m_permutation[j]; set_val(i, pj); diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h index 4c32de2d7..b1b956c76 100644 --- a/src/math/lp/stacked_vector.h +++ b/src/math/lp/stacked_vector.h @@ -38,7 +38,7 @@ public: unsigned m_i; public: ref(stacked_vector &m, unsigned key): m_vec(m), m_i(key) { - lp_assert(key < m.size()); + SASSERT(key < m.size()); } ref & operator=(const B & b) { m_vec.emplace_replace(m_i, b); @@ -81,7 +81,7 @@ public: unsigned m_i; public: ref_const(const stacked_vector &m, unsigned key) :m_vec(m), m_i(key) { - lp_assert(key < m.size()); + SASSERT(key < m.size()); } operator const B&() const { return m_vec.m_vector[m_i]; @@ -120,7 +120,7 @@ public: /* const B & operator[](unsigned a) const { - lp_assert(a < m_vector.size()); + SASSERT(a < m_vector.size()); return m_vector[a]; } */ @@ -139,7 +139,7 @@ public: template void pop_tail(svector & v, unsigned k) { - lp_assert(v.size() >= k); + SASSERT(v.size() >= k); v.resize(v.size() - k); } @@ -149,8 +149,8 @@ public: } void pop(unsigned k) { - lp_assert(m_stack_of_vector_sizes.size() >= k); - lp_assert(k > 0); + SASSERT(m_stack_of_vector_sizes.size() >= k); + SASSERT(k > 0); m_vector.resize(m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]); m_last_update.resize(m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]); pop_tail(m_stack_of_vector_sizes, k); @@ -179,7 +179,7 @@ public: } unsigned peek_size(unsigned k) const { - lp_assert(k > 0 && k <= m_stack_of_vector_sizes.size()); + SASSERT(k > 0 && k <= m_stack_of_vector_sizes.size()); return m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]; } diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 88046aeff..ee42c793b 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -236,7 +236,7 @@ public: for (auto & c : row) { unsigned j = c.var(); auto & col = m_columns[j]; - lp_assert(col[col.size() - 1].var() == m_rows.size() -1 ); // todo : start here!!!! + SASSERT(col[col.size() - 1].var() == m_rows.size() -1 ); // todo : start here!!!! col.pop_back(); } } @@ -263,7 +263,7 @@ public: m_columns.pop_back(); // delete the last column m_stack.pop(); } - lp_assert(is_correct()); + SASSERT(is_correct()); } void multiply_row(unsigned row, T const & alpha) { @@ -279,7 +279,7 @@ public: } T dot_product_with_column(const std_vector & y, unsigned j) const { - lp_assert(j < column_count()); + SASSERT(j < column_count()); T ret = numeric_traits::zero(); for (auto & it : m_columns[j]) { ret += y[it.var()] * get_val(it); // get_value_of_column_cell(it); @@ -302,12 +302,12 @@ public: // now fix the columns for (auto & rc : m_rows[i]) { column_cell & cc = m_columns[rc.var()][rc.offset()]; - lp_assert(cc.var() == ii); + SASSERT(cc.var() == ii); cc.var() = i; } for (auto & rc : m_rows[ii]) { column_cell & cc = m_columns[rc.var()][rc.offset()]; - lp_assert(cc.var() == i); + SASSERT(cc.var() == i); cc.var() = ii; } @@ -345,7 +345,7 @@ public: void fill_last_row_with_pivoting(const term& row, unsigned bj, // the index of the basis column const std_vector & basis_heading) { - lp_assert(row_count() > 0); + SASSERT(row_count() > 0); m_work_vector.clear(); m_work_vector.resize(column_count()); T a; @@ -366,7 +366,7 @@ public: for (unsigned j : m_work_vector.m_index) { set (last_row, j, m_work_vector.m_data[j]); } - lp_assert(column_count() > 0); + SASSERT(column_count() > 0); set(last_row, column_count() - 1, one_of_type()); } @@ -382,7 +382,7 @@ public: template L dot_product_with_row(unsigned row, const std_vector & w) const { L ret = zero_of_type(); - lp_assert(row < m_rows.size()); + SASSERT(row < m_rows.size()); for (auto & it : m_rows[row]) { ret += w[it.var()] * it.coeff(); } diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index 0fd34adae..aa3fff3dc 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -87,7 +87,7 @@ namespace lp { template void static_matrix::add_rows(const mpq& alpha, unsigned i, unsigned k) { - lp_assert(i < row_count() && k < row_count() && i != k); + SASSERT(i < row_count() && k < row_count() && i != k); auto & rowk = m_rows[k]; scan_row_strip_to_work_vector(rowk); unsigned prev_size_k = static_cast(rowk.size()); diff --git a/src/math/lp/test_bound_analyzer.h b/src/math/lp/test_bound_analyzer.h index 1ca99d637..6cc78526f 100644 --- a/src/math/lp/test_bound_analyzer.h +++ b/src/math/lp/test_bound_analyzer.h @@ -89,7 +89,7 @@ public : void analyze_i_for_upper(unsigned i) { mpq l; bool strict = false; - lp_assert(is_zero(l)); + SASSERT(is_zero(l)); for (unsigned k = 0; k < m_index.size(); k++) { if (k == i) continue; @@ -179,7 +179,7 @@ public : void analyze_i_for_lower(unsigned i) { mpq l; - lp_assert(is_zero(l)); + SASSERT(is_zero(l)); bool strict = false; for (unsigned k = 0; k < m_index.size(); k++) { if (k == i) diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index dedbaa4d0..49771ae47 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -91,7 +91,7 @@ public: unsigned external_to_local(unsigned j) const { auto it = m_external_to_local.find(j); - lp_assert(it != m_external_to_local.end()); + SASSERT(it != m_external_to_local.end()); return it->second; } diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 9ac675d1a..04ec122ab 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -72,7 +72,7 @@ struct gomory_test { expl.add_pair(column_lower_bound_constraint(x_j), new_a); } else { - lp_assert(at_upper(x_j)); + SASSERT(at_upper(x_j)); if (a.is_pos()) { new_a = a / f_0; new_a.neg(); // the upper terms are inverted. @@ -88,9 +88,9 @@ struct gomory_test { } void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term & t, explanation& expl, mpq & lcm_den, const mpq& f_0, const mpq& one_minus_f_0) { - lp_assert(is_integer(x_j)); - lp_assert(!a.is_int()); - lp_assert(f_0 > zero_of_type() && f_0 < one_of_type()); + SASSERT(is_integer(x_j)); + SASSERT(!a.is_int()); + SASSERT(f_0 > zero_of_type() && f_0 < one_of_type()); mpq f_j = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " x_j = " << x_j << ", k = " << k << "\n"; @@ -99,7 +99,7 @@ struct gomory_test { tout << "1 - f_0: " << one_minus_f_0 << "\n"; tout << "at_low(" << x_j << ") = " << at_low(x_j) << std::endl; ); - lp_assert (!f_j.is_zero()); + SASSERT (!f_j.is_zero()); mpq new_a; if (at_low(x_j)) { if (f_j <= one_minus_f_0) { @@ -112,7 +112,7 @@ struct gomory_test { expl.add_pair(column_lower_bound_constraint(x_j), new_a); } else { - lp_assert(at_upper(x_j)); + SASSERT(at_upper(x_j)); if (f_j <= f_0) { new_a = f_j / f_0; } @@ -134,13 +134,13 @@ struct gomory_test { } void adjust_term_and_k_for_some_ints_case_gomory(lar_term& t, mpq& k, mpq &lcm_den) { - lp_assert(!t.is_empty()); + SASSERT(!t.is_empty()); auto pol = t.coeffs_as_vector(); t.clear(); if (pol.size() == 1) { TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;); unsigned v = pol[0].second; - lp_assert(is_integer(v)); + SASSERT(is_integer(v)); const mpq& a = pol[0].first; k /= a; if (a.is_pos()) { // we have av >= k @@ -162,7 +162,7 @@ struct gomory_test { tout << pol[i].first << " " << pol[i].second << "\n"; } tout << "k: " << k << "\n";); - lp_assert(lcm_den.is_pos()); + SASSERT(lcm_den.is_pos()); if (!lcm_den.is_one()) { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { @@ -183,7 +183,7 @@ struct gomory_test { k.neg(); } TRACE("gomory_cut_detail", tout << "k = " << k << std::endl;); - lp_assert(k.is_int()); + SASSERT(k.is_int()); } void print_term(lar_term & t, std::ostream & out) { diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 5afeea3fa..3de741d42 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -384,7 +384,7 @@ vector allocate_basis_heading( void init_basic_part_of_basis_heading(vector &basis, vector &basis_heading) { - lp_assert(basis_heading.size() >= basis.size()); + SASSERT(basis_heading.size() >= basis.size()); unsigned m = basis.size(); for (unsigned i = 0; i < m; i++) { unsigned column = basis[i]; @@ -577,7 +577,7 @@ void test_stacked_unsigned() { v = 3; v = 4; v.pop(); - lp_assert(v == 2); + SASSERT(v == 2); v++; v++; std::cout << "before push v=" << v << std::endl; @@ -587,7 +587,7 @@ void test_stacked_unsigned() { v += 1; std::cout << "v = " << v << std::endl; v.pop(2); - lp_assert(v == 4); + SASSERT(v == 4); const unsigned &rr = v; std::cout << rr << std::endl; } @@ -751,22 +751,23 @@ void test_numeric_pair() { numeric_pair c(0.1, 0.5); a += 2 * c; a -= c; - lp_assert(a == b + c); + SASSERT(a == b + c); numeric_pair d = a * 2; std::cout << a << std::endl; - lp_assert(b == b); - lp_assert(b < a); - lp_assert(b <= a); - lp_assert(a > b); - lp_assert(a != b); - lp_assert(a >= b); - lp_assert(-a < b); - lp_assert(a < 2 * b); - lp_assert(b + b > a); - lp_assert(lp::mpq(2.1) * b + b > a); - lp_assert(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a); + SASSERT(b == b); + SASSERT(b < a); + SASSERT(b <= a); + SASSERT(a > b); + SASSERT(a != b); + SASSERT(a >= b); + SASSERT(-a < b); + SASSERT(a < 2 * b); + SASSERT(b + b > a); + SASSERT(lp::mpq(2.1) * b + b > a); + SASSERT(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a); std::cout << -b * lp::mpq(2.1) - b << std::endl; - lp_assert(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b); + SASSERT(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b); + std::cout << -b * (lp::mpq(2.1) + 1) << std::endl; } void get_matrix_dimensions(std::ifstream &f, unsigned &m, unsigned &n) { @@ -829,7 +830,7 @@ void test_term() { << t.second.get_double() << ","; } - std::cout << "\ntableu after cube\n"; + std::cout << "\ntableau after cube\n"; solver.pp(std::cout).print(); std::cout << "Ax_is_correct = " << solver.ax_is_correct() << "\n"; } @@ -854,7 +855,7 @@ void test_evidence_for_total_inf_simple(argument_parser &args_parser) { auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; std::unordered_map model; - lp_assert(solver.get_status() == lp_status::INFEASIBLE); + SASSERT(solver.get_status() == lp_status::INFEASIBLE); } void test_bound_propagation_one_small_sample1() { /* @@ -1060,8 +1061,8 @@ void test_total_case_l() { // ls.solve(); // my_bound_propagator bp(ls); // ls.propagate_bounds_for_touched_rows(bp); - // lp_assert(ev.size() == 4); - // lp_assert(contains_j_kind(x, GE, - one_of_type(), ev)); + // SASSERT(ev.size() == 4); + // SASSERT(contains_j_kind(x, GE, - one_of_type(), ev)); } void test_bound_propagation() { test_total_case_u(); @@ -1077,14 +1078,14 @@ void test_int_set() { indexed_uint_set s; s.insert(1); s.insert(2); - lp_assert(s.contains(2)); - lp_assert(s.size() == 2); + SASSERT(s.contains(2)); + SASSERT(s.size() == 2); s.remove(2); - lp_assert(s.size() == 1); + SASSERT(s.size() == 1); s.insert(3); s.insert(2); s.reset(); - lp_assert(s.size() == 0); + SASSERT(s.size() == 0); std::cout << "done test_int_set\n"; } @@ -1192,13 +1193,13 @@ void get_random_interval(bool &neg_inf, bool &pos_inf, int &x, int &y) { pos_inf = false; if (!neg_inf) { y = x + my_random() % (101 - x); - lp_assert(y >= x); + SASSERT(y >= x); } else { y = my_random() % 100; } } - lp_assert((neg_inf || (0 <= x && x <= 100)) && - (pos_inf || (0 <= y && y <= 100))); + SASSERT((neg_inf || (0 <= x && x <= 100)) && + (pos_inf || (0 <= y && y <= 100))); } void test_gomory_cut_0() { @@ -1628,7 +1629,7 @@ void test_maximize_term() { solver.add_var_bound(term_x_min_y, LE, zero_of_type()); solver.add_var_bound(term_2x_pl_2y, LE, mpq(5)); solver.find_feasible_solution(); - lp_assert(solver.get_status() == lp_status::OPTIMAL); + SASSERT(solver.get_status() == lp_status::OPTIMAL); std::cout << solver.constraints(); std::unordered_map model; solver.get_model(model); @@ -1671,7 +1672,8 @@ void test_dio() { lpvar fx_7 = solver.add_var(_fx_7, true); lpvar fx_17 = solver.add_var(_fx_17, true); vector> term_ls; - /* 3x1 + 3x2 + 14x3 − 7 */ + /* 3x1 + 3x2 +```cpp + 14x3 − 7 */ term_ls.push_back(std::pair(mpq(3), x1)); term_ls.push_back(std::pair(mpq(3), x2)); term_ls.push_back(std::pair(mpq(14), x3)); @@ -1701,7 +1703,7 @@ void test_dio() { solver.add_var_bound(t1, LE, mpq(0)); solver.add_var_bound(t1, GE, mpq(0)); // solver.find_feasible_solution(); - //lp_assert(solver.get_status() == lp_status::OPTIMAL); + //SASSERT(solver.get_status() == lp_status::OPTIMAL); enable_trace("dioph_eq"); enable_trace("dioph_eq_fresh"); #ifdef Z3DEBUG @@ -1908,13 +1910,13 @@ void asserts_on_patching(const rational &x, const rational &alpha) { auto a2 = denominator(alpha); auto x1 = numerator(x); auto x2 = denominator(x); - lp_assert(a1.is_pos()); - lp_assert(abs(a1) < abs(a2)); - lp_assert(coprime(a1, a2)); - lp_assert(x1.is_pos()); - lp_assert(x1 < x2); - lp_assert(coprime(x1, x2)); - lp_assert((a2 / x2).is_int()); + SASSERT(a1.is_pos()); + SASSERT(abs(a1) < abs(a2)); + SASSERT(coprime(a1, a2)); + SASSERT(x1.is_pos()); + SASSERT(x1 < x2); + SASSERT(coprime(x1, x2)); + SASSERT((a2 / x2).is_int()); } void get_patching_deltas(const rational &x, const rational &alpha, rational &delta_0, rational &delta_1) { std::cout << "get_patching_deltas(" << x << ", " << alpha << ")" << std::endl; @@ -1922,7 +1924,7 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del auto a2 = denominator(alpha); auto x1 = numerator(x); auto x2 = denominator(x); - lp_assert(divides(x2, a2)); + SASSERT(divides(x2, a2)); // delta has to be integral. // We need to find delta such that x1/x2 + (a1/a2)*delta is integral. // Then a2*x1/x2 + a1*delta is integral, that means that t = a2/x2 is integral. @@ -1936,17 +1938,17 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del // We know that a2 and a1 are coprime, and x2 divides a2, so x2 and a1 are coprime. rational u, v; auto g = gcd(a1, x2, u, v); - lp_assert(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2); + SASSERT(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2); std::cout << "u = " << u << ", v = " << v << std::endl; std::cout << "x= " << (x1 / x2) << std::endl; std::cout << "x + (a1 / a2) * (-u * t) * x1 = " << x + (a1 / a2) * (-u * t) * x1 << std::endl; - lp_assert((x + (a1 / a2) * (-u * t) * x1).is_int()); + SASSERT((x + (a1 / a2) * (-u * t) * x1).is_int()); // 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l. rational d = u * t * x1; delta_0 = mod(d, a2); - lp_assert(delta_0 > 0); + SASSERT(delta_0 > 0); delta_1 = delta_0 - a2; - lp_assert(delta_1 < 0); + SASSERT(delta_1 < 0); std::cout << "delta_0 = " << delta_0 << std::endl; std::cout << "delta_1 = " << delta_1 << std::endl; } @@ -1974,10 +1976,10 @@ void test_patching_alpha(const rational &x, const rational &alpha) { rational delta_0, delta_1; get_patching_deltas(x, alpha, delta_0, delta_1); - lp_assert(delta_0 * delta_1 < 0); + SASSERT(delta_0 * delta_1 < 0); - lp_assert((x - alpha * delta_0).is_int()); - lp_assert((x - alpha * delta_1).is_int()); + SASSERT((x - alpha * delta_0).is_int()); + SASSERT((x - alpha * delta_1).is_int()); try_find_smaller_delta(x, alpha, delta_0, delta_1); // std::cout << "delta_minus = " << delta_minus << ", delta_1 = " << delta_1 << "\n"; // std::cout << "x + alpha*delta_minus = " << x + alpha * delta_minus << "\n"; @@ -1988,7 +1990,7 @@ void find_a1_x1_x2_and_fix_a2(int &x1, int &x2, int &a1, int &a2) { x2 = (rand() % a2) + (int)(a2 / 3); auto g = gcd(rational(a2), rational(x2)); a2 *= (x2 / numerator(g).get_int32()); - lp_assert(rational(a2, x2).is_int()); + SASSERT(rational(a2, x2).is_int()); do { x1 = rand() % (unsigned)x2 + 1; } while (!coprime(x1, x2)); @@ -1998,6 +2000,7 @@ void find_a1_x1_x2_and_fix_a2(int &x1, int &x2, int &a1, int &a2) { } while (!coprime(a1, a2)); } + void test_patching() { srand(1); // repeat the test 100 times diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 0e638399f..3458e3b2a 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -117,13 +117,13 @@ namespace lp { void fill_simple_elem(lisp_elem & lm) { int separator = first_separator(); - lp_assert(-1 != separator && separator != 0); + SASSERT(-1 != separator && separator != 0); lm.m_head = m_line.substr(0, separator); m_line = m_line.substr(separator); } void fill_nested_elem(lisp_elem & lm) { - lp_assert(m_line[0] == '('); + SASSERT(m_line[0] == '('); m_line = m_line.substr(1); int separator = first_separator(); lm.m_head = m_line.substr(0, separator); @@ -190,11 +190,11 @@ namespace lp { } void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { - // lp_assert(el.m_head == "0"); // do nothing for the time being + // SASSERT(el.m_head == "0"); // do nothing for the time being } void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) { - lp_assert(el.m_elems.size() == 2); + SASSERT(el.m_elems.size() == 2); set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]); adjust_right_side(c, el.m_elems[1]); } @@ -210,7 +210,7 @@ namespace lp { add_mult_elem(c, el.m_elems); } else if (el.m_head == "~") { lisp_elem & minel = el.m_elems[0]; - lp_assert(minel.is_simple()); + SASSERT(minel.is_simple()); c.m_right_side += mpq(str_to_int(minel.m_head)); } else { std::cout << "unexpected input " << el.m_head << std::endl; @@ -220,14 +220,14 @@ namespace lp { } std::string get_name(lisp_elem & name) { - lp_assert(name.is_simple()); - lp_assert(!is_integer(name.m_head)); + SASSERT(name.is_simple()); + SASSERT(!is_integer(name.m_head)); return name.m_head; } void add_mult_elem(formula_constraint & c, std::vector & els) { - lp_assert(els.size() == 2); + SASSERT(els.size() == 2); mpq coeff = get_coeff(els[0]); std::string col_name = get_name(els[1]); c.add_pair(coeff, col_name); @@ -237,16 +237,16 @@ namespace lp { if (le.is_simple()) { return mpq(str_to_int(le.m_head)); } else { - lp_assert(le.m_head == "~"); - lp_assert(le.size() == 1); + SASSERT(le.m_head == "~"); + SASSERT(le.size() == 1); lisp_elem & el = le.m_elems[0]; - lp_assert(el.is_simple()); + SASSERT(el.is_simple()); return -mpq(str_to_int(el.m_head)); } } int str_to_int(std::string & s) { - lp_assert(is_integer(s)); + SASSERT(is_integer(s)); return atoi(s.c_str()); } @@ -254,7 +254,7 @@ namespace lp { if (el.size()) { add_complex_sum_elem(c, el); } else { - lp_assert(is_integer(el.m_head)); + SASSERT(is_integer(el.m_head)); int v = atoi(el.m_head.c_str()); mpq vr(v); c.m_right_side -= vr;