From 32762b54a74f22113084bcb0269546df3a212297 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2013 07:50:25 -0800 Subject: [PATCH] debug looping behavior Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 4 ++-- src/smt/theory_arith_aux.h | 28 +++++++++++++++++++++------- src/smt/theory_arith_int.h | 15 +++++++++++---- 3 files changed, 34 insertions(+), 13 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index a7d58080e..ee2ce349d 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -855,8 +855,8 @@ namespace smt { row m_tmp_row; void add_tmp_row(row & r1, numeral const & coeff, row const & r2); - theory_var pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skiped_row); - bool is_safe_to_leave(theory_var x); + 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); void 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 485b68e2a..77845fee6 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 theory_arith::is_safe_to_leave(theory_var x, bool& has_int) { if (get_context().is_shared(get_enode(x))) { return false; @@ -936,14 +936,16 @@ namespace smt { column & c = m_columns[x]; typename svector::iterator it = c.begin_entries(); typename svector::iterator end = c.end_entries(); + has_int = false; for (; it != end; ++it) { if (it->is_dead()) continue; row const & r = m_rows[it->m_row_id]; theory_var s = r.get_base_var(); numeral const & coeff = r[it->m_row_idx].m_coeff; + if (s != null_theory_var && is_int(s)) has_int = true; bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int()); is_unsafe = is_unsafe || (s != null_theory_var && get_context().is_shared(get_enode(s))); - TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << "\n"; + TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << " " << (has_int?"int":"real") << "\n"; display_row(tout, r, true);); if (is_unsafe) return false; } @@ -952,7 +954,9 @@ namespace smt { } template - theory_var theory_arith::pick_var_to_leave(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; @@ -982,6 +986,10 @@ namespace smt { skipped_row = true; continue; } + if (!curr_gain.is_int() && has_int) { + skipped_row = true; + continue; + } x_i = s; a_ij = coeff; gain = curr_gain; @@ -1294,6 +1302,7 @@ namespace smt { #ifdef _TRACE unsigned i = 0; #endif + max_min_t result; while (true) { x_j = null_theory_var; x_i = null_theory_var; @@ -1307,13 +1316,14 @@ namespace smt { SASSERT(is_non_base(curr_x_j)); curr_coeff = it->m_coeff; bool curr_inc = curr_coeff.is_pos() ? max : !max; + 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)) { + if (!is_safe_to_leave(curr_x_j, has_int)) { skipped_row = true; continue; } - theory_var curr_x_i = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row); + theory_var curr_x_i = pick_var_to_leave(has_int, curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row); if (curr_x_i == null_theory_var) { TRACE("opt", tout << "unbounded\n";); // we can increase/decrease curr_x_j as much as we want. @@ -1348,7 +1358,8 @@ namespace smt { TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); - return skipped_row?BEST_EFFORT:OPTIMIZED; + result = skipped_row?BEST_EFFORT:OPTIMIZED; + break; } if (x_i == null_theory_var) { @@ -1367,7 +1378,8 @@ namespace smt { SASSERT(satisfy_bounds()); continue; } - return UNBOUNDED; + result = skipped_row?BEST_EFFORT:UNBOUNDED; + break; } if (!is_fixed(x_j) && is_bounded(x_j) && (upper_bound(x_j) - lower_bound(x_j) <= gain)) { @@ -1413,6 +1425,8 @@ namespace smt { SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); } + TRACE("opt", display(tout);); + return result; } /** diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 4fa9e75c7..4b5388062 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -33,11 +33,15 @@ namespace smt { // Integrality // // ----------------------------------- + /** \brief Move non base variables to one of its bounds. If the variable does not have bounds, it is integer, but it is not assigned to an integer value, then the variable is set to an integer value. + In mixed integer/real problems moving a real variable to a bound could cause an integer value to + have an infinitesimal. Such an assignment would disable mk_gomory_cut, and Z3 would loop. + */ template void theory_arith::move_non_base_vars_to_bounds() { @@ -413,10 +417,10 @@ namespace smt { for (; it != end; ++it) { // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed). if (!it->is_dead() && it->m_var != b && (!at_bound(it->m_var) || !get_value(it->m_var).is_rational())) { - TRACE("gomory_cut", tout << "row is gomory cut target:\n"; + TRACE("gomory_cut", tout << "row is not gomory cut target:\n"; display_var(tout, it->m_var); tout << "at_bound: " << at_bound(it->m_var) << "\n"; - tout << "infinitesimal: " << get_value(it->m_var).is_rational() << "\n";); + tout << "infinitesimal: " << !get_value(it->m_var).is_rational() << "\n";); return false; } } @@ -1378,6 +1382,7 @@ namespace smt { m_branch_cut_counter++; // TODO: add giveup code if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) { + TRACE("opt", display(tout);); move_non_base_vars_to_bounds(); if (!make_feasible()) { TRACE("arith_int", tout << "failed to move variables to bounds.\n";); @@ -1389,7 +1394,9 @@ namespace smt { TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";); SASSERT(is_base(int_var)); row const & r = m_rows[get_var_row(int_var)]; - mk_gomory_cut(r); + if (!mk_gomory_cut(r)) { + // silent failure + } return FC_CONTINUE; } } @@ -1399,7 +1406,7 @@ namespace smt { } theory_var int_var = find_infeasible_int_base_var(); if (int_var != null_theory_var) { - TRACE("arith_int", tout << "v" << int_var << " does not have and integer assignment: " << get_value(int_var) << "\n";); + TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";); // apply branching branch_infeasible_int_var(int_var); return FC_CONTINUE;