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

cancel bugs fixes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-11-17 19:54:52 -08:00 committed by Lev Nachmanson
parent e4f3b5753f
commit c300843585
1 changed files with 20 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/math/lp/dioph_eq.cpp
View file

@ -771,6 +771,7 @@ namespace lp {
if ((int)st >= (int)lp::lp_status::FEASIBLE) { if ((int)st >= (int)lp::lp_status::FEASIBLE) {
return false; return false;
} }
if (st == lp_status::CANCELLED) return false;
lra.get_infeasibility_explanation(m_infeas_explanation); lra.get_infeasibility_explanation(m_infeas_explanation);
return true; return true;
} }
@ -846,7 +847,6 @@ namespace lp {
// returns true if the left and the right branches were explored // returns true if the left and the right branches were explored
bool undo_last_branch() { bool undo_last_branch() {
unsigned h = m_branch_stack.size() - 1;
if (m_branch_stack.back().m_fully_explored) { if (m_branch_stack.back().m_fully_explored) {
TRACE("dio_br", tout << "pop fully explored, m_branch_stack.size():" << m_branch_stack.size() << std::endl;); TRACE("dio_br", tout << "pop fully explored, m_branch_stack.size():" << m_branch_stack.size() << std::endl;);
m_branch_stack.pop_back(); m_branch_stack.pop_back();
@ -905,7 +905,7 @@ namespace lp {
lra.pop(); lra.pop();
} }
lra.find_feasible_solution(); lra.find_feasible_solution();
SASSERT(lra.is_feasible()); SASSERT(lra.get_status() == lp_status::CANCELLED || lra.is_feasible());
} }
// Returns true if a branch is created, and false if not. // Returns true if a branch is created, and false if not.
// The latter case can happen if we have a sat. // The latter case can happen if we have a sat.
@ -940,7 +940,7 @@ namespace lp {
m_lra_level--; m_lra_level--;
lra.pop(); lra.pop();
lra.find_feasible_solution(); lra.find_feasible_solution();
SASSERT(lra.is_feasible()); SASSERT(lra.get_status() == lp_status::CANCELLED || lra.is_feasible());
} }
lia_move process_undef() { lia_move process_undef() {
@ -970,8 +970,8 @@ namespace lp {
lra_pop(); lra_pop();
continue; continue;
} }
int st = static_cast<int>(lra.find_feasible_solution()); auto st = lra.find_feasible_solution();
if (st >= static_cast<int>(lp_status::FEASIBLE)) { if ((int)st >= (int)(lp_status::FEASIBLE)) {
// have a feasible solution // have a feasible solution
unsigned n_of_ii = get_number_of_int_inf(); unsigned n_of_ii = get_number_of_int_inf();
TRACE("dio_br", tout << "n_of_ii:" << n_of_ii << "\n";); TRACE("dio_br", tout << "n_of_ii:" << n_of_ii << "\n";);
@ -982,7 +982,8 @@ namespace lp {
// got to create a new branch // got to create a new branch
update_branch_stats(*b, n_of_ii); update_branch_stats(*b, n_of_ii);
need_create_branch = true; need_create_branch = true;
} else { // got a conflict } else {
if (st == lp_status::CANCELLED) return lia_move::undef;
collect_evidence(); collect_evidence();
if (m_branch_stack.size() == 0) if (m_branch_stack.size() == 0)
return lia_move::conflict; return lia_move::conflict;
@ -1023,6 +1024,7 @@ namespace lp {
m_branch_stats[b.m_j].m_ii_after_right.push_back(n_of_ii); m_branch_stats[b.m_j].m_ii_after_right.push_back(n_of_ii);
} }
} }
branch create_branch() { branch create_branch() {
unsigned bj = UINT_MAX; unsigned bj = UINT_MAX;
@ -1040,17 +1042,18 @@ namespace lp {
} }
} }
branch br; branch br;
if (bj == UINT_MAX) { // it a the case when we cannot create a branch if (bj == UINT_MAX) { // it the case when we cannot create a branch
SASSERT(lra.is_feasible() && SASSERT(
[&]() { lra.settings().get_cancel_flag() ||
for (unsigned j = 0; j < lra.column_count(); ++j) { (lra.is_feasible() && [&]() {
if (lia.column_is_int_inf(j)) { for (unsigned j = 0; j < lra.column_count(); ++j) {
return false; if (lia.column_is_int_inf(j)) {
} return false;
} }
return true; }
}()); return true;
return br; // to signal that we have no ii variables }()));
return br; // to signal that we have no ii variables
} }
br.m_j = bj; br.m_j = bj;