work on incremental dio

Signed-off-by: Lev Nachmanson <[email protected]>
Z3Prover · Feb 11, 2025 · 57b665d · 57b665d
1 parent 28556ce
commit 57b665d
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git 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,17 +371,15 @@ 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());
                 }
             }
             if (is_fixed(t.j())) {
                 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
@@ -147,6 +147,8 @@ class static_matrix
         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);