mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 07:24:40 +00:00
Code Activity

branch on inf basic in gomory

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-13 11:38:22 -07:00
parent 78950fde17
commit e705e5a309
3 changed files with 49 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/util/lp/int_solver.cpp
View file

@ -102,6 +102,8 @@ bool int_solver::is_gomory_cut_target(const row_strip<mpq>& row) {
for (const auto & p : row) {
j = p.var();
if (is_base(j)) continue;
if (is_free(j))
return false;
if (!at_bound(j))
return false;
if (!is_zero(get_value(j).y)) {
@ -350,24 +352,11 @@ lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row
return lia_move::cut;
}
int int_solver::find_free_var_in_gomory_row(const row_strip<mpq>& row) {
unsigned j;
for (const auto & p : row) {
j = p.var();
if (!is_base(j) && is_free(j))
return static_cast<int>(j);
}
return -1;
}
lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
if (-1 != find_free_var_in_gomory_row(row))
return lia_move::undef;
if (!is_gomory_cut_target(row))
return lia_move::undef;
return create_branch_on_column(j);
*m_upper = true;
return mk_gomory_cut(j, row);