mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

return conflict on an empty term in Gomory cuts

Browse source
This commit is contained in:
Lev Nachmanson 2024-01-03 18:56:35 -10:00
parent b75367ffc7
commit 239d68ed9c
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/gomory.cpp
View file

@ -538,8 +538,11 @@ public:
create_cut cc(lia.m_t, lia.m_k, lia.m_ex, j, row, lia); create_cut cc(lia.m_t, lia.m_k, lia.m_ex, j, row, lia);
auto r = cc.cut(); auto r = cc.cut();
if (r != lia_move::cut) if (r != lia_move::cut) {
if (r == lia_move::conflict)
return lia_move::conflict;
continue; continue;
}
cut_result cr = {cc.m_dep, lia.m_t, lia.m_k, cc.m_polarity, j}; cut_result cr = {cc.m_dep, lia.m_t, lia.m_k, cc.m_polarity, j};
if (abs(cr.polarity) == 1) // need to delay the update of the bounds for j in a polar case, because simplify_inequality relies on the old bounds if (abs(cr.polarity) == 1) // need to delay the update of the bounds for j in a polar case, because simplify_inequality relies on the old bounds
polar_vars.push_back( {j, cr.polarity, cc.m_dep} ); polar_vars.push_back( {j, cr.polarity, cc.m_dep} );