From d45c7ce0824d9516ba1111fa056ae1a16ca589f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Jan 2015 04:11:40 +0530 Subject: [PATCH] prepare revised primal phase Signed-off-by: Nikolaj Bjorner --- src/smt/old_interval.cpp | 8 +- src/smt/theory_arith.h | 20 +- src/smt/theory_arith_aux.h | 426 +++++++++++++++++++++++++++++-------- src/smt/theory_arith_inv.h | 9 + src/smt/theory_arith_nl.h | 17 +- src/smt/theory_arith_pp.h | 27 ++- 6 files changed, 411 insertions(+), 96 deletions(-) diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index ffc3331be..616b74ed6 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -72,7 +72,11 @@ ext_numeral & ext_numeral::operator-=(ext_numeral const & other) { } ext_numeral & ext_numeral::operator*=(ext_numeral const & other) { - if (is_zero() || other.is_zero()) { + if (is_zero()) { + m_kind = FINITE; + return *this; + } + if (other.is_zero()) { m_kind = FINITE; m_value.reset(); return *this; @@ -295,6 +299,8 @@ interval & interval::operator*=(interval const & other) { } if (other.is_zero()) { *this = other; + m_lower_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); + m_upper_dep = m_lower_dep; return *this; } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index ffdc82f86..cba6bf662 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -265,6 +265,7 @@ namespace smt { inf_numeral const & get_value() const { return m_value; } virtual bool has_justification() const { return false; } virtual void push_justification(antecedents& antecedents, numeral const& coeff, bool proofs_enabled) {} + virtual void display(theory_arith const& th, std::ostream& out) const; }; @@ -291,6 +292,7 @@ namespace smt { virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { a.push_lit(literal(get_bool_var(), !m_is_true), coeff, proofs_enabled); } + virtual void display(theory_arith const& th, std::ostream& out) const; }; class eq_bound : public bound { @@ -309,6 +311,7 @@ namespace smt { SASSERT(m_lhs->get_root() == m_rhs->get_root()); a.push_eq(enode_pair(m_lhs, m_rhs), coeff, proofs_enabled); } + virtual void display(theory_arith const& th, std::ostream& out) const; }; class derived_bound : public bound { @@ -323,6 +326,7 @@ namespace smt { virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled); virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); } virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); } + virtual void display(theory_arith const& th, std::ostream& out) const; }; class justified_derived_bound : public derived_bound { @@ -883,7 +887,18 @@ namespace smt { max_min_t max_min(row & r, bool max, bool& has_shared); bool max_min(svector const & vars); - // max_min_t max_min_new(theory_var v, bool max, bool& has_shared); + max_min_t max_min_new(row& r, bool max, bool& has_shared); + bool unbounded_gain(inf_numeral const & max_gain) const; + bool safe_gain(inf_numeral const& min_gain, inf_numeral const & max_gain) const; + void normalize_gain(numeral const& divisor, inf_numeral & max_gain) const; + void init_gains(theory_var x, bool inc, inf_numeral& min_gain, inf_numeral& max_gain); + bool update_gains(bool inc, theory_var x_i, numeral const& a_ij, + inf_numeral& min_gain, inf_numeral& max_gain); + bool move_to_bound_new(theory_var x_i, bool inc, bool& best_effort, bool& has_shared); + bool pick_var_to_leave( + theory_var x_j, bool inc, numeral & a_ij, + inf_numeral& min_gain, inf_numeral& max_gain, + bool& shared, theory_var& x_i); // ----------------------------------- // @@ -1064,6 +1079,8 @@ namespace smt { void display_bounds_in_smtlib() const; void display_nl_monomials(std::ostream & out) const; void display_coeff_exprs(std::ostream & out, sbuffer const & p) const; + void display_interval(std::ostream& out, interval const& i); + void display_deps(std::ostream& out, v_dependency* dep); protected: // ----------------------------------- @@ -1079,6 +1096,7 @@ namespace smt { bool wf_rows() const; bool wf_column(theory_var v) const; bool wf_columns() const; + bool valid_assignment() const; bool valid_row_assignment() const; bool valid_row_assignment(row const & r) const; bool satisfy_bounds() const; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index f4d908a5c..7930dbec2 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -363,6 +363,19 @@ namespace smt { return m_params.c_ptr(); } + // ----------------------------------- + // + // Bounds + // + // ----------------------------------- + + + template + void theory_arith::bound::display(theory_arith const& th, std::ostream& out) const { + out << "v" << m_var << " " << get_bound_kind() << " " << get_value(); + } + + // ----------------------------------- // // Atoms @@ -401,6 +414,27 @@ namespace smt { } } + template + void theory_arith::atom::display(theory_arith const& th, std::ostream& out) const { + literal l(get_bool_var(), !m_is_true); + out << "v" << m_var << " " << get_bound_kind() << " " << get_k() << " "; + out << l << ":"; + th.get_context().display_detailed_literal(out, l); + } + + // ----------------------------------- + // + // eq_bound + // + // ----------------------------------- + + template + void theory_arith::eq_bound::display(theory_arith const& th, std::ostream& out) const { + ast_manager& m = th.get_manager(); + out << "#" << m_lhs->get_owner_id() << " " << mk_pp(m_lhs->get_owner(), m) << " = " + << "#" << m_rhs->get_owner_id() << " " << mk_pp(m_rhs->get_owner(), m); + } + // ----------------------------------- // // Auxiliary methods @@ -711,6 +745,24 @@ namespace smt { } } + template + void theory_arith::derived_bound::display(theory_arith const& th, std::ostream& out) const { + out << "v" << m_var << " " << get_bound_kind() << " " << get_value(); + + ast_manager& m = th.get_manager(); + for (unsigned i = 0; i < m_eqs.size(); ++i) { + enode* a = m_eqs[i].first; + enode* b = m_eqs[i].second; + out << " "; + out << "#" << a->get_owner_id() << " " << mk_pp(a->get_owner(), m) << " = " + << "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m); + } + for (unsigned i = 0; i < m_lits.size(); ++i) { + literal l = m_lits[i]; + out << " " << l << ":"; th.get_context().display_detailed_literal(out, l); + } + } + template void theory_arith::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { @@ -1313,8 +1365,8 @@ namespace smt { bool skipped_row = false; has_shared = false; - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); + SASSERT(valid_assignment()); + theory_var x_i = null_theory_var; theory_var x_j = null_theory_var; @@ -1379,8 +1431,7 @@ namespace smt { if (x_j == null_theory_var) { TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); + SASSERT(valid_assignment()); result = skipped_row?BEST_EFFORT:OPTIMIZED; break; } @@ -1390,17 +1441,13 @@ namespace smt { if (inc && upper(x_j) && !skipped_row) { update_value(x_j, upper_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); continue; } if (!inc && lower(x_j) && !skipped_row) { update_value(x_j, lower_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); continue; } result = skipped_row?BEST_EFFORT:UNBOUNDED; @@ -1417,9 +1464,7 @@ namespace smt { update_value(x_j, lower_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); } - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); continue; } @@ -1451,134 +1496,313 @@ namespace smt { coeff.neg(); add_tmp_row(r, coeff, r2); SASSERT(r.get_idx_of(x_j) == -1); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); } TRACE("opt", display(tout);); return result; } -#if 0 + /** + \brief Select tightest variable x_i to pivot with x_j. The goal + is to select a x_i such that the value of x_j is increased + (decreased) if inc = true (inc = false), and the tableau + remains feasible. Store the gain in x_j of the pivoting + operation in 'gain'. Note the gain can be too much. That is, + it may make x_i infeasible. In this case, instead of pivoting + we move x_j to its upper bound (lower bound) when inc = true (inc = false). + + 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 + bool theory_arith::pick_var_to_leave( + theory_var x_j, // non-base variable to increment/decrement + bool inc, + numeral & a_ij, // coefficient of x_i + inf_numeral& min_gain, // minimal required gain on x_j (integral value on integers) + inf_numeral& max_gain, // maximal possible gain on x_j + bool& has_shared, // determine if pivot involves shared variable + theory_var& x_i) { // base variable to pivot with x_j + + + context& ctx = get_context(); + column & c = m_columns[x_j]; + typename svector::iterator it = c.begin_entries(); + typename svector::iterator end = c.end_entries(); + init_gains(x_j, inc, min_gain, max_gain); + has_shared |= ctx.is_shared(get_enode(x_j)); + 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_ij = r[it->m_row_idx].m_coeff; + if (update_gains(inc, s, coeff_ij, min_gain, max_gain)) { + x_i = s; + } + has_shared |= ctx.is_shared(get_enode(s)); + } + if (safe_gain(min_gain, max_gain)) { + SASSERT(unbounded_gain(max_gain) == (x_i != null_theory_var)); + return true; + } + else { + return false; + } + } + + template + bool theory_arith::unbounded_gain(inf_numeral const & max_gain) const { + return max_gain.is_minus_one(); + } + + /* + A gain is 'safe' with respect to the tableau if: + - the selected variable is unbounded and every base variable where it occurs is unbounded + in the direction of the gain. max_gain == -1 is used to indicate unbounded variables. + - the selected variable is a rational (min_gain == -1, max_gain >= 0). + - + */ + template + bool theory_arith::safe_gain(inf_numeral const& min_gain, inf_numeral const & max_gain) const { + return + unbounded_gain(max_gain) || + min_gain <= max_gain; + } + + /** + \brief ensure that maximal gain is divisible by divisor. + */ + template + void theory_arith::normalize_gain(numeral const& divisor, inf_numeral & max_gain) const { + SASSERT(divisor.is_int()); + SASSERT(divisor.is_pos()); + if (!divisor.is_one()) { + max_gain = floor(max_gain/divisor)*divisor; + } + } + + /** + \brief initialize gains for x_j based on the bounds for x_j. + */ + template + void theory_arith::init_gains( + theory_var x, // non-base variable to increment/decrement + bool inc, + inf_numeral& min_gain, // min value to increment, -1 if rational + inf_numeral& max_gain) { // max value to decrement, -1 if unbounded + min_gain = -inf_numeral::one(); + max_gain = -inf_numeral::one(); + if (inc && upper(x)) { + max_gain = upper_bound(x) - get_value(x); + } + else if (!inc && lower(x)) { + max_gain = get_value(x) - lower_bound(x); + } + if (is_int(x)) { + min_gain = inf_numeral::one(); + } + SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); + SASSERT(min_gain.is_minus_one() || min_gain.is_one()); + SASSERT(!is_int(x) || max_gain.is_int()); + SASSERT(is_int(x) == min_gain.is_one()); + } + + template + bool theory_arith::update_gains( + bool inc, // increment/decrement x_j + theory_var x_i, // potential base variable to pivot + numeral const& a_ij, // coefficient of x_j in row where x_i is base. + inf_numeral& min_gain, // min value to increment, -1 if rational + inf_numeral& max_gain) { // max value to decrement, -1 if unbounded + + // x_i = row + a_ij*x_j + // a_ij > 0, inc -> decrement x_i + // a_ij < 0, !inc -> decrement x_i + // a_ij denominator + + if (!safe_gain(min_gain, max_gain)) return false; + + inf_numeral max_inc = inf_numeral::minus_one(); + bool decrement_x_i = (inc && a_ij.is_pos()) || (!inc && a_ij.is_neg()); + if (decrement_x_i && lower(x_i)) { + max_inc = abs((get_value(x_i) - lower_bound(x_i))/a_ij); + } + else if (!decrement_x_i && upper(x_i)) { + max_inc = abs((upper_bound(x_i) - get_value(x_i))/a_ij); + } + numeral den_aij(1); + bool is_tighter = false; + if (is_int(x_i)) den_aij = denominator(a_ij); + SASSERT(den_aij.is_pos() && den_aij.is_int()); + if (!max_inc.is_minus_one()) { + if (is_int(x_i)) { + normalize_gain(den_aij, max_inc); + } + if (unbounded_gain(max_gain)) { + max_gain = max_inc; + is_tighter = true; + } + else if (max_gain > max_inc) { + max_gain = max_inc; + is_tighter = true; + } + } + if (is_int(x_i)) { + SASSERT(min_gain.is_pos()); + if (!den_aij.is_one()) { + min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij)); + normalize_gain(den_aij, max_gain); + } + } + SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); + SASSERT(min_gain.is_minus_one() || !min_gain.is_neg()); + SASSERT(!is_int(x_i) || min_gain.is_pos()); + SASSERT(!is_int(x_i) || min_gain.is_int()); + SASSERT(!is_int(x_i) || max_gain.is_int()); + return is_tighter; + } + /** \brief Maximize (Minimize) the given temporary row. Return true if succeeded. */ template - typename theory_arith::max_min_t theory_arith::max_min_new(row & r, bool max, bool& has_shared) { + typename theory_arith::max_min_t theory_arith::max_min_new( + row & r, + bool max, + bool& has_shared) { TRACE("max_min", tout << "max_min...\n";); m_stats.m_max_min++; - bool skipped_row = false; - has_shared = false; + bool best_effort = false, inc = false; - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); + SASSERT(valid_assignment()); - theory_var x_i = null_theory_var; - theory_var x_j = null_theory_var; - bool inc = false; numeral a_ij, curr_a_ij, coeff, curr_coeff; - inf_numeral gain, curr_gain; + inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain; #ifdef _TRACE - unsigned i = 0; + unsigned round = 0; #endif - max_min_t result = BEST_EFFORT; + max_min_t result = OPTIMIZED; + has_shared = false; while (true) { - x_j = null_theory_var; - x_i = null_theory_var; - gain.reset(); - TRACE("opt", tout << "i: " << i << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout); i++;); + theory_var x_j = null_theory_var; + theory_var x_i = null_theory_var; + max_gain.reset(); + min_gain.reset(); + TRACE("opt", tout << "round: " << (round++) << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout);); 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; theory_var curr_x_j = it->m_var; + 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 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, curr_inc, has_int, has_shared)) { - skipped_row = true; + 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. + continue; + } + if (!pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, + curr_min_gain, curr_max_gain, + has_shared, curr_x_i)) { + best_effort = true; continue; } - theory_var curr_x_i = pick_var_to_leave(has_int, curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row); + SASSERT(safe_gain(curr_min_gain, curr_max_gain)); if (curr_x_i == null_theory_var) { TRACE("opt", tout << "unbounded\n";); // we can increase/decrease curr_x_j as much as we want. x_i = null_theory_var; // unbounded x_j = curr_x_j; inc = curr_inc; + min_gain = curr_min_gain; + max_gain = curr_max_gain; break; } - else if (curr_gain > gain) { + else if (curr_max_gain > max_gain) { x_i = curr_x_i; x_j = curr_x_j; a_ij = curr_a_ij; coeff = curr_coeff; - gain = curr_gain; + max_gain = curr_max_gain; + min_gain = curr_min_gain; inc = curr_inc; } - else if (curr_gain.is_zero() && (x_i == null_theory_var || curr_x_i < x_i)) { + else if (curr_max_gain.is_zero() && (x_i == null_theory_var || curr_x_i < x_i)) { x_i = curr_x_i; x_j = curr_x_j; a_ij = curr_a_ij; coeff = curr_coeff; - gain = curr_gain; + max_gain = curr_max_gain; + min_gain = curr_min_gain; inc = curr_inc; // continue } } - TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n"; - tout << "skipped row: " << (skipped_row?"yes":"no") << "\n"; + TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n"; + tout << "skipped row: " << (best_effort?"yes":"no") << "\n"; display(tout);); if (x_j == null_theory_var) { TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - result = skipped_row?BEST_EFFORT:OPTIMIZED; + SASSERT(valid_assignment()); + result = OPTIMIZED; break; } + if (min_gain.is_pos() && !min_gain.is_one()) { + best_effort = true; + } if (x_i == null_theory_var) { // can increase/decrease x_j as much as we want. - if (inc && upper(x_j) && !skipped_row) { - update_value(x_j, upper_bound(x_j) - get_value(x_j)); + + if (inc && upper(x_j)) { + SASSERT(!unbounded_gain(max_gain)); + update_value(x_j, max_gain); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); continue; } - if (!inc && lower(x_j) && !skipped_row) { - update_value(x_j, lower_bound(x_j) - get_value(x_j)); + if (!inc && lower(x_j)) { + SASSERT(!unbounded_gain(max_gain)); + max_gain.neg(); + update_value(x_j, max_gain); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); continue; } - result = skipped_row?BEST_EFFORT:UNBOUNDED; + SASSERT(unbounded_gain(max_gain)); + best_effort = false; + result = UNBOUNDED; break; } - if (!is_fixed(x_j) && is_bounded(x_j) && !skipped_row && (upper_bound(x_j) - lower_bound(x_j) <= gain)) { + if (!is_fixed(x_j) && is_bounded(x_j) && + (upper_bound(x_j) - lower_bound(x_j) == max_gain)) { // can increase/decrease x_j up to upper/lower bound. if (inc) { - update_value(x_j, upper_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); } else { - update_value(x_j, lower_bound(x_j) - get_value(x_j)); + max_gain.neg(); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); } - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + update_value(x_j, max_gain); + SASSERT(valid_assignment()); continue; } @@ -1591,33 +1815,66 @@ namespace smt { tout << "value x_j: " << get_value(x_j) << "\n"; ); pivot(x_i, x_j, a_ij, false); - - + 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(); - if (!move_to_bound(x_i, move_xi_to_lower)) { - result = BEST_EFFORT; + bool inc_xi = inc?a_ij.is_neg():a_ij.is_pos(); + if (!move_to_bound_new(x_i, inc_xi, best_effort, has_shared)) { + best_effort = true; break; } - + row & r2 = m_rows[get_var_row(x_j)]; coeff.neg(); add_tmp_row(r, coeff, r2); SASSERT(r.get_idx_of(x_j) == -1); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); - SASSERT(satisfy_integrality()); + SASSERT(valid_assignment()); } TRACE("opt", display(tout);); - return result; + return best_effort?BEST_EFFORT:result; + } + + /** + Move the variable x_i maximally towards its bound as long as + bounds of other variables are not violated. + Returns false if an integer bound was truncated and no + progress was made. + */ + + template + bool theory_arith::move_to_bound_new( + theory_var x_i, // variable to move + bool inc, // increment variable or decrement + bool& best_effort, // is bound move a best effort? + bool& has_shared) { // does move include shared variables? + inf_numeral min_gain, max_gain; + init_gains(x_i, inc, min_gain, max_gain); + column & c = m_columns[x_i]; + typename svector::iterator it = c.begin_entries(); + typename svector::iterator end = c.end_entries(); + 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; + update_gains(inc, s, coeff, min_gain, max_gain); + has_shared |= get_context().is_shared(get_enode(s)); + } + if (safe_gain(min_gain, max_gain)) { + TRACE("opt", tout << "Safe delta: " << max_gain << "\n";); + SASSERT(!unbounded_gain(max_gain)); + if (!inc) { + max_gain.neg(); + } + update_value(x_i, max_gain); + best_effort = min_gain.is_pos() && !min_gain.is_one(); + return !max_gain.is_zero(); + } + else { + return false; + } } -#endif /** Move the variable x_i maximally towards its bound as long as @@ -1630,7 +1887,7 @@ namespace smt { bool theory_arith::move_to_bound(theory_var x_i, bool move_to_lower) { inf_numeral delta, delta_abs; numeral lc(1); - + if (move_to_lower) { delta = lower_bound(x_i) - get_value(x_i); SASSERT(!delta.is_pos()); @@ -1711,8 +1968,8 @@ namespace smt { template typename theory_arith::max_min_t theory_arith::max_min(theory_var v, bool max, bool& has_shared) { expr* e = get_enode(v)->get_owner(); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); + + SASSERT(valid_assignment()); SASSERT(!is_quasi_base(v)); if ((max && at_upper(v)) || (!max && at_lower(v))) { TRACE("opt", tout << "At bound: " << mk_pp(e, get_manager()) << "...\n";); @@ -1872,8 +2129,7 @@ namespace smt { bool theory_arith::try_to_imply_eq(theory_var v1, theory_var v2) { SASSERT(v1 != v2); SASSERT(get_value(v1) == get_value(v2)); - SASSERT(valid_row_assignment()); - SASSERT(satisfy_bounds()); + SASSERT(valid_assignment()); if (is_quasi_base(v1) || is_quasi_base(v2)) return false; m_tmp_row.reset(); diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index 99e4303ff..007c8025f 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -211,6 +211,15 @@ namespace smt { } return true; } + + template + bool theory_arith::valid_assignment() const { + return + valid_row_assignment() && + satisfy_bounds() && + satisfy_integrality(); + } + #endif }; diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index cace15db4..8ff122c1e 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -333,12 +333,15 @@ namespace smt { void theory_arith::mul_bound_of(expr * var, unsigned power, interval & target) { theory_var v = expr2var(var); interval i = mk_interval_for(v); - TRACE("non_linear", tout << "bound: " << i << "\n" << mk_pp(var, get_manager()) << "\n"; + + TRACE("non_linear", + display_interval(tout << "bound: ",i); tout << i << "\n"; + tout << mk_pp(var, get_manager()) << "\n"; tout << "power " << power << ": " << expt(i, power) << "\n"; - tout << "target before: " << target << "\n";); + display_interval(tout << "target before: ", target); tout << "\n";); i.expt(power); target *= i; - TRACE("non_linear", tout << "target after: " << target << "\n";); + TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";); } /** @@ -427,12 +430,12 @@ namespace smt { template void theory_arith::mk_derived_nl_bound(theory_var v, inf_numeral const & coeff, bound_kind k, v_dependency * dep) { inf_numeral coeff_norm = normalize_bound(v, coeff, k); - TRACE("buggy_bound", tout << "v" << v << " " << coeff << " " << coeff_norm << " " << k << "\n";); derived_bound * new_bound = alloc(derived_bound, v, coeff_norm, k); m_bounds_to_delete.push_back(new_bound); m_asserted_bounds.push_back(new_bound); // copy justification to new bound dependency2new_bound(dep, *new_bound); + TRACE("buggy_bound", new_bound->display(*this, tout); tout << "\n";); } /** @@ -449,7 +452,8 @@ namespace smt { new_lower += get_epsilon(v); bound * old_lower = lower(v); if (old_lower == 0 || new_lower > old_lower->get_value()) { - TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n";); + TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n"; + display_interval(tout, i); tout << "\n";); mk_derived_nl_bound(v, new_lower, B_LOWER, i.get_lower_dependencies()); r = true; } @@ -460,7 +464,8 @@ namespace smt { new_upper -= get_epsilon(v); bound * old_upper = upper(v); if (old_upper == 0 || new_upper < old_upper->get_value()) { - TRACE("non_linear", tout << "NEW upper bound for v" << v << " " << new_upper << "\n";); + TRACE("non_linear", tout << "NEW upper bound for v" << v << " " << new_upper << "\n"; + display_interval(tout, i); tout << "\n";); mk_derived_nl_bound(v, new_upper, B_UPPER, i.get_upper_dependencies()); r = true; } diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 4eeb6a189..f954f082c 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -395,9 +395,30 @@ namespace smt { template void theory_arith::display_bound(std::ostream & out, bound * b, unsigned indent) const { for (unsigned i = 0; i < indent; i++) out << " "; - theory_var v = b->get_var(); - enode * e = get_enode(v); - out << "v" << v << " #" << e->get_owner_id() << " " << (b->get_bound_kind() == B_LOWER ? ">=" : "<=") << " " << b->get_value() << "\n"; + b->display(*this, out); + out << "\n"; + } + + template + void theory_arith::display_deps(std::ostream & out, v_dependency* dep) { + ptr_vector bounds; + m_dep_manager.linearize(dep, bounds); + m_tmp_lit_set.reset(); + m_tmp_eq_set.reset(); + ptr_vector::const_iterator it = bounds.begin(); + ptr_vector::const_iterator end = bounds.end(); + for (; it != end; ++it) { + bound * b = static_cast(*it); + out << " "; + b->display(*this, out); + } + } + + template + void theory_arith::display_interval(std::ostream & out, interval const& i) { + i.display(out); + display_deps(out << " lo:", i.get_lower_dependencies()); + display_deps(out << " hi:", i.get_upper_dependencies()); } template