mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

uniform choice of a beneficial column

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-07-29 22:33:19 -07:00
parent e9595eb283
commit 2de27ae3af
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/util/lp/lp_primal_core_solver.h
View file

@ -280,7 +280,8 @@ public:
if (m_bland_mode_tableau) if (m_bland_mode_tableau)
return find_beneficial_column_in_row_tableau_rows_bland_mode(i, a_ent); return find_beneficial_column_in_row_tableau_rows_bland_mode(i, a_ent);
// a short row produces short infeasibility explanation and benefits at least one pivot operation // a short row produces short infeasibility explanation and benefits at least one pivot operation
vector<const row_cell<T>*> choices; int choice = -1;
int nchoices = 0;
unsigned num_of_non_free_basics = 1000000; unsigned num_of_non_free_basics = 1000000;
unsigned len = 100000000; unsigned len = 100000000;
unsigned bj = this->m_basis[i]; unsigned bj = this->m_basis[i];
@ -302,24 +303,23 @@ public:
if (damage < num_of_non_free_basics) { if (damage < num_of_non_free_basics) {
num_of_non_free_basics = damage; num_of_non_free_basics = damage;
len = this->m_A.m_columns[j].live_size(); len = this->m_A.m_columns[j].live_size();
choices.clear(); choice = k;
choices.push_back(&rc); nchoices = 1;
} else if (damage == num_of_non_free_basics && } else if (damage == num_of_non_free_basics &&
this->m_A.m_columns[j].live_size() <= len && (this->m_settings.random_next() % 2)) { this->m_A.m_columns[j].live_size() <= len && (this->m_settings.random_next() % (++nchoices))) {
choices.push_back(&rc); choice = k;
len = this->m_A.m_columns[j].live_size(); len = this->m_A.m_columns[j].live_size();
} }
} }
if (choices.size() == 0) { if (choice == -1) {
m_inf_row_index_for_tableau = i; m_inf_row_index_for_tableau = i;
return -1; return -1;
} }
const row_cell<T>* rc = choices.size() == 1? choices[0] : const row_cell<T>& rc = this->m_A.m_rows[i].m_cells[choice];
choices[this->m_settings.random_next() % choices.size()]; a_ent = rc.coeff();
a_ent = rc->coeff(); return rc.var();
return rc->var();
} }
static X positive_infinity() { static X positive_infinity() {
return convert_struct<X, unsigned>::convert(std::numeric_limits<unsigned>::max()); return convert_struct<X, unsigned>::convert(std::numeric_limits<unsigned>::max());