mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

branch of an int inf base if the row is not a gomory target

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-14 11:07:14 -07:00 • committed by Lev Nachmanson
parent 0be5fc5693
commit 11d37d97a1
1 changed files with 0 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -140,16 +140,6 @@ lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row
return gc.create_cut(); return gc.create_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) { 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)); const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));