From ffa78b95ab347ce3410ffeba4b5c0d9f828d1917 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Oct 2015 14:38:47 -0700 Subject: [PATCH 1/3] fix unbounded, issue #252 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index bad141e94..532152100 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1530,6 +1530,7 @@ namespace smt { while (best_efforts < max_efforts && !ctx.get_cancel_flag()) { theory_var x_j = null_theory_var; theory_var x_i = null_theory_var; + unsigned has_bound = false; max_gain.reset(); min_gain.reset(); ++round; @@ -1538,7 +1539,7 @@ namespace smt { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); for (; it != end; ++it) { - if (it->is_dead()) continue; + if (it->is_dead()) continue; theory_var curr_x_j = it->m_var; theory_var curr_x_i = null_theory_var; SASSERT(is_non_base(curr_x_j)); @@ -1546,6 +1547,7 @@ namespace smt { bool curr_inc = curr_coeff.is_pos() ? max : !max; if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) { // variable cannot be used for max/min. + has_bound = true; continue; } bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, @@ -1593,10 +1595,10 @@ namespace smt { TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n"; tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";); - if (x_j == null_theory_var && x_i == null_theory_var) { + if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) { has_shared = false; best_efforts = 0; - result = UNBOUNDED; + result = UNBOUNDED; break; } From ac902dad1a1022a3762320e321c4b2f696a8dbd0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Oct 2015 08:53:12 -0700 Subject: [PATCH 2/3] fix another regression and missing detection of bounds, Issue #254 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 532152100..1f729d7b5 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1530,7 +1530,7 @@ namespace smt { while (best_efforts < max_efforts && !ctx.get_cancel_flag()) { theory_var x_j = null_theory_var; theory_var x_i = null_theory_var; - unsigned has_bound = false; + bool has_bound = false; max_gain.reset(); min_gain.reset(); ++round; @@ -1544,10 +1544,12 @@ namespace smt { theory_var curr_x_i = null_theory_var; SASSERT(is_non_base(curr_x_j)); curr_coeff = it->m_coeff; - bool curr_inc = curr_coeff.is_pos() ? max : !max; + bool curr_inc = curr_coeff.is_pos() ? max : !max; + if ((curr_inc && upper(curr_x_j)) || (!curr_inc && lower(curr_x_j))) { + has_bound = true; + } if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) { // variable cannot be used for max/min. - has_bound = true; continue; } bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, @@ -1557,7 +1559,7 @@ namespace smt { SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain)); - if (!picked_var) { // && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain)) + if (!safe_gain(curr_min_gain, curr_max_gain)) { TRACE("opt", tout << "no variable picked\n";); best_efforts++; } From 05c6ed16982a88d2c87694d8ad709c989248b620 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Oct 2015 09:54:05 -0700 Subject: [PATCH 3/3] fixing issue #254 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 1f729d7b5..45654310f 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1561,6 +1561,7 @@ namespace smt { if (!safe_gain(curr_min_gain, curr_max_gain)) { TRACE("opt", tout << "no variable picked\n";); + has_bound = true; best_efforts++; } else if (curr_x_i == null_theory_var) {