mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

debugging network simplex

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-05 16:31:29 -08:00
parent 192ce11ca6
commit 5fc429c501
6 changed files with 75 additions and 102 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/network_flow.h
View file

@ -144,9 +144,11 @@ namespace smt {
graph m_graph;
scoped_ptr<spanning_tree_base> m_tree;
scoped_ptr<pivot_rule_impl> m_pivot;
vector<fin_numeral> m_balances; // Denote supply/demand b_i on node i
vector<numeral> m_potentials; // Duals of flows which are convenient to compute dual solutions
vector<numeral> m_flows; // Basic feasible flows
vector<fin_numeral> m_balances; // nodes + 1 |-> [b -1b] Denote supply/demand b_i on node i
vector<numeral> m_potentials; // nodes + 1 |-> initial: +/- 1
// Duals of flows which are convenient to compute dual solutions
// become solutions to Dual simplex.
vector<numeral> m_flows; // edges + nodes |-> assignemnt Basic feasible flows
svector<edge_state> m_states;
unsigned m_step;
edge_id m_enter_id;
@ -176,9 +178,10 @@ namespace smt {
bool check_well_formed();
bool check_optimal();
void display(std::ofstream & os);
void display_primal(std::ofstream & os);
void display_dual(std::ofstream & os);
void display_spanning_tree(std::ofstream & os);
void display_system(std::ofstream & os);
public:

119
src/smt/network_flow_def.h
View file

@ -28,7 +28,7 @@ namespace smt {
template<typename Ext>
bool network_flow<Ext>::first_eligible_pivot::choose_entering_edge() {
TRACE("network_flow", tout << "choose_entering_edge...\n";);
numeral cost = numeral::zero();
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;
@ -37,65 +37,51 @@ namespace smt {
}
node src = m_graph.get_source(id);
node tgt = m_graph.get_target(id);
numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
if (cost.is_pos()) {
m_next_edge = m_enter_id = id;
TRACE("network_flow",
tout << "Found entering edge " << id << " between node ";
tout << src << " and node " << tgt << " with reduced cost = " << cost << "...\n";);
return true;
}
}
TRACE("network_flow", tout << "Found no entering edge...\n";);
return false;
};
template<typename Ext>
bool network_flow<Ext>::best_eligible_pivot::choose_entering_edge() {
TRACE("network_flow", tout << "choose_entering_edge...\n";);
unsigned num_edges = m_graph.get_num_edges();
numeral max = numeral::zero();
numeral cost = numeral::zero();
for (unsigned i = 0; i < num_edges; ++i) {
node src = m_graph.get_source(i);
node tgt = m_graph.get_target(i);
if (!edge_in_tree(i)) {
numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(i);
if (cost > max) {
max = cost;
numeral new_cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(i);
if (new_cost > cost) {
cost = new_cost;
m_enter_id = i;
}
}
}
if (max.is_pos()) {
TRACE("network_flow", {
tout << "Found entering edge " << m_enter_id << " between node ";
tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id);
tout << " with reduced cost = " << max << "...\n";
});
return true;
}
TRACE("network_flow", tout << "Found no entering edge...\n";);
return false;
return cost.is_pos();
};
template<typename Ext>
bool network_flow<Ext>::candidate_list_pivot::choose_entering_edge() {
numeral cost = numeral::zero();
if (m_current_length == 0 || m_minor_step == MINOR_STEP_LIMIT) {
// Build the candidate list
unsigned num_edges = m_graph.get_num_edges();
numeral max = numeral::zero();
m_current_length = 0;
for (unsigned 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);
if (!edge_in_tree(id)) {
numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
if (cost.is_pos()) {
numeral new_cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
if (new_cost.is_pos()) {
m_candidates[m_current_length] = id;
++m_current_length;
if (cost > max) {
max = cost;
if (new_cost > cost) {
cost = new_cost;
m_enter_id = id;
}
}
@ -104,48 +90,29 @@ namespace smt {
}
m_next_edge = m_enter_id;
m_minor_step = 1;
if (max.is_pos()) {
TRACE("network_flow", {
tout << "Found entering edge " << m_enter_id << " between node ";
tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id);
tout << " with reduced cost = " << max << "...\n";
});
return true;
}
TRACE("network_flow", tout << "Found no entering edge...\n";);
return false;
return cost.is_pos();
}
++m_minor_step;
numeral max = numeral::zero();
for (unsigned i = 0; i < m_current_length; ++i) {
edge_id id = m_candidates[i];
node src = m_graph.get_source(id);
node tgt = m_graph.get_target(id);
if (!edge_in_tree(id)) {
numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
if (cost > max) {
max = cost;
numeral new_cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
if (new_cost > cost) {
cost = new_cost;
m_enter_id = id;
}
// Remove stale candidates
if (!cost.is_pos()) {
if (!new_cost.is_pos()) {
--m_current_length;
m_candidates[i] = m_candidates[m_current_length];
--i;
}
}
}
if (max.is_pos()) {
TRACE("network_flow", {
tout << "Found entering edge " << m_enter_id << " between node ";
tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id);
tout << " with reduced cost = " << max << "...\n";
});
return true;
}
TRACE("network_flow", tout << "Found no entering edge...\n";);
return false;
return cost.is_pos();
};
template<typename Ext>
@ -167,7 +134,7 @@ namespace smt {
tout << "Difference logic optimization:" << std::endl;
display_dual(tout);
tout << "Minimum cost flow:" << std::endl;
display(tout);
display_primal(tout);
};);
m_step = 0;
@ -219,7 +186,8 @@ namespace smt {
tout << pp_vector("Flows", m_flows);
tout << "Cost: " << get_cost() << "\n";
tout << "Spanning tree:\n";
display_spanning_tree(tout););
display_spanning_tree(tout);
display_primal(tout););
SASSERT(check_well_formed());
}
@ -252,7 +220,6 @@ namespace smt {
template<typename Ext>
void network_flow<Ext>::update_flows() {
TRACE("network_flow", tout << "update_flows...\n";);
m_flows[m_enter_id] += *m_delta;
node src = m_graph.get_source(m_enter_id);
node tgt = m_graph.get_target(m_enter_id);
@ -269,7 +236,6 @@ namespace smt {
template<typename Ext>
bool network_flow<Ext>::choose_leaving_edge() {
TRACE("network_flow", tout << "choose_leaving_edge...\n";);
node src = m_graph.get_source(m_enter_id);
node tgt = m_graph.get_target(m_enter_id);
m_delta.set_invalid();
@ -286,14 +252,7 @@ namespace smt {
}
}
m_leave_id = leave_id;
TRACE("network_flow",
tout << "Leaving edge " << m_leave_id;
tout << " between node " << m_graph.get_source(m_leave_id);
tout << " and node " << m_graph.get_target(m_leave_id) ;
if (m_delta) tout << " with delta = " << *m_delta;
tout << "\n";);
return m_delta;
}
@ -329,6 +288,19 @@ namespace smt {
while (choose_entering_edge(pr)) {
bool bounded = choose_leaving_edge();
if (!bounded) return UNBOUNDED;
//TRACE("network_flow",
{
vector<edge>const& es = m_graph.get_all_edges();
edge const& e_in = es[m_enter_id];
edge const& e_out = es[m_leave_id];
node src_in = e_in.get_source(), tgt_in = e_in.get_target();
node src_out = e_out.get_source(), tgt_out = e_out.get_target();
numeral c1 = m_potentials[src_in] - m_potentials[tgt_in] - m_graph.get_weight(m_enter_id);
numeral c2 = m_potentials[src_out] - m_potentials[tgt_out] - m_graph.get_weight(m_leave_id);
tout << "new base: y_" << src_in << "_" << tgt_in << " cost: " << c1 << " delta: " << *m_delta << "\n";
tout << "old base: y_" << src_out << "_" << tgt_out << " cost: " << c2 << "\n";
}
// );
update_flows();
if (m_enter_id != m_leave_id) {
SASSERT(edge_in_tree(m_leave_id));
@ -340,10 +312,18 @@ namespace smt {
TRACE("network_flow",
tout << "Spanning tree:\n";
display_spanning_tree(tout);
tout << "Cost: " << get_cost() << "\n";);
tout << "Cost: " << get_cost() << "\n";
display_primal(tout);
);
SASSERT(check_well_formed());
}
}
TRACE("network_flow",
tout << "Spanning tree:\n";
display_spanning_tree(tout);
tout << "Cost: " << get_cost() << "\n";
display_primal(tout);
);
if (is_infeasible()) return INFEASIBLE;
TRACE("network_flow", tout << "Found optimal solution.\n";);
SASSERT(check_optimal());
@ -352,14 +332,13 @@ namespace smt {
template<typename Ext>
bool network_flow<Ext>::is_infeasible() {
#if 0
// Flows of artificial arcs should be zero
unsigned num_nodes = m_graph.get_num_nodes();
unsigned num_edges = m_graph.get_num_edges();
SASSERT(m_flows.size() == num_edges);
for (unsigned i = 1; i < num_nodes; ++i) {
if (m_flows[num_edges - i].is_pos()) return true;
}
#endif
return false;
}
@ -445,7 +424,7 @@ namespace smt {
// display methods
template<typename Ext>
void network_flow<Ext>::display(std::ofstream & os) {
void network_flow<Ext>::display_primal(std::ofstream & os) {
vector<edge> const & es = m_graph.get_all_edges();
for (unsigned i = 0; i < m_graph.get_num_edges(); ++i) {
edge const & e = es[i];
@ -486,6 +465,12 @@ namespace smt {
};
os << "))" << std::endl;
os << "(optimize)" << std::endl;
if (!m_flows.empty()) {
for (unsigned i = 0; i < m_graph.get_num_edges(); ++i) {
edge const & e = es[i];
os << "; y_" << e.get_source() << "_" << e.get_target() << " = " << m_flows[i] << "\n";
}
}
}

10
src/smt/theory_diff_logic.h
View file

@ -165,8 +165,7 @@ namespace smt {
arith_eq_adapter m_arith_eq_adapter;
theory_diff_logic_statistics m_stats;
dl_graph<GExt> m_graph;
theory_var m_zero_int; // cache the variable representing the zero variable.
theory_var m_zero_real; // cache the variable representing the zero variable.
theory_var m_zero; // cache the variable representing the zero variable.
int_vector m_scc_id; // Cheap equality propagation
eq_prop_info_set m_eq_prop_info_set; // set of existing equality prop infos
ptr_vector<eq_prop_info> m_eq_prop_infos;
@ -217,8 +216,7 @@ namespace smt {
m_params(params),
m_util(m),
m_arith_eq_adapter(*this, params, m_util),
m_zero_int(null_theory_var),
m_zero_real(null_theory_var),
m_zero(null_theory_var),
m_asserted_qhead(0),
m_num_core_conflicts(0),
m_num_propagation_calls(0),
@ -358,9 +356,9 @@ namespace smt {
void get_implied_bound_antecedents(edge_id bridge_edge, edge_id subsumed_edge, conflict_resolution & cr);
theory_var get_zero(sort* s) const { return m_util.is_int(s)?m_zero_int:m_zero_real; }
theory_var get_zero(sort* s) const { return m_zero; }
theory_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
theory_var get_zero(expr* e) const { return m_zero; }
void inc_conflicts();

17
src/smt/theory_diff_logic_def.h
View file

@ -71,12 +71,7 @@ void theory_diff_logic<Ext>::init(context * ctx) {
zero = m_util.mk_numeral(rational(0), true);
e = ctx->mk_enode(zero, false, false, true);
SASSERT(!is_attached_to_var(e));
m_zero_int = mk_var(e);
zero = m_util.mk_numeral(rational(0), false);
e = ctx->mk_enode(zero, false, false, true);
SASSERT(!is_attached_to_var(e));
m_zero_real = mk_var(e);
m_zero = mk_var(e);
}
@ -356,7 +351,7 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
TRACE("arith_final", display(tout); );
// either will already be zero (as we don't do mixed constraints).
m_graph.set_to_zero(m_zero_int, m_zero_real);
m_graph.set_to_zero(m_zero);
SASSERT(is_consistent());
if (m_non_diff_logic_exprs) {
return FC_GIVEUP;
@ -766,8 +761,7 @@ void theory_diff_logic<Ext>::reset_eh() {
dealloc(m_atoms[i]);
}
m_graph .reset();
m_zero_int = null_theory_var;
m_zero_real = null_theory_var;
m_zero = null_theory_var;
m_atoms .reset();
m_asserted_atoms .reset();
m_stats .reset();
@ -1022,10 +1016,9 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
sum += balance;
}
// HACK: assume that v0 is always value 0
if (balances[0].is_zero()) {
balances[0] = -sum;
}
balances[0] = -sum;
TRACE("arith", display(tout););
network_flow<GExt> net_flow(m_graph, balances);
min_flow_result result = net_flow.min_cost();
SASSERT(result != UNBOUNDED);

5
src/smt/theory_utvpi.h
View file

@ -138,8 +138,7 @@ namespace smt {
smt_params m_params;
arith_util a;
arith_eq_adapter m_arith_eq_adapter;
th_var m_zero_int; // cache the variable representing the zero variable.
th_var m_zero_real; // cache the variable representing the zero variable.
th_var m_zero; //cache the variable representing the zero variable.
dl_graph<GExt> m_graph;
nc_functor m_nc_functor;
@ -304,7 +303,7 @@ namespace smt {
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
th_var get_zero(sort* s) const { return m_zero; }
th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }

15
src/smt/theory_utvpi_def.h
View file

@ -62,8 +62,7 @@ namespace smt {
theory(m.mk_family_id("arith")),
a(m),
m_arith_eq_adapter(*this, m_params, a),
m_zero_int(null_theory_var),
m_zero_real(null_theory_var),
m_zero(null_theory_var),
m_nc_functor(*this),
m_asserted_qhead(0),
m_agility(0.5),
@ -134,8 +133,7 @@ namespace smt {
template<typename Ext>
void theory_utvpi<Ext>::reset_eh() {
m_graph .reset();
m_zero_int = null_theory_var;
m_zero_real = null_theory_var;
m_zero = null_theory_var;
m_atoms .reset();
m_asserted_atoms .reset();
m_stats .reset();
@ -261,8 +259,7 @@ namespace smt {
template<typename Ext>
void theory_utvpi<Ext>::init(context* ctx) {
theory::init(ctx);
m_zero_int = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true));
m_zero_real = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), false), false, false, true));
m_zero = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true));
}
/**
@ -556,7 +553,7 @@ namespace smt {
theory_var v = null_theory_var;
context& ctx = get_context();
if (r.is_zero()) {
v = a.is_int(n)?m_zero_int:m_zero_real;
v = m_zero;
}
else if (ctx.e_internalized(n)) {
enode* e = ctx.get_enode(n);
@ -778,9 +775,7 @@ namespace smt {
m_factory = alloc(arith_factory, get_manager());
m.register_factory(m_factory);
enforce_parity();
m_graph.set_to_zero(to_var(m_zero_int), to_var(m_zero_real));
m_graph.set_to_zero(neg(to_var(m_zero_int)), neg(to_var(m_zero_real)));
m_graph.set_to_zero(to_var(m_zero_int), neg(to_var(m_zero_int)));
m_graph.set_to_zero(to_var(m_zero), neg(to_var(m_zero)));
compute_delta();
DEBUG_CODE(validate_model(););
}