mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

work on incremental dio

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-12-24 07:32:49 -10:00 committed by Lev Nachmanson
parent 28556ce625
commit 57b665d075
2 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/dioph_eq.cpp
View file

@ -358,6 +358,8 @@ namespace lp {
SASSERT(m_l_matrix.row_count() == m_e_matrix.row_count()); SASSERT(m_l_matrix.row_count() == m_e_matrix.row_count());
// fill m_l_matrix row // fill m_l_matrix row
m_l_matrix.add_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)); m_l_matrix.add_new_element(entry_index, t.j(), mpq(1));
// fill E-entry // fill E-entry
m_e_matrix.add_row(); m_e_matrix.add_row();
@ -369,8 +371,7 @@ namespace lp {
e.m_c += p.coeff() * lia.lower_bound(p.var()).x; e.m_c += p.coeff() * lia.lower_bound(p.var()).x;
else { else {
unsigned lj = add_var(p.var()); unsigned lj = add_var(p.var());
while (lj >= m_e_matrix.column_count()) m_e_matrix.add_columns_up_to(lj);
m_e_matrix.add_column();
m_e_matrix.add_new_element(entry_index, lj, p.coeff()); 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; e.m_c -= lia.lower_bound(t.j()).x;
} else { } else {
unsigned lj = add_var(t.j()); unsigned lj = add_var(t.j());
while (lj >= m_e_matrix.column_count()) m_e_matrix.add_columns_up_to(lj);
m_e_matrix.add_column();
m_e_matrix.add_new_element(entry_index, lj, -mpq(1)); m_e_matrix.add_new_element(entry_index, lj, -mpq(1));
} }
TRACE("dioph_eq", print_entry(entry_index, tout);); TRACE("dioph_eq", print_entry(entry_index, tout););
@ -572,7 +572,7 @@ namespace lp {
} }
m_c += coeff * e.m_c; 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"; TRACE("dioph_eq", tout << "after subs k:" << k << "\n";
print_term_o(create_term_from_ind_c(), tout) << std::endl; print_term_o(create_term_from_ind_c(), tout) << std::endl;
tout << "m_tmp_l:{"; print_lar_term_L(m_tmp_l, tout); tout << "m_tmp_l:{"; print_lar_term_L(m_tmp_l, tout);

2
src/math/lp/static_matrix.h
View file

@ -147,6 +147,8 @@ public:
m_work_vector_of_row_offsets.push_back(-1); 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 forget_last_columns(unsigned how_many_to_forget);
void remove_last_column(unsigned j); void remove_last_column(unsigned j);