mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Update basic spanning tree to be on par with threaded one
This commit is contained in:
parent
7bc7a61a40
commit
37f5628824
|
@ -71,7 +71,6 @@ namespace smt {
|
|||
edge_id & m_enter_id;
|
||||
|
||||
public:
|
||||
pivot_rule_impl() {}
|
||||
pivot_rule_impl(graph & g, vector<numeral> & potentials,
|
||||
svector<edge_state> & states, edge_id & enter_id)
|
||||
: m_graph(g),
|
||||
|
@ -79,7 +78,7 @@ namespace smt {
|
|||
m_states(states),
|
||||
m_enter_id(enter_id) {
|
||||
}
|
||||
bool choose_entering_edge() {return false;};
|
||||
virtual bool choose_entering_edge() = 0;
|
||||
};
|
||||
|
||||
class first_eligible_pivot : public pivot_rule_impl {
|
||||
|
|
|
@ -40,6 +40,24 @@ namespace smt {
|
|||
m_graph.add_edge(e.get_target(), e.get_source(), e.get_weight(), explanation());
|
||||
}
|
||||
}
|
||||
TRACE("network_flow", {
|
||||
tout << "Solving different logic optimization problem:" << std::endl;
|
||||
for (unsigned i = 0; i < m_graph.get_num_nodes(); ++i) {
|
||||
tout << "(declare-fun v" << i << " () Real)" << std::endl;
|
||||
}
|
||||
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];
|
||||
tout << "(assert (<= (- v" << e.get_source() << " v" << e.get_target() << ") " << e.get_weight() << "))" << std::endl;
|
||||
};
|
||||
tout << "(maximize (+ ";
|
||||
for (unsigned i = 0; i < balances.size(); ++i) {
|
||||
tout << "(* " << balances[i] << " v" << i << ") ";
|
||||
};
|
||||
tout << "))" << std::endl;
|
||||
tout << "(optimize)" << std::endl;
|
||||
};);
|
||||
|
||||
m_step = 0;
|
||||
m_tree = alloc(basic_spanning_tree<Ext>, m_graph);
|
||||
}
|
||||
|
@ -130,7 +148,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool network_flow<Ext>::choose_leaving_edge() {
|
||||
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);
|
||||
|
@ -155,10 +173,10 @@ namespace smt {
|
|||
tout << "Found 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) << " with delta = " << *m_delta << "...\n";
|
||||
});
|
||||
});
|
||||
return true;
|
||||
}
|
||||
TRACE("network_flow", tout << "Can't find a leaving edge... The problem is unbounded.\n";);
|
||||
TRACE("network_flow", tout << "Can't find a leaving edge... The problem is unbounded.\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
|
@ -179,7 +197,7 @@ namespace smt {
|
|||
pivot = alloc(best_eligible_pivot, m_graph, m_potentials, m_states, m_enter_id);
|
||||
break;
|
||||
case CANDIDATE_LIST:
|
||||
pivot = alloc(best_eligible_pivot, m_graph, m_potentials, m_states, m_enter_id);
|
||||
pivot = alloc(candidate_list_pivot, m_graph, m_potentials, m_states, m_enter_id);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
@ -208,7 +226,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
m_states[m_leave_id] = m_states[m_leave_id] == LOWER ? UPPER : LOWER;
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE("network_flow", tout << "Found optimal solution.\n";);
|
||||
SASSERT(check_optimal());
|
||||
|
|
|
@ -74,7 +74,6 @@ namespace smt {
|
|||
private:
|
||||
graph * m_tree_graph;
|
||||
|
||||
|
||||
public:
|
||||
basic_spanning_tree(graph & g);
|
||||
void initialize(svector<edge_id> const & tree);
|
||||
|
|
|
@ -421,8 +421,7 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void basic_spanning_tree<Ext>::initialize(svector<edge_id> const & tree) {
|
||||
m_tree_graph = alloc(graph);
|
||||
m_tree.reset();
|
||||
m_tree.append(tree);
|
||||
m_tree = tree;
|
||||
unsigned num_nodes = m_graph.get_num_nodes();
|
||||
for (unsigned i = 0; i < num_nodes; ++i) {
|
||||
m_tree_graph->init_var(i);
|
||||
|
@ -464,11 +463,25 @@ namespace smt {
|
|||
m_tree_graph->bfs_undirected(root, m_pred, m_depth);
|
||||
m_tree_graph->dfs_undirected(root, m_thread);
|
||||
|
||||
for (node x = m_thread[root]; x != root; x = m_thread[x]) {
|
||||
vector<edge> const & tree_edges = m_tree_graph->get_all_edges();
|
||||
for (unsigned i = 0; i < tree_edges.size(); ++i) {
|
||||
edge const & e = tree_edges[i];
|
||||
dl_var src = e.get_source();
|
||||
dl_var tgt = e.get_target();
|
||||
edge_id id;
|
||||
VERIFY(m_graph.get_edge_id(x, m_pred[x], id));
|
||||
m_tree[x] = id;
|
||||
VERIFY(m_graph.get_edge_id(src, tgt, id));
|
||||
SASSERT(tgt == m_pred[src] || src == m_pred[tgt]);
|
||||
if (tgt == m_pred[src]) {
|
||||
m_tree[src] = id;
|
||||
}
|
||||
else {
|
||||
m_tree[tgt] = id;
|
||||
}
|
||||
}
|
||||
|
||||
node p = m_graph.get_source(enter_id);
|
||||
node q = m_graph.get_target(enter_id);
|
||||
m_root_t2 = p == m_pred[q] ? q : p;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -192,7 +192,6 @@ namespace smt {
|
|||
vector<objective_term> m_objectives;
|
||||
vector<rational> m_objective_consts;
|
||||
vector<vector<numeral> > m_objective_assignments;
|
||||
numeral m_objective_value;
|
||||
|
||||
// Set a conflict due to a negative cycle.
|
||||
void set_neg_cycle_conflict();
|
||||
|
|
|
@ -1007,9 +1007,9 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
|
|||
|
||||
IF_VERBOSE(1,
|
||||
for (unsigned i = 0; i < objective.size(); ++i) {
|
||||
verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
|
||||
verbose_stream() << "Coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
|
||||
}
|
||||
verbose_stream() << "free coefficient " << m_objective_consts[v] << "\n";);
|
||||
verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";);
|
||||
|
||||
// Objective coefficients now become balances
|
||||
vector<fin_numeral> balances(m_graph.get_num_nodes());
|
||||
|
@ -1018,24 +1018,33 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
|
|||
fin_numeral balance(objective[i].second);
|
||||
balances[objective[i].first] = balance;
|
||||
}
|
||||
|
||||
|
||||
network_flow<GExt> net_flow(m_graph, balances);
|
||||
bool is_optimal = net_flow.min_cost();
|
||||
if (is_optimal) {
|
||||
vector<numeral> potentials;
|
||||
m_objective_value = net_flow.get_optimal_solution(potentials, true);
|
||||
std::cout << "Objective value of var " << v << ": " << m_objective_value << std::endl;
|
||||
m_objective_assignments[v] = potentials;
|
||||
numeral objective_value = net_flow.get_optimal_solution(m_objective_assignments[v], true) + numeral(m_objective_consts[v]);
|
||||
IF_VERBOSE(1, verbose_stream() << "Optimal value of objective " << v << ": " << objective_value << std::endl;);
|
||||
|
||||
DEBUG_CODE(
|
||||
numeral initial_value = numeral(m_objective_consts[v]);
|
||||
for (unsigned i = 0; i < objective.size(); ++i) {
|
||||
initial_value += fin_numeral(objective[i].second) * m_graph.get_assignment(objective[i].first);
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "Initial value of objective " << v << ": " << initial_value << std::endl;);
|
||||
SASSERT(objective_value >= initial_value););
|
||||
|
||||
vector<numeral> & current_assigments = m_objective_assignments[v];
|
||||
SASSERT(!current_assigments.empty());
|
||||
TRACE("network_flow",
|
||||
for (unsigned i = 0; i < potentials.size(); ++i) {
|
||||
tout << "v" << i << " -> " << potentials[i] << "\n";
|
||||
for (unsigned i = 0; i < current_assigments.size(); ++i) {
|
||||
tout << "v" << i << " -> " << current_assigments[i] << std::endl;
|
||||
});
|
||||
rational r = m_objective_value.get_rational().to_rational();
|
||||
rational i = m_objective_value.get_infinitesimal().to_rational();
|
||||
rational r = objective_value.get_rational().to_rational();
|
||||
rational i = objective_value.get_infinitesimal().to_rational();
|
||||
return inf_eps_rational<inf_rational>(inf_rational(r, i));
|
||||
}
|
||||
else {
|
||||
std::cout << "Unbounded objective" << std::endl;
|
||||
IF_VERBOSE(1, verbose_stream() << "Unbounded objective" << std::endl;);
|
||||
return inf_eps_rational<inf_rational>::infinity();
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue