From 52c6f7c3b10cefb33b624cfbfb5d0fc79c965502 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jan 2015 15:22:40 -0800 Subject: [PATCH] refine the safety check for leaving basis. As long as all base variables are unbounded in compatible directions as the non-basic variable we can detect unbounded variables. This partial check fixes integer divergence in a case exposed by Karpenov. Establishing or converting this to a check that always identifies unbounded integer variables is left for further analysis. Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_aux.h | 21 +++++++++++++-------- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 5936ca3d3..99a36c463 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -874,7 +874,7 @@ namespace smt { void add_tmp_row(row & r1, numeral const & coeff, row const & r2); theory_var pick_var_to_leave(bool has_int, theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skiped_row); - bool is_safe_to_leave(theory_var x, bool& has_int, bool& is_shared); + bool is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& is_shared); bool move_to_bound(theory_var x_i, bool inc); template void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 30c92feea..d377fb7ad 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -928,7 +928,7 @@ namespace smt { */ template - bool theory_arith::is_safe_to_leave(theory_var x, bool& has_int, bool& shared) { + bool theory_arith::is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& shared) { context& ctx = get_context(); shared |= ctx.is_shared(get_enode(x)); @@ -936,6 +936,8 @@ namespace smt { typename svector::iterator it = c.begin_entries(); typename svector::iterator end = c.end_entries(); has_int = false; + bool unbounded = (inc && !upper(x)) || (!inc && !lower(x)); + bool was_unsafe = false; for (; it != end; ++it) { if (it->is_dead()) continue; row const & r = m_rows[it->m_row_id]; @@ -944,19 +946,22 @@ namespace smt { if (s != null_theory_var && is_int(s)) has_int = true; bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int()); shared |= (s != null_theory_var && ctx.is_shared(get_enode(s))); + was_unsafe |= is_unsafe; + bool inc_s = coeff.is_neg() ? inc : !inc; + unbounded &= !get_bound(s, inc_s); TRACE("opt", tout << "is v" << x << " safe to leave for v" << s - << "? " << (is_unsafe?"no":"yes") << " " << (has_int?"int":"real") << "\n"; + << "? " << (is_unsafe?"no":"yes") << " " << (has_int?"int":"real") << " " << (unbounded?"unbounded":"bounded") << "\n"; display_row(tout, r, true);); - if (is_unsafe) return false; + if (was_unsafe && !unbounded) return false; } - return true; + return !was_unsafe || unbounded; } template - theory_var theory_arith::pick_var_to_leave( - bool has_int, theory_var x_j, bool inc, - numeral & a_ij, inf_numeral & gain, bool& skipped_row) { + theory_var theory_arith::pick_var_to_leave( + bool has_int, theory_var x_j, bool inc, + numeral & a_ij, inf_numeral & gain, bool& skipped_row) { TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";); theory_var x_i = null_theory_var; inf_numeral curr_gain; @@ -1335,7 +1340,7 @@ namespace smt { bool has_int = false; if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) continue; // variable cannot be used for max/min. - if (!is_safe_to_leave(curr_x_j, has_int, has_shared)) { + if (!is_safe_to_leave(curr_x_j, curr_inc, has_int, has_shared)) { skipped_row = true; continue; }