mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

changes in column_info of lar_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-09-22 12:01:24 -07:00
parent 3113901c8f
commit 43f89dc2cc
5 changed files with 5 additions and 19 deletions
Show stats 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)) 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) { column_info(const column_info & ci) {
m_name = ci.m_name; m_name = ci.m_name;
m_lower_bound_is_set = ci.m_lower_bound_is_set; 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; return false;
} }
column_type lar_solver::get_column_type(const column_info<mpq> & ci) { column_type lar_solver::get_column_type(unsigned j) const{
auto ret = ci.get_column_type_no_flipping(); return m_mpq_lar_core_solver.m_column_types[j];
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;
} }
std::string lar_solver::get_column_name(unsigned j) const { 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); 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; 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; break;
case column_type::free_column: case column_type::free_column:
out << "( _" << this->m_x[j] << "_)" << std::endl; out << "( _" << this->m_x[j] << "_)" << std::endl;
break;
default: default:
lp_unreachable(); lp_unreachable();
} }

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

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