mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge pull request #1843 from levnach/gomory

Browse source 
changes in column_info of lar_solver
This commit is contained in:
Lev Nachmanson 2018-09-22 14:29:40 -07:00 • committed by GitHub
commit 2d46234fd0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 5 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/lp/column_info.h
View file

@ -69,16 +69,6 @@ public:
m_column_index(static_cast<unsigned>(-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<T>::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;

9
src/util/lp/lar_solver.cpp
View file

@ -909,13 +909,8 @@ bool lar_solver::try_to_set_fixed(column_info<mpq> & ci) {
return false;
}
column_type lar_solver::get_column_type(const column_info<mpq> & 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 {

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

@ -395,7 +395,7 @@ public:
bool try_to_set_fixed(column_info<mpq> & ci);
column_type get_column_type(const column_info<mpq> & ci);
column_type get_column_type(unsigned j) const;
std::string get_column_name(unsigned j) const;

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

@ -1238,6 +1238,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
break;
case column_type::free_column:
out << "( _" << this->m_x[j] << "_)" << std::endl;
break;
default:
lp_unreachable();
}

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

@ -24,7 +24,7 @@ Revision History:
namespace lp {
template <typename T, typename X> column_info<T> * lp_solver<T, X>::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<T>(static_cast<unsigned>(-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<T>()) : it->second;
}
template <typename T, typename X>