From 11010086be4beb571a4036ee4da45293c0447b2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Oct 2013 11:57:30 +0800 Subject: [PATCH] fixing bug with optimization Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 1 + src/smt/theory_arith_aux.h | 120 +++++++++++++++++++++++++++++++++---- 2 files changed, 111 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index e0e535189..8d0011ec1 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -853,6 +853,7 @@ namespace smt { 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); + void move_to_bound(theory_var x_i, bool inc); template void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); bool max_min(theory_var v, bool max); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 8d010be71..d50b1d505 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -912,6 +912,16 @@ namespace smt { If no x_i imposes a restriction on x_j, then return null_theory_var. That is, x_j is free to move to its upper bound (lower bound). + + Get the equations for x_j: + + x_i1 = coeff_1 * x_j + rest_1 + ... + x_in = coeff_n * x_j + rest_n + + gain_k := (upper_bound(x_ik) - value(x_ik))/coeff_k + + */ template theory_var theory_arith::pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain) { @@ -939,10 +949,15 @@ namespace smt { x_i = s; a_ij = coeff; gain = curr_gain; + TRACE("maximize", + tout << "x_i: v" << x_i << ", gain: " << gain << "\n"; + tout << "value(s): (" << get_value(s) << " - " << b->get_value() << ")/" << coeff << "\n"; + display_row(tout, r, true); + ); } } } - TRACE("maximize", tout << "x_j: v" << x_i << ", gain: " << gain << "\n";); + TRACE("maximize", tout << "x_i: v" << x_i << ", gain: " << gain << "\n";); } } TRACE("maximize", tout << "x_i v" << x_i << "\n";); @@ -982,7 +997,7 @@ namespace smt { theory_var x_j = null_theory_var; bool inc = false; numeral a_ij, curr_a_ij, coeff, curr_coeff; - inf_numeral curr_gain, gain; + inf_numeral gain, curr_gain; #ifdef _TRACE unsigned i = 0; #endif @@ -1071,19 +1086,45 @@ namespace smt { continue; } - TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n";); + TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; + if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; + if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; + tout << "value x_i: " << get_value(x_i) << "\n"; + if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; + if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; + tout << "value x_j: " << get_value(x_j) << "\n"; + ); + pivot(x_i, x_j, a_ij, false); + + TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; + if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; + if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; + tout << "value x_i: " << get_value(x_i) << "\n"; + if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; + if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; + tout << "value x_j: " << get_value(x_j) << "\n"; + + ); + + SASSERT(is_non_base(x_i)); + SASSERT(is_base(x_j)); + bool move_xi_to_lower; if (inc) move_xi_to_lower = a_ij.is_pos(); else move_xi_to_lower = a_ij.is_neg(); - pivot(x_i, x_j, a_ij, false); - SASSERT(is_non_base(x_i)); - SASSERT(is_base(x_j)); - if (move_xi_to_lower) - update_value(x_i, lower_bound(x_i) - get_value(x_i)); - else - update_value(x_i, upper_bound(x_i) - get_value(x_i)); + move_to_bound(x_i, move_xi_to_lower); + + TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; + if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; + if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; + tout << "value x_i: " << get_value(x_i) << "\n"; + if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; + if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; + tout << "value x_j: " << get_value(x_j) << "\n"; + ); + row & r2 = m_rows[get_var_row(x_j)]; coeff.neg(); add_tmp_row(r, coeff, r2); @@ -1093,6 +1134,65 @@ namespace smt { } } + /** + Move the variable x_i maximally towards its bound as long as + bounds of other variables are not violated. + */ + + template + void theory_arith::move_to_bound(theory_var x_i, bool move_to_lower) { + inf_numeral delta, delta_abs; + + if (move_to_lower) { + delta = lower_bound(x_i) - get_value(x_i); + SASSERT(!delta.is_pos()); + } + else { + delta = upper_bound(x_i) - get_value(x_i); + SASSERT(!delta.is_neg()); + } + + TRACE("maximize", tout << "Original delta: " << delta << "\n";); + + delta_abs = abs(delta); + // + // Decrease absolute value of delta according to bounds on rows where x_i is used. + // + column & c = m_columns[x_i]; + typename svector::iterator it = c.begin_entries(); + typename svector::iterator end = c.end_entries(); + for (; it != end && delta_abs.is_pos(); ++it) { + if (!it->is_dead()) { + row & r = m_rows[it->m_row_id]; + theory_var s = r.get_base_var(); + if (s != null_theory_var && !is_quasi_base(s)) { + numeral const & coeff = r[it->m_row_idx].m_coeff; + SASSERT(!coeff.is_zero()); + bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this.. + bound * b = get_bound(s, inc_s); + if (b) { + inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff); + if (delta2 < delta_abs) { + delta_abs = delta2; + } + } + } + } + } + + + if (move_to_lower) { + delta = -delta_abs; + } + else { + delta = delta_abs; + } + + TRACE("maximize", tout << "Safe delta: " << delta << "\n";); + + update_value(x_i, delta); + } + /** \brief Add an entry to a temporary row.