diff --git a/src/math/lp/column.h b/src/math/lp/column.h index 68e1e557a..dc4b63134 100644 --- a/src/math/lp/column.h +++ b/src/math/lp/column.h @@ -40,7 +40,6 @@ class lar_term; // forward definition class column { u_dependency* m_lower_bound_witness = nullptr; u_dependency* m_upper_bound_witness = nullptr; - bool m_associated_with_row = false; lar_term* m_term = nullptr; public: lar_term* term() const { return m_term; } @@ -50,13 +49,11 @@ public: u_dependency*& upper_bound_witness() { return m_upper_bound_witness; } u_dependency* upper_bound_witness() const { return m_upper_bound_witness; } - column() = delete; - column(bool) = delete; + column() {} - column(bool associated_with_row, lar_term* term) : - m_associated_with_row(associated_with_row), m_term(term) {} + column(lar_term* term) : m_term(term) {} - bool associated_with_row() const { return m_associated_with_row; } + bool associated_with_row() const { return m_term != nullptr; } }; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f687f87f0..5818641f1 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1577,7 +1577,7 @@ namespace lp { return local_j; lp_assert(m_columns.size() == A_r().column_count()); local_j = A_r().column_count(); - m_columns.push_back(column(false, nullptr)); // false - not associated with a row, nullptr for term + m_columns.push_back(column()); m_trail.push(undo_add_column(*this)); while (m_usage_in_terms.size() <= local_j) m_usage_in_terms.push_back(0); @@ -1704,7 +1704,7 @@ namespace lp { // j will be a new variable unsigned j = A_r().column_count(); SASSERT(ext_index == null_lpvar || external_to_local(ext_index) == j); - column ul(true, term); // true - to mark this column as associated_with_row + column ul(term); term->j() = j; // point from the term to the column m_columns.push_back(ul); m_trail.push(undo_add_column(*this));