diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index a3a44e34b..0e00e368b 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -636,9 +636,11 @@ namespace simplex { // pivot(x_i, x_j, a_ij); - move_to_bound(x_i, inc != m.is_pos(a_ij)); + TRACE("simplex", display(tout << "after pivot\n");); + move_to_bound(x_i, !inc); SASSERT(well_formed_row(row(m_vars[x_j].m_base2row))); TRACE("simplex", display(tout);); + SASSERT(is_feasible()); } return l_true; } @@ -685,7 +687,8 @@ namespace simplex { em.sub(*bound, vs.m_value, delta2); em.mul(delta2, base_coeff, delta2); em.div(delta2, coeff, delta2); - abs(delta2); + em.abs(delta2); + TRACE("simplex", tout << "Delta for v" << s << " " << delta2 << "\n";); if (delta2 < delta) { delta = delta2; } @@ -697,6 +700,15 @@ namespace simplex { update_value(x, delta); } + /** + \brief + Arguments: + v - base variable of row(v) to optimize + x_i - base variable of row(x_i) to become non-base + x_j - variable in row(v) to make a base variable + a_ij - coefficient to x_j in row(x_i) + inc - whether to increment x_j (true if coefficient in row(v) is negative). + */ template void simplex::select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij, bool& inc) { row r(m_vars[v].m_base2row); @@ -758,7 +770,7 @@ namespace simplex { numeral const& a_ij = it.get_row_entry().m_coeff; numeral const& a_ii = vi.m_base_coeff; bool inc_s = (m.is_pos(a_ii) != m.is_pos(a_ij)) ? inc : !inc; - TRACE("simplex", tout << "v" << x_j << " incs: " << inc_s + TRACE("simplex", tout << "v" << x_j << " base v" << s << " incs: " << inc_s << " upper valid:" << vi.m_upper_valid << " lower valid:" << vi.m_lower_valid << "\n"; display_row(tout, r);); @@ -775,13 +787,13 @@ namespace simplex { if (is_neg(curr_gain)) { curr_gain.neg(); } - if (x_i == null_var || (gain < curr_gain) || + if (x_i == null_var || (curr_gain < gain) || (is_zero(gain) && is_zero(curr_gain) && s < x_i)) { x_i = s; gain = curr_gain; new_a_ij = a_ij; TRACE("simplex", tout << "x_j v" << x_j << " x_i v" << x_i << " gain: "; - tout << em.to_string(curr_gain) << "\n";); + tout << curr_gain << "\n";); } } return x_i; diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 70a3268d7..91cf9796f 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -190,7 +190,7 @@ namespace smt { typedef vector > objective_term; vector m_objectives; vector m_objective_consts; - vector > m_objective_assignments; + vector m_objective_assignments; // Set a conflict due to a negative cycle. void set_neg_cycle_conflict(); @@ -317,7 +317,7 @@ namespace smt { private: - virtual expr* block_objective(theory_var v, inf_rational const& val); + expr_ref block_objective(theory_var v, inf_rational const& val); virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 553a4aef2..875a3ff94 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1000,8 +1000,9 @@ void theory_diff_logic::get_implied_bound_antecedents(edge_id bridge_edge, template inf_eps_rational theory_diff_logic::maximize(theory_var v) { - - simplex::simplex S; + + typedef simplex::simplex Simplex; + Simplex S; objective_term const& objective = m_objectives[v]; IF_VERBOSE(1, @@ -1059,7 +1060,7 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { } coeffs.push_back(mpq(1)); vars.push_back(w); - S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr()); + Simplex::row row = S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr()); TRACE("opt", S.display(tout); display(tout);); @@ -1076,6 +1077,16 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { simplex::mpq_ext::eps_numeral const& val = S.get_value(w); inf_rational r(-rational(val.first), -rational(val.second)); TRACE("opt", tout << r << " " << "\n"; ); + Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row); + S.display_row(std::cout, row, true); + for (; it != end; ++it) { + unsigned v = it->m_var; + if (num_nodes <= v && v < num_nodes + num_edges) { + unsigned edge_id = v - num_nodes; + literal lit = m_graph.get_explanation(edge_id); + std::cout << lit << "\n"; + } + } return inf_eps_rational(rational(0), r); } default: @@ -1089,7 +1100,7 @@ theory_var theory_diff_logic::add_objective(app* term) { objective_term objective; theory_var result = m_objectives.size(); rational q(1), r(0); - vector vr; + expr_ref_vector vr(get_manager()); if (internalize_objective(term, q, r, objective)) { m_objectives.push_back(objective); m_objective_consts.push_back(r); @@ -1102,7 +1113,7 @@ theory_var theory_diff_logic::add_objective(app* term) { } template -expr* theory_diff_logic::block_objective(theory_var v, inf_rational const& val) { +expr_ref theory_diff_logic::block_objective(theory_var v, inf_rational const& val) { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); @@ -1123,55 +1134,26 @@ expr* theory_diff_logic::block_objective(theory_var v, inf_rational const& f = m_util.mk_sub(f, f2); } else { - expr_ref_vector disj(m); - vector const & ns = m_objective_assignments[v]; - inf_rational val; - rational r, s; - rational r0 = ns[0].get_rational().to_rational(); - rational s0 = ns[0].get_infinitesimal().to_rational(); - app * x; - app * x0 = get_enode(t[0].first)->get_owner(); - // Assert improved bounds for x_i - x_0 - for (unsigned i = 1; i < t.size(); ++i) { - r = ns[i].get_rational().to_rational(); - s = ns[i].get_infinitesimal().to_rational(); - val = inf_rational(r - r0, s - s0); - x = get_enode(t[i].first)->get_owner(); - f = m_util.mk_sub(x, x0); - e = m_util.mk_numeral(val.get_rational(), m.get_sort(f)); - if (t[i].second.is_neg() && val.get_infinitesimal().is_pos()) { - disj.push_back(m_util.mk_le(f, e)); - } - else if (t[i].second.is_neg()) { - disj.push_back(m_util.mk_lt(f, e)); - } - else if (t[i].second.is_pos() && val.get_infinitesimal().is_neg()) { - disj.push_back(m_util.mk_ge(f, e)); - } - else if (t[i].second.is_pos()) { - disj.push_back(m_util.mk_gt(f, e)); - } - else { - UNREACHABLE(); - } - } - return m.mk_or(disj.size(), disj.c_ptr()); + // + f = m.mk_true(); + return f; } inf_rational new_val = val - inf_rational(m_objective_consts[v]); e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f)); if (new_val.get_infinitesimal().is_neg()) { - return m_util.mk_ge(f, e); + f = m_util.mk_ge(f, e); } else { - return m_util.mk_gt(f, e); + f = m_util.mk_gt(f, e); } + return f; } template expr* theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) { - expr * o = block_objective(v, val); + expr_ref o = block_objective(v, val); context & ctx = get_context(); model_ref mdl; ctx.get_model(mdl); diff --git a/src/util/mpq_inf.cpp b/src/util/mpq_inf.cpp index cb3232d6c..19289b737 100644 --- a/src/util/mpq_inf.cpp +++ b/src/util/mpq_inf.cpp @@ -38,5 +38,6 @@ std::string mpq_inf_manager::to_string(mpq_inf const & a) { return s; } + template class mpq_inf_manager; template class mpq_inf_manager; diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h index 4b6a7d33d..052183dd1 100644 --- a/src/util/mpq_inf.h +++ b/src/util/mpq_inf.h @@ -271,6 +271,11 @@ public: } std::string to_string(mpq_inf const & a); + + void display(std::ostream & out, mpq_inf const & a) { + out << to_string(a); + } + }; typedef mpq_inf_manager synch_mpq_inf_manager;