diff --git a/src/util/lp/column_info.h b/src/util/lp/column_info.h index 407f40dfc..2a38900c1 100644 --- a/src/util/lp/column_info.h +++ b/src/util/lp/column_info.h @@ -69,16 +69,6 @@ public: m_column_index(static_cast(-1)) {} - column_info(unsigned column_index) : - m_lower_bound_is_set(false), - m_lower_bound_is_strict(false), - m_upper_bound_is_set (false), - m_upper_bound_is_strict (false), - m_is_fixed(false), - m_cost(numeric_traits::zero()), - m_column_index(column_index) { - } - column_info(const column_info & ci) { m_name = ci.m_name; m_lower_bound_is_set = ci.m_lower_bound_is_set; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 30494aa1c..c83268602 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -909,13 +909,8 @@ bool lar_solver::try_to_set_fixed(column_info & ci) { return false; } -column_type lar_solver::get_column_type(const column_info & ci) { - auto ret = ci.get_column_type_no_flipping(); - if (ret == column_type::boxed) { // changing boxed to fixed because of the no span - if (ci.get_lower_bound() == ci.get_upper_bound()) - ret = column_type::fixed; - } - return ret; +column_type lar_solver::get_column_type(unsigned j) const{ + return m_mpq_lar_core_solver.m_column_types[j]; } std::string lar_solver::get_column_name(unsigned j) const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f3aa4f23b..cfe581ba3 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -395,7 +395,7 @@ public: bool try_to_set_fixed(column_info & ci); - column_type get_column_type(const column_info & ci); + column_type get_column_type(unsigned j) const; std::string get_column_name(unsigned j) const; diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h index 1e9edbd31..872922f60 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/util/lp/lp_primal_core_solver_def.h @@ -1238,6 +1238,7 @@ template void lp_primal_core_solver::print_column break; case column_type::free_column: out << "( _" << this->m_x[j] << "_)" << std::endl; + break; default: lp_unreachable(); } diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h index 10c7a6feb..9b385dee6 100644 --- a/src/util/lp/lp_solver_def.h +++ b/src/util/lp/lp_solver_def.h @@ -24,7 +24,7 @@ Revision History: namespace lp { template column_info * lp_solver::get_or_create_column_info(unsigned column) { auto it = m_map_from_var_index_to_column_info.find(column); - return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info(static_cast(-1))) : it->second; + return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info()) : it->second; } template