From db5ac5afa8087d5176a40cc66e88800e16954e05 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 1 Aug 2019 11:44:39 -0700 Subject: [PATCH 1/2] fix a bug in lar_solver in queryaing if a column is int Signed-off-by: Lev Nachmanson --- src/util/lp/gomory.cpp | 8 ++++---- src/util/lp/hnf.h | 4 ++-- src/util/lp/hnf_cutter.h | 2 +- src/util/lp/int_solver.cpp | 20 ++++++++++---------- src/util/lp/int_solver.h | 2 +- src/util/lp/lar_solver.cpp | 3 ++- src/util/lp/lp_core_solver_base.h | 4 +++- src/util/lp/lp_core_solver_base_def.h | 5 ++--- src/util/lp/lp_utils.h | 2 +- 9 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index ad1c0262563..d5fae828f2f 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -47,7 +47,7 @@ class gomory::imp { bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); } void int_case_in_gomory_cut(unsigned j) { - lp_assert(is_int(j) && m_fj.is_pos()); + lp_assert(m_int_solver.column_is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", tout << " k = " << m_k; tout << ", fj: " << m_fj << ", "; @@ -117,7 +117,7 @@ class gomory::imp { if (pol.size() == 1) { TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;); unsigned v = pol[0].second; - lp_assert(is_int(v)); + lp_assert(m_int_solver.column_is_int(v)); const mpq& a = pol[0].first; m_k /= a; if (a.is_pos()) { // we have av >= k @@ -139,7 +139,7 @@ class gomory::imp { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { pi.first *= m_lcm_den; - SASSERT(!is_int(pi.second) || pi.first.is_int()); + SASSERT(!m_int_solver.column_is_int(pi.second) || pi.first.is_int()); } m_k *= m_lcm_den; } @@ -195,7 +195,7 @@ class gomory::imp { } void dump_declaration(std::ostream& out, unsigned v) const { - out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n"; + out << "(declare-const " << var_name(v) << (m_int_solver.column_is_int(v) ? " Int" : " Real") << ")\n"; } void dump_declarations(std::ostream& out) const { diff --git a/src/util/lp/hnf.h b/src/util/lp/hnf.h index 8edce39e089..b6828d05320 100644 --- a/src/util/lp/hnf.h +++ b/src/util/lp/hnf.h @@ -137,7 +137,7 @@ void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & overflow = true; return; } - lp_assert(is_int(m[i][j])); + lp_assert(is_integer(m[i][j])); } } } @@ -577,7 +577,7 @@ class hnf { process_row_modulo(); lp_assert(is_pos(m_W[m_i][m_i])); m_R /= m_W[m_i][m_i]; - lp_assert(is_int(m_R)); + lp_assert(is_integer(m_R)); m_half_R = floor(m_R / 2); } } diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h index 3f9038651b9..c7070ef9a44 100644 --- a/src/util/lp/hnf_cutter.h +++ b/src/util/lp/hnf_cutter.h @@ -120,7 +120,7 @@ class hnf_cutter { int ret = -1; int n = 0; for (int i = 0; i < static_cast(b.size()); i++) { - if (is_int(b[i])) continue; + if (is_integer(b[i])) continue; if (n == 0 ) { lp_assert(ret == -1); n = 1; diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index ad6766f643f..0d25a9d1155 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -16,7 +16,7 @@ void int_solver::trace_inf_rows() const { TRACE("arith_int_rows", unsigned num = m_lar_solver->A_r().column_count(); for (unsigned v = 0; v < num; v++) { - if (is_int(v) && !get_value(v).is_int()) { + if (column_is_int(v) && !get_value(v).is_int()) { display_column(tout, v); } } @@ -197,7 +197,7 @@ impq int_solver::get_cube_delta_for_term(const lar_term& t) const { bool seen_minus = false; bool seen_plus = false; for(const auto & p : t) { - if (!is_int(p.var())) + if (!column_is_int(p.var())) goto usual_delta; const mpq & c = p.coeff(); if (c == one_of_type()) { @@ -215,7 +215,7 @@ impq int_solver::get_cube_delta_for_term(const lar_term& t) const { usual_delta: mpq delta = zero_of_type(); for (const auto & p : t) - if (is_int(p.var())) + if (column_is_int(p.var())) delta += abs(p.coeff()); delta *= mpq(1, 2); @@ -759,7 +759,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq unsigned i = lcs.m_r_basis[row_index]; impq const & xi = get_value(i); - if (is_int(i) && is_int(j) && !a.is_int()) + if (column_is_int(i) && column_is_int(j) && !a.is_int()) m = lcm(m, denominator(a)); if (a.is_neg()) { if (has_low(i)) @@ -791,12 +791,12 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq return (inf_l || inf_u || l <= u); } -bool int_solver::is_int(unsigned j) const { +bool int_solver::column_is_int(unsigned j) const { return m_lar_solver->column_is_int(j); } bool int_solver::is_real(unsigned j) const { - return !is_int(j); + return !column_is_int(j); } bool int_solver::value_is_int(unsigned j) const { @@ -821,7 +821,7 @@ void int_solver::display_column(std::ostream & out, unsigned j) const { } bool int_solver::column_is_int_inf(unsigned j) const { - return is_int(j) && (!value_is_int(j)); + return column_is_int(j) && (!value_is_int(j)); } bool int_solver::is_base(unsigned j) const { @@ -912,7 +912,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) { set_value_for_nbasic_column_ignore_old_values(j, new_val); return true; } - if (is_int(j)) { + if (column_is_int(j)) { if (!inf_l) { l = ceil(l); if (!m.is_one()) @@ -940,7 +940,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) { set_value_for_nbasic_column_ignore_old_values(j, new_val); return true; } - if (!is_int(j)) { + if (!column_is_int(j)) { SASSERT(!inf_l && !inf_u); mpq delta = mpq(random() % (range + 1)); impq new_val = l + ((delta * (u - l)) / mpq(range)); @@ -975,7 +975,7 @@ bool int_solver::non_basic_columns_are_at_bounds() const { return false; break; default: - if (is_int(j) && !val.is_int()) { + if (column_is_int(j) && !val.is_int()) { return false; } } diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 9fb6aa06665..9ccf5724186 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -59,7 +59,7 @@ class int_solver { bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; const impq & upper_bound(unsigned j) const; - bool is_int(unsigned j) const; + bool column_is_int(unsigned j) const; const impq & get_value(unsigned j) const; bool at_lower(unsigned j) const; bool at_upper(unsigned j) const; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 503624a6e56..9fa84297cec 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -512,7 +512,7 @@ bool lar_solver::move_non_basic_column_to_bounds(unsigned j) { } break; default: - if (is_int(j) && !val.is_int()) { + if (column_is_int(j) && !val.is_int()) { set_value_for_nbasic_column(j, impq(floor(val))); return true; } @@ -526,6 +526,7 @@ void lar_solver::set_value_for_nbasic_column(unsigned j, const impq & new_val) { auto & x = m_mpq_lar_core_solver.m_r_x[j]; auto delta = new_val - x; x = new_val; + m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j); change_basic_columns_dependend_on_a_given_nb_column(j, delta); } diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 4c17df29c98..c35dd176cfb 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -550,6 +550,7 @@ class lp_core_solver_base { bool non_basic_columns_are_set_correctly() const { for (unsigned j : this->m_nbasis) if (!column_is_feasible(j)) { + TRACE("lp_core", tout << "inf col "; print_column_info(j, tout) << "\n";); return false; } return true; @@ -573,7 +574,7 @@ class lp_core_solver_base { } } - void print_column_info(unsigned j, std::ostream & out) const { + std::ostream& print_column_info(unsigned j, std::ostream & out) const { out << "j = " << j << ",\tname = "<< column_name(j) << "\t"; switch (m_column_types[j]) { case column_type::fixed: @@ -598,6 +599,7 @@ class lp_core_solver_base { out << " base\n"; else out << " \n"; + return out; } bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/util/lp/lp_core_solver_base_def.h index 6844ab8397c..8a4fc38bb62 100644 --- a/src/util/lp/lp_core_solver_base_def.h +++ b/src/util/lp/lp_core_solver_base_def.h @@ -511,12 +511,11 @@ template bool lp_core_solver_base::calc_current_x } template bool lp_core_solver_base::inf_set_is_correct() const { - unsigned j = this->m_n(); - while (j--) { + for (unsigned j = 0; j < this->m_n(); j++) { bool belongs_to_set = m_inf_set.contains(j); bool is_feas = column_is_feasible(j); - if (is_feas == belongs_to_set) { + TRACE("lp_core", tout << "incorrectly set column in inf set "; print_column_info(j, tout) << "\n";); return false; } } diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h index 573fc319c1d..069bf9abf31 100644 --- a/src/util/lp/lp_utils.h +++ b/src/util/lp/lp_utils.h @@ -86,7 +86,7 @@ template inline X one_of_type() { return numeric_traits::one(); template inline bool is_zero(const X & v) { return numeric_traits::is_zero(v); } template inline bool is_pos(const X & v) { return numeric_traits::is_pos(v); } template inline bool is_neg(const X & v) { return numeric_traits::is_neg(v); } -template inline bool is_int(const X & v) { return numeric_traits::is_int(v); } +template inline bool is_integer(const X & v) { return numeric_traits::is_int(v); } template inline X ceil_ratio(const X & a, const X & b) { return numeric_traits::ceil_ratio(a, b); } template inline X floor_ratio(const X & a, const X & b) { return numeric_traits::floor_ratio(a, b); } From e9e950062aa48e65cf23c40baf09df756294fb96 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 1 Aug 2019 14:09:26 -0700 Subject: [PATCH 2/2] fix the build Signed-off-by: Lev Nachmanson --- src/test/lp/gomory_test.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 972466dc36a..0ac55406cdc 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -86,7 +86,7 @@ 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_int(x_j)); + lp_assert(is_integer(x_j)); lp_assert(!a.is_int()); lp_assert(f_0 > zero_of_type() && f_0 < one_of_type()); mpq f_j = fractional_part(a); @@ -138,7 +138,7 @@ struct gomory_test { if (pol.size() == 1) { TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;); unsigned v = pol[0].second; - lp_assert(is_int(v)); + lp_assert(is_integer(v)); const mpq& a = pol[0].first; k /= a; if (a.is_pos()) { // we have av >= k @@ -165,7 +165,7 @@ struct gomory_test { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { pi.first *= lcm_den; - SASSERT(!is_int(pi.second) || pi.first.is_int()); + SASSERT(!is_integer(pi.second) || pi.first.is_int()); } k *= lcm_den; }