From 7fe703e2296961de2edf2afcd89d529d5b284028 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 20 Dec 2024 10:37:23 -1000
Subject: [PATCH] simplify column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/column.h | 9 +++------
src/math/lp/lar_solver.cpp | 4 ++--
2 files changed, 5 insertions(+), 8 deletions(-)
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));