From 5a27c035e4c544ec48ae86c951e0c37a406db790 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 8 Nov 2013 18:00:48 -0800 Subject: [PATCH] Add a vector of edges to handle spanning trees --- src/smt/network_flow.h | 3 +- src/smt/network_flow_def.h | 95 ++++++++++++++++++----------------- src/smt/spanning_tree.h | 34 +++++++------ src/smt/spanning_tree_base.h | 10 ++-- src/smt/spanning_tree_def.h | 96 +++++++++++++++++++++--------------- 5 files changed, 129 insertions(+), 109 deletions(-) diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index 6ac46f0d5..44861575a 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -51,7 +51,7 @@ namespace smt { typedef typename Ext::fin_numeral fin_numeral; graph m_graph; - spanning_tree_base m_tree; + thread_spanning_tree m_tree; // Denote supply/demand b_i on node i vector m_balances; @@ -68,7 +68,6 @@ namespace smt { edge_id m_enter_id, m_leave_id; optional m_delta; - bool m_is_swap_enter, m_is_swap_leave; // Initialize the network with a feasible spanning tree void initialize(); diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index ca3e6db29..d31289dfc 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -27,7 +27,8 @@ namespace smt { template network_flow::network_flow(graph & g, vector const & balances) : - m_balances(balances) { + m_balances(balances), + m_tree(m_graph) { // Network flow graph has the edges in the reversed order compared to constraint graph // We only take enabled edges from the original graph for (unsigned i = 0; i < g.get_num_nodes(); ++i) { @@ -40,14 +41,13 @@ namespace smt { m_graph.add_edge(e.get_target(), e.get_source(), e.get_weight(), explanation()); } } - m_tree = thread_spanning_tree(m_graph); m_step = 0; } template void network_flow::initialize() { TRACE("network_flow", tout << "initialize...\n";); - // Create an artificial root node to construct initial spanning m_tree + // Create an artificial root node to construct initial spanning tree unsigned num_nodes = m_graph.get_num_nodes(); unsigned num_edges = m_graph.get_num_edges(); @@ -69,39 +69,44 @@ namespace smt { m_states.resize(num_nodes + num_edges); m_states.fill(LOWER); - // Create artificial edges from/to root node to/from other nodes and initialize the spanning m_tree - svector upwards(num_nodes, false); + // Create artificial edges from/to root node to/from other nodes and initialize the spanning tree + svector tree; + bool is_forward; for (unsigned i = 0; i < num_nodes; ++i) { - upwards[i] = !m_balances[i].is_neg(); + is_forward = !m_balances[i].is_neg(); m_states[num_edges + i] = BASIS; - node src = upwards[i] ? i : root; - node tgt = upwards[i] ? root : i; - m_flows[num_edges + i] = upwards[i] ? m_balances[i] : -m_balances[i]; - m_potentials[i] = upwards[i] ? numeral::one() : -numeral::one(); - m_graph.add_edge(src, tgt, numeral::one(), explanation()); + node src = is_forward ? i : root; + node tgt = is_forward ? root : i; + m_flows[num_edges + i] = is_forward ? m_balances[i] : -m_balances[i]; + m_potentials[i] = is_forward ? numeral::one() : -numeral::one(); + tree.push_back(m_graph.add_edge(src, tgt, numeral::one(), explanation())); } - m_tree.initialize(upwards); + m_tree.initialize(tree); TRACE("network_flow", { tout << pp_vector("Potentials", m_potentials, true) << pp_vector("Flows", m_flows); }); - TRACE("network_flow", tout << "Spanning m_tree:\n" << display_spanning_tree();); + TRACE("network_flow", tout << "Spanning tree:\n" << display_spanning_tree();); SASSERT(check_well_formed()); } template void network_flow::update_potentials() { node src = m_graph.get_source(m_enter_id); - node tgt = m_graph.get_target(m_enter_id); + node tgt = m_graph.get_target(m_enter_id); numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(m_enter_id); - numeral change = m_is_swap_leave ? -cost : cost; + numeral change = m_tree.in_subtree_t2(tgt) ? cost : -cost; + node start = m_graph.get_source(m_leave_id); + if (!m_tree.in_subtree_t2(start)) { + start = m_graph.get_target(m_leave_id);; + } + TRACE("network_flow", tout << "update_potentials of T_" << start << " with change = " << change << "...\n";); svector descendants; - node start = m_is_swap_enter ? src : tgt; - TRACE("network_flow", tout << "update_potentials of T_" << start << " with delta = " << change << "...\n";); m_tree.get_descendants(start, descendants); + SASSERT(descendants.size() >= 1); for (unsigned i = 0; i < descendants.size(); ++i) { - node u = descendants[i]; + node u = descendants[i]; m_potentials[u] += change; } TRACE("network_flow", tout << pp_vector("Potentials", m_potentials, true);); @@ -110,25 +115,25 @@ namespace smt { template void network_flow::update_flows() { TRACE("network_flow", tout << "update_flows...\n";); - numeral val = *m_delta; - m_flows[m_enter_id] += val; + 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); svector path; svector against; m_tree.get_path(src, tgt, path, against); + SASSERT(path.size() >= 1); for (unsigned i = 0; i < path.size(); ++i) { edge_id e_id = path[i]; - m_flows[e_id] += against[i] ? -val : val; + m_flows[e_id] += against[i] ? - *m_delta : *m_delta; } TRACE("network_flow", tout << pp_vector("Flows", m_flows, true);); } template bool network_flow::choose_entering_edge() { - TRACE("network_flow", tout << "choose_entering_edge...\n";); - vector const & es = m_graph.get_all_edges(); - for (unsigned i = 0; i < es.size(); ++i) { + TRACE("network_flow", tout << "choose_entering_edge...\n";); + unsigned num_edges = m_graph.get_num_edges(); + for (unsigned i = 0; i < num_edges; ++i) { node src = m_graph.get_source(i); node tgt = m_graph.get_target(i); if (m_states[i] != BASIS) { @@ -138,7 +143,7 @@ namespace smt { m_enter_id = i; TRACE("network_flow", { tout << "Found entering edge " << i << " between node "; - tout << src << " and node " << tgt << "...\n"; + tout << src << " and node " << tgt << " with reduced cost = " << cost << "...\n"; }); return true; } @@ -158,9 +163,10 @@ namespace smt { svector path; svector against; m_tree.get_path(src, tgt, path, against); + SASSERT(path.size() >= 1); for (unsigned i = 0; i < path.size(); ++i) { edge_id e_id = path[i]; - if (against[i] && (!m_delta || m_flows[e_id] <= *m_delta)) { + if (against[i] && (!m_delta || m_flows[e_id] < *m_delta)) { m_delta = m_flows[e_id]; leave_id = e_id; } @@ -182,7 +188,7 @@ namespace smt { template void network_flow::update_spanning_tree() { - m_tree.update(m_enter_id, m_leave_id, m_is_swap_enter, m_is_swap_leave); + m_tree.update(m_enter_id, m_leave_id); } // Minimize cost flows @@ -201,7 +207,7 @@ namespace smt { m_states[m_leave_id] = (m_flows[m_leave_id].is_zero()) ? LOWER : UPPER; update_spanning_tree(); update_potentials(); - TRACE("network_flow", tout << "Spanning m_tree:\n" << display_spanning_tree();); + TRACE("network_flow", tout << "Spanning tree:\n" << display_spanning_tree();); SASSERT(check_well_formed()); } else { @@ -217,12 +223,11 @@ namespace smt { template typename network_flow::numeral network_flow::get_optimal_solution(vector & result, bool is_dual) { numeral objective_value = numeral::zero(); - vector const & es = m_graph.get_all_edges(); - for (unsigned i = 0; i < es.size(); ++i) { - edge const & e = es[i]; + unsigned num_edges = m_graph.get_num_edges(); + for (unsigned i = 0; i < num_edges; ++i) { if (m_states[i] == BASIS) { - objective_value += e.get_weight().get_rational() * m_flows[i]; + objective_value += m_graph.get_weight(i).get_rational() * m_flows[i]; } } result.reset(); @@ -243,6 +248,7 @@ namespace smt { template bool network_flow::check_well_formed() { SASSERT(m_tree.check_well_formed()); + SASSERT(!m_delta || !(*m_delta).is_neg()); // m_flows are zero on non-basic edges for (unsigned i = 0; i < m_flows.size(); ++i) { @@ -250,11 +256,10 @@ namespace smt { SASSERT(m_states[i] == BASIS || m_flows[i].is_zero()); } - vector const & es = m_graph.get_all_edges(); - for (unsigned i = 0; i < es.size(); ++i) { - edge const & e = es[i]; + unsigned num_edges = m_graph.get_num_edges(); + for (unsigned i = 0; i < num_edges; ++i) { if (m_states[i] == BASIS) { - SASSERT(m_potentials[e.get_source()] - m_potentials[e.get_target()] == e.get_weight()); + SASSERT(m_potentials[m_graph.get_source(i)] - m_potentials[m_graph.get_target(i)] == m_graph.get_weight(i)); } } @@ -264,11 +269,10 @@ namespace smt { template bool network_flow::check_optimal() { numeral total_cost = numeral::zero(); - vector const & es = m_graph.get_all_edges(); - for (unsigned i = 0; i < es.size(); ++i) { - edge const & e = es[i]; + unsigned num_edges = m_graph.get_num_edges(); + for (unsigned i = 0; i < num_edges; ++i) { if (m_states[i] == BASIS) { - total_cost += e.get_weight().get_rational() * m_flows[i]; + total_cost += m_graph.get_weight(i).get_rational() * m_flows[i]; } } @@ -299,15 +303,14 @@ namespace smt { oss << prefix << root << "[shape=doublecircle,label=\"" << prefix << root << " ["; oss << m_potentials[root] << "/" << m_balances[root] << "]\"];\n"; - vector const & es = m_graph.get_all_edges(); - for (unsigned i = 0; i < es.size(); ++i) { - edge const & e = es[i]; - oss << prefix << e.get_source() << " -> " << prefix << e.get_target(); + unsigned num_edges = m_graph.get_num_edges(); + for (unsigned i = 0; i < num_edges; ++i) { + oss << prefix << m_graph.get_source(i) << " -> " << prefix << m_graph.get_target(i); if (m_states[i] == BASIS) { - oss << "[color=red,penwidth=3.0,label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n"; + oss << "[color=red,penwidth=3.0,label=\"" << m_flows[i] << "/" << m_graph.get_weight(i) << "\"];\n"; } else { - oss << "[label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n"; + oss << "[label=\"" << m_flows[i] << "/" << m_graph.get_weight(i) << "\"];\n"; } } oss << std::endl; diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index e085d4542..c591f5485 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -40,9 +40,10 @@ namespace smt { // Store the pointer from node i to the next node in depth-first search order svector m_thread; - // m_upwards[i] is true if the corresponding edge - // (i, m_pred[i]) points upwards (pointing toward the root node) - svector m_upwards; + // i |-> edge between (i, m_pred[i]) + svector m_tree; + + node m_root_t2; graph & m_graph; @@ -50,21 +51,24 @@ namespace smt { node find_rev_thread(node n) const; void fix_depth(node start, node end); node get_final(int start); - bool is_preorder_traversal(node start, node end); - edge_id get_edge_to_parent(node start) const; + bool is_preorder_traversal(node start, node end); node get_common_ancestor(node u, node v); - - public: - thread_spanning_tree(graph & g); - - void initialize(svector const & upwards); - void get_descendants(node start, svector & descendants); - - void update(edge_id enter_id, edge_id leave_id, bool & is_swap_enter, bool & is_swap_leave); - bool check_well_formed(); - void get_path(node start, node end, svector & path, svector & against); bool is_forward_edge(edge_id e_id) const; bool is_ancestor_of(node ancestor, node child); + + public: + thread_spanning_tree() {}; + thread_spanning_tree(graph & g); + ~thread_spanning_tree() {}; + + void initialize(svector const & tree); + void get_descendants(node start, svector & descendants); + + void update(edge_id enter_id, edge_id leave_id); + void get_path(node start, node end, svector & path, svector & against); + bool in_subtree_t2(node child); + + bool check_well_formed(); }; } diff --git a/src/smt/spanning_tree_base.h b/src/smt/spanning_tree_base.h index 17f49980c..e492f80fa 100644 --- a/src/smt/spanning_tree_base.h +++ b/src/smt/spanning_tree_base.h @@ -47,14 +47,14 @@ namespace smt { typedef int node; public: - virtual void initialize(svector const & upwards) {}; + virtual void initialize(svector const & tree) {}; virtual void get_descendants(node start, svector & descendants) {}; - virtual void update(edge_id enter_id, edge_id leave_id, bool & is_swap_enter, bool & is_swap_leave) {}; - virtual bool check_well_formed() {UNREACHABLE(); return false;}; + virtual void update(edge_id enter_id, edge_id leave_id) {}; virtual void get_path(node start, node end, svector & path, svector & against) {}; - virtual bool is_forward_edge(edge_id e_id) const {UNREACHABLE(); return false;}; - virtual bool is_ancestor_of(node ancestor, node child) {UNREACHABLE(); return false;}; + virtual bool in_subtree_t2(node child) {UNREACHABLE(); return false;}; + + virtual bool check_well_formed() {UNREACHABLE(); return false;}; }; } diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index fb2b3c6f3..2be593842 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -29,14 +29,15 @@ namespace smt { } template - void thread_spanning_tree::initialize(svector const & upwards) { + void thread_spanning_tree::initialize(svector const & tree) { + m_tree = tree; + unsigned num_nodes = m_graph.get_num_nodes(); m_pred.resize(num_nodes); m_depth.resize(num_nodes); m_thread.resize(num_nodes); - m_upwards.resize(num_nodes); - - node root = m_graph.get_num_nodes() - 1; + + node root = num_nodes - 1; m_pred[root] = -1; m_depth[root] = 0; m_thread[root] = 0; @@ -46,12 +47,11 @@ namespace smt { m_pred[i] = root; m_depth[i] = 1; m_thread[i] = i + 1; - m_upwards[i] = upwards[i]; } TRACE("network_flow", { tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread); - tout << pp_vector("Depths", m_depth) << pp_vector("Upwards", m_upwards); + tout << pp_vector("Depths", m_depth) << pp_vector("Tree", m_tree); }); } @@ -66,27 +66,18 @@ namespace smt { return u; } - template - edge_id thread_spanning_tree::get_edge_to_parent(node start) const { - SASSERT(m_pred[start] != -1); - edge_id id; - node end = m_pred[start]; - VERIFY(m_upwards[start] ? m_graph.get_edge_id(start, end, id) : m_graph.get_edge_id(end, start, id)); - return id; - } - template void thread_spanning_tree::get_path(node start, node end, svector & path, svector & against) { node join = get_common_ancestor(start, end); path.reset(); while (start != join) { - edge_id e_id = get_edge_to_parent(start); + edge_id e_id = m_tree[start]; path.push_back(e_id); against.push_back(is_forward_edge(e_id)); start = m_pred[start]; } while (end != join) { - edge_id e_id = get_edge_to_parent(end); + edge_id e_id = m_tree[end]; path.push_back(e_id); against.push_back(!is_forward_edge(e_id)); end = m_pred[end]; @@ -103,12 +94,22 @@ namespace smt { template void thread_spanning_tree::get_descendants(node start, svector & descendants) { - descendants.reset(); - node u = start; - while (m_depth[m_thread[u]] > m_depth[start]) { + descendants.reset(); + descendants.push_back(start); + node u = m_thread[start]; + while (m_depth[u] > m_depth[start]) { descendants.push_back(u); u = m_thread[u]; } + + } + + template + bool thread_spanning_tree::in_subtree_t2(node child) { + if (m_depth[child] < m_depth[m_root_t2]) { + return false; + } + return is_ancestor_of(m_root_t2, child); } template @@ -138,7 +139,7 @@ namespace smt { q q */ template - void thread_spanning_tree::update(edge_id enter_id, edge_id leave_id, bool & is_swap_enter, bool & is_swap_leave) { + void thread_spanning_tree::update(edge_id enter_id, edge_id leave_id) { node p = m_graph.get_source(enter_id); node q = m_graph.get_target(enter_id); node u = m_graph.get_source(leave_id); @@ -146,54 +147,61 @@ namespace smt { if (m_pred[u] == v) { std::swap(u, v); - is_swap_leave = true; - } - else { - is_swap_leave = false; } + SASSERT(m_pred[v] == u); - bool prev_upwards = false; if (is_ancestor_of(v, p)) { - std::swap(p, q); - prev_upwards = true; + std::swap(p, q); } - is_swap_enter = prev_upwards; SASSERT(is_ancestor_of(v, q)); - + TRACE("network_flow", { tout << "update_spanning_tree: (" << p << ", " << q << ") enters, ("; tout << u << ", " << v << ") leaves\n"; }); - // Update m_pred (for nodes in the stem from q to v) - // Note: m_pred[v] == u - // Initialize m_upwards[q] = q_upwards - node old_pred = m_pred[q]; + // Update stem nodes from q to v if (q != v) { for (node n = q; n != u; ) { SASSERT(old_pred != u || n == v); // the last processed node is v SASSERT(-1 != m_pred[old_pred]); int next_old_pred = m_pred[old_pred]; swap_order(n, old_pred); - std::swap(m_upwards[n], prev_upwards); - prev_upwards = !prev_upwards; // flip previous version of upwards. + m_tree[old_pred] = m_tree[n]; n = old_pred; old_pred = next_old_pred; } } - m_pred[q] = p; + else { + node x = get_final(p); + node y = m_thread[x]; + node z = get_final(q); + node t = m_thread[get_final(v)]; + node r = find_rev_thread(v); + m_thread[z] = y; + m_thread[x] = q; + m_thread[r] = t; + } - // m_thread were updated. - // update the depth. + m_pred[q] = p; + m_tree[q] = enter_id; + m_root_t2 = q; + + SASSERT(!in_subtree_t2(p)); + SASSERT(in_subtree_t2(q)); + SASSERT(!in_subtree_t2(u)); + SASSERT(in_subtree_t2(v)); + + // Update the depth. fix_depth(q, get_final(q)); TRACE("network_flow", { tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread); - tout << pp_vector("Depths", m_depth) << pp_vector("Upwards", m_upwards); + tout << pp_vector("Depths", m_depth) << pp_vector("Tree", m_tree); }); } @@ -263,7 +271,13 @@ namespace smt { // All nodes belong to the same spanning tree for (unsigned i = 0; i < roots.size(); ++i) { SASSERT(roots[i] + roots.size() == 0 || roots[i] >= 0); - } + } + + for (unsigned i = 0; i < m_tree.size(); ++i) { + node src = m_graph.get_source(m_tree[i]); + node tgt = m_graph.get_target(m_tree[i]); + SASSERT(m_pred[src] == tgt || m_pred[tgt] == src); + } return true; }