mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix a bug in dio

Browse source
This commit is contained in:
Lev Nachmanson 2024-12-20 12:37:07 -10:00 • committed by Lev Nachmanson
parent b0383da8f2
commit 7ecac27335
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -233,7 +233,9 @@ namespace lp {
// {coeff*lar.get_term(k)})
std_vector<unsigned> m_k2s;
std_vector<unsigned> m_fresh_definitions;
std_vector<unsigned> m_fresh_definitions; // seems only needed in the debug
// version in remove_fresh_vars
unsigned m_conflict_index = -1; // m_entries[m_conflict_index] gives the conflict
unsigned m_max_number_of_iterations = 100;
unsigned m_number_of_iterations;
@ -302,7 +304,7 @@ namespace lp {
void fill_entry(const lar_term& t) {
TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;);
entry te = {lar_term(t.j()), mpq(0), entry_status::F};
unsigned entry_index = (unsigned)m_entries.size();
unsigned entry_index = m_entries.size();
m_f.push_back(entry_index);
m_entries.push_back(te);
entry& e = m_entries.back();
@ -926,10 +928,11 @@ namespace lp {
}
TRACE("dio_br", lra.print_column_info(b.m_j, tout) <<"add bound" << std::endl;);
if (lra.column_is_fixed(b.m_j)) {
unsigned local_b_mj;
if (!m_var_register.external_is_used(b.m_j, local_b_mj))
unsigned local_mj;
if (! m_var_register.external_is_used(b.m_j, local_mj))
return lia_move::undef;
if (fix_var(local_b_mj) == lia_move::conflict) {
if (fix_var(lar_solver_to_local(b.m_j)) == lia_move::conflict) {
TRACE("dio_br", tout << "conflict in fix_var" << std::endl;) ;
return lia_move::conflict;
}
@ -1025,7 +1028,7 @@ namespace lp {
}
unsigned get_number_of_int_inf() const {
return (unsigned)std::count_if(
return std::count_if(
lra.r_basis().begin(), lra.r_basis().end(),
[this](unsigned j) {
return lia.column_is_int_inf(j);
@ -1166,7 +1169,7 @@ namespace lp {
[ei](const auto& cell) {
return cell.var() == ei;
});
unsigned pivot_col_cell_index = (unsigned) std::distance(column.begin(), it);
unsigned pivot_col_cell_index = std::distance(column.begin(), it);
if (pivot_col_cell_index != 0) {
// swap the pivot column cell with the head cell
auto c = column[0];
@ -1329,7 +1332,7 @@ namespace lp {
m_e_matrix.add_new_element(fresh_row, i, q);
}
m_k2s.resize(k + 1, -1);
m_k2s.resize(std::max(k + 1, xt + 1), -1);
m_k2s[k] = fresh_row;
m_fresh_definitions.resize(xt + 1, -1);
m_fresh_definitions[xt] = fresh_row;