From 97c1ba4641138b3990cb93a8aa10c3a1ea6d3f4e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 4 Mar 2023 11:56:23 -0800 Subject: [PATCH] rm get_column_in_lu_mode --- src/math/lp/lar_solver.h | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index f13231610bd..20556deab75 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -267,13 +267,7 @@ class lar_solver : public column_namer { void shrink_explanation_to_minimum(vector> & explanation) const; inline bool column_value_is_integer(unsigned j) const { return get_column_value(j).is_int(); } bool model_is_int_feasible() const; - inline - indexed_vector & get_column_in_lu_mode(unsigned j) { - m_column_buffer.clear(); - m_column_buffer.resize(A_r().row_count()); - m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); - return m_column_buffer; - } + bool bound_is_integer_for_integer_column(unsigned j, const mpq & right_side) const; inline lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; } void catch_up_in_updating_int_solver();