mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

correctly process cancellation in gomory cuts

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-09-19 14:11:27 -07:00
parent b99c4a47a4
commit 342dccdc02
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -527,7 +527,7 @@ public:
has_small_cut = true; has_small_cut = true;
add_cut(cc.m_t, cc.m_k, cc.m_dep); add_cut(cc.m_t, cc.m_k, cc.m_dep);
if (lia.settings().get_cancel_flag()) if (lia.settings().get_cancel_flag())
return lia_move::undef; return lia_move::cancelled;
} }
if (big_cuts.size()) { if (big_cuts.size()) {
@ -544,6 +544,9 @@ public:
if (!_check_feasible()) if (!_check_feasible())
return lia_move::conflict; return lia_move::conflict;
if (lra.get_status() == lp_status::CANCELLED)
return lia_move::cancelled;
if (!lia.has_inf_int()) if (!lia.has_inf_int())
return lia_move::sat; return lia_move::sat;

3
src/math/lp/lia_move.h
View file

@ -26,7 +26,8 @@ namespace lp {
conflict, conflict,
continue_with_check, continue_with_check,
undef, undef,
unsat unsat,
cancelled
}; };
inline std::string lia_move_to_string(lia_move m) { inline std::string lia_move_to_string(lia_move m) {
switch (m) { switch (m) {