From 57b665d07507ea3688b659de7bcc6a73156563e8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 24 Dec 2024 07:32:49 -1000 Subject: [PATCH] work on incremental dio Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 10 +++++----- src/math/lp/static_matrix.h | 2 ++ 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index d0f174673..adfe54fed 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -358,6 +358,8 @@ namespace lp { SASSERT(m_l_matrix.row_count() == m_e_matrix.row_count()); // fill m_l_matrix row m_l_matrix.add_row(); + // todo: consider to compress variables t.j() by using a devoted var_register for term columns + m_l_matrix.add_columns_up_to(t.j()); m_l_matrix.add_new_element(entry_index, t.j(), mpq(1)); // fill E-entry m_e_matrix.add_row(); @@ -369,8 +371,7 @@ namespace lp { e.m_c += p.coeff() * lia.lower_bound(p.var()).x; else { unsigned lj = add_var(p.var()); - while (lj >= m_e_matrix.column_count()) - m_e_matrix.add_column(); + m_e_matrix.add_columns_up_to(lj); m_e_matrix.add_new_element(entry_index, lj, p.coeff()); } } @@ -378,8 +379,7 @@ namespace lp { e.m_c -= lia.lower_bound(t.j()).x; } else { unsigned lj = add_var(t.j()); - while (lj >= m_e_matrix.column_count()) - m_e_matrix.add_column(); + m_e_matrix.add_columns_up_to(lj); m_e_matrix.add_new_element(entry_index, lj, -mpq(1)); } TRACE("dioph_eq", print_entry(entry_index, tout);); @@ -572,7 +572,7 @@ namespace lp { } m_c += coeff * e.m_c; - m_tmp_l += coeff * l_term_from_row(k); // improve later + m_tmp_l += coeff * l_term_from_row(sub_index(k)); // improve later TRACE("dioph_eq", tout << "after subs k:" << k << "\n"; print_term_o(create_term_from_ind_c(), tout) << std::endl; tout << "m_tmp_l:{"; print_lar_term_L(m_tmp_l, tout); diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 3504312b0..a4f4912c2 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -147,6 +147,8 @@ public: m_work_vector_of_row_offsets.push_back(-1); } + void add_columns_up_to(unsigned j) { while (j >= column_count()) add_column(); } + void forget_last_columns(unsigned how_many_to_forget); void remove_last_column(unsigned j);