diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 8bc841ca0..2380f8969 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -434,7 +434,6 @@ namespace smt { bool m_eager_gcd; // true if gcd should be applied at every add_row unsigned m_final_check_idx; - u_map m_objective_theory_vars; // backtracking svector m_bound_trail; @@ -857,11 +856,13 @@ 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); + bool is_safe_to_leave(theory_var x); 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); - bool max_min(row & r, bool max); + enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT}; + max_min_t max_min(theory_var v, bool max); + max_min_t max_min(row & r, bool max); bool max_min(svector const & vars); // ----------------------------------- diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 7007232b6..515b019eb 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -927,6 +927,26 @@ namespace smt { */ + template + bool theory_arith::is_safe_to_leave(theory_var x) { + + column & c = m_columns[x]; + 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; + bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int()); + TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << "\n"; + display_row(tout, r, true);); + if (is_unsafe) return false; + } + + return true; + } + template theory_var theory_arith::pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain) { TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";); @@ -986,6 +1006,9 @@ namespace smt { } } } + else if (m_util.is_to_real(n, x) || m_util.is_to_int(n, x)) { + return get_theory_vars(x, vars); + } else if (m_util.is_mul(n, x, y) && m_util.is_numeral(x, r)) { return get_theory_vars(y, vars); } @@ -1019,10 +1042,6 @@ namespace smt { template theory_var theory_arith::add_objective(app* term) { theory_var v = internalize_term_core(term); - uint_set vars; - if (get_theory_vars(term, vars)) { - m_objective_theory_vars.insert(v, vars); - } TRACE("opt", tout << mk_pp(term, get_manager()) << " |-> v" << v << "\n";); TRACE("opt", tout << "data-size: " << m_data.size() << "\n";); SASSERT(!is_quasi_base(v)); @@ -1032,22 +1051,12 @@ namespace smt { template inf_eps_rational theory_arith::maximize(theory_var v) { TRACE("opt", tout << "data-size: " << m_data.size() << "\n";); - bool r = max_min(v, true); - if (r || at_upper(v)) { - if (m_objective_theory_vars.contains(v)) { - // FIXME: put this block inside verbose code - uint_set & vars = m_objective_theory_vars[v]; - uint_set::iterator it = vars.begin(), end = vars.end(); - ast_manager& m = get_manager(); - IF_VERBOSE(1, - verbose_stream() << "Optimal assigment:" << std::endl; - for (; it != end; ++it) { - verbose_stream() << mk_pp(get_enode(*it)->get_owner(), m) << " |-> " << get_value(*it) << std::endl; - };); - } - return inf_eps_rational(get_value(v)); + max_min_t r = max_min(v, true); + if (r == UNBOUNDED) { + return inf_eps_rational::infinity(); } - return inf_eps_rational::infinity(); + return inf_eps_rational(get_value(v)); + } /** @@ -1092,7 +1101,6 @@ namespace smt { */ template expr* theory_arith::mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val) { - SASSERT(m_objective_theory_vars.contains(v)); ast_manager& m = get_manager(); context& ctx = get_context(); std::ostringstream strm; @@ -1262,9 +1270,10 @@ namespace smt { Return true if succeeded. */ template - bool theory_arith::max_min(row & r, bool max) { + typename theory_arith::max_min_t theory_arith::max_min(row & r, bool max) { TRACE("max_min", tout << "max_min...\n";); m_stats.m_max_min++; + bool skipped_row = false; SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); @@ -1292,6 +1301,10 @@ 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))) continue; // variable cannot be used for max/min. + if (!is_safe_to_leave(curr_x_j)) { + skipped_row = true; + continue; + } theory_var curr_x_i = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_gain); if (curr_x_i == null_theory_var) { // we can increase/decrease curr_x_j as much as we want. @@ -1325,7 +1338,7 @@ namespace smt { TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); - return true; + return skipped_row?BEST_EFFORT:OPTIMIZED; } if (x_i == null_theory_var) { @@ -1344,7 +1357,7 @@ namespace smt { SASSERT(satisfy_bounds()); continue; } - return false; // unbounded. + return UNBOUNDED; } if (!is_fixed(x_j) && is_bounded(x_j) && (upper_bound(x_j) - lower_bound(x_j) <= gain)) { @@ -1471,13 +1484,13 @@ namespace smt { \brief Maximize/Minimize the given variable. The bounds of v are update if procedure succeeds. */ template - bool theory_arith::max_min(theory_var v, bool max) { + typename theory_arith::max_min_t theory_arith::max_min(theory_var v, bool max) { TRACE("opt", tout << (max ? "maximizing" : "minimizing") << " v" << v << "...\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); SASSERT(!is_quasi_base(v)); if ((max && at_upper(v)) || (!max && at_lower(v))) - return false; // nothing to be done... + return AT_BOUND; // nothing to be done... m_tmp_row.reset(); if (is_non_base(v)) { add_tmp_row_entry(m_tmp_row, numeral(1), v); @@ -1491,15 +1504,15 @@ namespace smt { add_tmp_row_entry(m_tmp_row, it->m_coeff, it->m_var); } } - if (max_min(m_tmp_row, max)) { + max_min_t r = max_min(m_tmp_row, max); + if (r == OPTIMIZED) { TRACE("opt", tout << "v" << v << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n"; display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row);); mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row); - return true; } - return false; + return r; } /** @@ -1512,9 +1525,9 @@ namespace smt { svector::const_iterator it = vars.begin(); svector::const_iterator end = vars.end(); for (; it != end; ++it) { - if (max_min(*it, true)) + if (max_min(*it, true) == OPTIMIZED) succ = true; - if (max_min(*it, false)) + if (max_min(*it, false) == OPTIMIZED) succ = true; } if (succ) { @@ -1688,9 +1701,9 @@ namespace smt { m_tmp_lit_set.reset(); m_tmp_eq_set.reset(); - if (max_min(m_tmp_row, true) && + if ((OPTIMIZED == max_min(m_tmp_row, true)) && is_zero_row(m_tmp_row, true, m_tmp_acc_lits, m_tmp_acc_eqs, m_tmp_lit_set, m_tmp_eq_set) && - max_min(m_tmp_row, false) && + (OPTIMIZED == max_min(m_tmp_row, false)) && is_zero_row(m_tmp_row, false, m_tmp_acc_lits, m_tmp_acc_eqs, m_tmp_lit_set, m_tmp_eq_set)) { // v1 == v2 TRACE("imply_eq", tout << "found new implied equality:\n"; diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 944414267..49032bdc8 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1237,7 +1237,6 @@ namespace smt { m_nl_rounds = 0; m_nl_gb_exhausted = false; m_nl_strategy_idx = 0; - m_objective_theory_vars .reset(); theory::reset_eh(); }