diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index 6e6fcaee0..3ba733174 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -93,8 +93,8 @@ namespace smt { bool choose_entering_edge() { TRACE("network_flow", tout << "choose_entering_edge...\n";); - unsigned num_edges = m_graph.get_num_edges(); - for (unsigned i = m_next_edge; i < m_next_edge + num_edges; ++i) { + int num_edges = m_graph.get_num_edges(); + for (int i = m_next_edge; i < m_next_edge + num_edges; ++i) { edge_id id = (i >= num_edges) ? (i - num_edges) : i; node src = m_graph.get_source(id); node tgt = m_graph.get_target(id); @@ -106,6 +106,10 @@ namespace smt { tout << "Found entering edge " << id << " between node "; tout << src << " and node " << tgt << " with reduced cost = " << cost << "...\n"; }); + m_next_edge = m_enter_id; + if (m_next_edge >= num_edges) { + m_next_edge -= num_edges; + } return true; } } diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index c5038222e..2b48dadac 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -295,6 +295,13 @@ namespace smt { } } + for (unsigned i = 0; i < num_edges; ++i) { + dl_var src = m_graph.get_source(i); + dl_var tgt = m_graph.get_target(i); + numeral weight = m_graph.get_weight(i); + SASSERT(m_potentials[src] - m_potentials[tgt] <= weight); + } + // m_flows are zero on non-basic edges for (unsigned i = 0; i < m_flows.size(); ++i) { SASSERT(m_states[i] == BASIS || m_flows[i].is_zero()); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 45e2ffdfa..15fc6e19a 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -37,6 +37,7 @@ Revision History: #include"arith_simplifier_plugin.h" #include"arith_eq_solver.h" #include"theory_opt.h" +#include"uint_set.h" namespace smt { @@ -433,7 +434,7 @@ namespace smt { bool m_eager_gcd; // true if gcd should be applied at every add_row unsigned m_final_check_idx; - inf_eps_rational m_objective_value; + u_map m_objective_vars; // backtracking svector m_bound_trail; @@ -1008,6 +1009,7 @@ namespace smt { private: bool_var m_bound_watch; inf_eps_rational m_upper_bound; + bool get_theory_vars(expr * n, uint_set & vars); public: // ----------------------------------- // diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 430e29358..6948cc8a7 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -966,28 +966,78 @@ namespace smt { return x_i; } + template + bool theory_arith::get_theory_vars(expr * n, uint_set & vars) { + rational r; + expr* x, *y; + if (m_util.is_numeral(n, r)) { + return true; + } + else if (m_util.is_add(n)) { + for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) { + if (!get_theory_vars(to_app(n)->get_arg(i), vars)) { + return false; + } + } + } + else if (m_util.is_mul(n, x, y) && m_util.is_numeral(x, r)) { + return get_theory_vars(y, vars); + } + else if (m_util.is_mul(n, y, x) && m_util.is_numeral(x, r)) { + return get_theory_vars(y, vars); + } + else if (!is_app(n)) { + return false; + } + else if (to_app(n)->get_family_id() == m_util.get_family_id()) { + return false; + } + else { + context & ctx = get_context(); + SASSERT(ctx.e_internalized(n)); + enode * e = ctx.get_enode(n); + if (is_attached_to_var(e)) { + vars.insert(e->get_th_var(get_id())); + } + return true; + } + return true; + } + // // add_objective(expr* term) internalizes the arithmetic term and creates // a row for it if it is not already internalized. // Then return the variable corresponding to the term. // - template theory_var theory_arith::add_objective(app* term) { - return internalize_term_core(term); + theory_var v = internalize_term_core(term); + uint_set vars; + if (get_theory_vars(term, vars)) { + m_objective_vars.insert(v, vars); + } + return v; } template inf_eps_rational theory_arith::maximize(theory_var v) { bool r = max_min(v, true); - if (at_upper(v)) { - m_objective_value = get_value(v); + if (r || at_upper(v)) { + if (m_objective_vars.contains(v)) { + // FIXME: put this block inside verbose code + uint_set & vars = m_objective_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)); } - else if (!r) { - m_objective_value = inf_eps_rational::infinity(); - } - return m_objective_value; + return inf_eps_rational::infinity(); } /** @@ -1414,8 +1464,6 @@ namespace smt { TRACE("maximize", 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);); - m_objective_value = get_value(v); - mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row); return true; diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 7f85d854f..f6b704359 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -316,7 +316,9 @@ namespace smt { bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); - private: + private: + + virtual expr* 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 d0cef90cf..e87c34b94 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -29,6 +29,7 @@ Revision History: #include"warning.h" #include"smt_model_generator.h" #include"network_flow_def.h" +#include"model_implicant.h" using namespace smt; @@ -1036,9 +1037,12 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { vector & current_assigments = m_objective_assignments[v]; SASSERT(!current_assigments.empty()); - TRACE("network_flow", - for (unsigned i = 0; i < current_assigments.size(); ++i) { - tout << "v" << i << " -> " << current_assigments[i] << std::endl; + ast_manager& m = get_manager(); + IF_VERBOSE(1, + verbose_stream() << "Optimal assigment:" << std::endl; + for (unsigned i = 0; i < objective.size(); ++i) { + theory_var v = objective[i].first; + verbose_stream() << mk_pp(get_enode(v)->get_owner(), m) << " |-> " << current_assigments[v] << std::endl; }); rational r = objective_value.get_rational().to_rational(); rational i = objective_value.get_infinitesimal().to_rational(); @@ -1068,7 +1072,7 @@ theory_var theory_diff_logic::add_objective(app* term) { } template -expr* theory_diff_logic::block_lower_bound(theory_var v, inf_rational const& val) { +expr* 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); @@ -1135,6 +1139,19 @@ expr* theory_diff_logic::block_lower_bound(theory_var v, inf_rational const } } +template +expr* theory_diff_logic::block_lower_bound(theory_var v, inf_rational const& val) { + expr * o = block_objective(v, val); + context & ctx = get_context(); + model_ref mdl; + ctx.get_model(mdl); + ptr_vector formulas(ctx.get_num_asserted_formulas(), ctx.get_asserted_formulas()); + ast_manager& m = get_manager(); + model_implicant impl_extractor(m); + expr_ref_vector implicants = impl_extractor.minimize_literals(formulas, mdl); + return m.mk_and(o, m.mk_not(m.mk_and(implicants.size(), implicants.c_ptr()))); +} + template bool theory_diff_logic::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) {