From cff0e0fc6c28071fd7ae4398bc34e8bbd9f9d121 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Dec 2013 09:18:06 +0200 Subject: [PATCH] debug min_max Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_aux.h | 12 ++++++++---- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 2380f8969..a7d58080e 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -855,7 +855,7 @@ 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); + 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); void move_to_bound(theory_var x_i, bool inc); template diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index bb8e8ef77..b0d983bca 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -952,7 +952,7 @@ namespace smt { } template - theory_var theory_arith::pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain) { + theory_var theory_arith::pick_var_to_leave(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; @@ -974,10 +974,14 @@ namespace smt { if (curr_gain.is_neg()) curr_gain.neg(); if (x_i == null_theory_var || (curr_gain < gain) || (gain.is_zero() && curr_gain.is_zero() && s < x_i)) { - if (is_int(s) && !curr_gain.is_int()) + if (is_int(s) && !curr_gain.is_int()) { + skipped_row = true; continue; - if (is_int(x_j) && !curr_gain.is_int()) + } + if (is_int(x_j) && !curr_gain.is_int()) { + skipped_row = true; continue; + } x_i = s; a_ij = coeff; gain = curr_gain; @@ -1309,7 +1313,7 @@ namespace smt { skipped_row = true; continue; } - theory_var curr_x_i = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_gain); + theory_var curr_x_i = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row); if (curr_x_i == null_theory_var) { // we can increase/decrease curr_x_j as much as we want. x_i = null_theory_var; // unbounded