From 6ddc8386285cd9c1eff50640cb09b1112e25db0f Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 15 Nov 2013 18:34:05 -0800 Subject: [PATCH] Add a basic spanning tree --- src/smt/diff_logic.h | 82 +++++++++++++++++++++++++++++++++++++ src/smt/network_flow_def.h | 2 +- src/smt/spanning_tree.h | 21 +++++++--- src/smt/spanning_tree_def.h | 57 ++++++++++++++++++++++++++ 4 files changed, 155 insertions(+), 7 deletions(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index ff01a4792..fcd4f6309 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -25,6 +25,7 @@ Revision History: #include"trace.h" #include"warning.h" #include"uint_set.h" +#include typedef int dl_var; @@ -953,6 +954,87 @@ public: return m_edges; } + void get_neighbours_undirected(dl_var current, svector & neighbours) { + neighbours.reset(); + edge_id_vector & edges = m_out_edges[current]; + typename edge_id_vector::iterator it = edges.begin(), end = edges.end(); + for (; it != end; ++it) { + edge_id e_id = *it; + edge & e = m_edges[e_id]; + if (!e.is_enabled()) continue; + SASSERT(e.get_source() == current); + dl_var neighbour = e.get_target(); + neighbours.push_back(neighbour); + } + edges = m_in_edges[current]; + it = edges.begin(); + end = edges.end(); + for (; it != end; ++it) { + edge_id e_id = *it; + edge & e = m_edges[e_id]; + if (!e.is_enabled()) continue; + SASSERT(e.get_target() == current); + dl_var neighbour = e.get_source(); + neighbours.push_back(neighbour); + } + } + + void dfs_undirected(dl_var start, svector & threads) { + threads.reset(); + threads.resize(get_num_nodes()); + uint_set visited; + svector nodes; + nodes.push_back(start); + dl_var prev = -1; + while(!nodes.empty()) { + dl_var current = nodes.back(); + nodes.pop_back(); + visited.insert(current); + if (prev != -1) + threads[prev] = current; + prev = current; + svector neighbours; + get_neighbours_undirected(current, neighbours); + for (unsigned i = 0; i < neighbours.size(); ++i) { + edge_id id; + SASSERT(prev == -1 || get_edge_id(prev, current, id) || get_edge_id(current, prev, id)); + if (!visited.contains(neighbours[i])) { + nodes.push_back(neighbours[i]); + } + } + } + threads[prev] = start; + } + + void bfs_undirected(dl_var start, svector & parents, svector & depths) { + parents.reset(); + parents.resize(get_num_nodes()); + depths.reset(); + depths.resize(get_num_nodes()); + uint_set visited; + std::deque nodes; + visited.insert(start); + nodes.push_front(start); + while(!nodes.empty()) { + dl_var current = nodes.back(); + nodes.pop_back(); + SASSERT(visited.contains(current)); + svector neighbours; + get_neighbours_undirected(current, neighbours); + for (unsigned i = 0; i < neighbours.size(); ++i) { + dl_var & next = neighbours[i]; + edge_id id; + SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id)); + if (!visited.contains(next)) { + parents[next] = current; + depths[next] = depths[current] + 1; + visited.insert(next); + nodes.push_front(next); + } + } + } + } + template void enumerate_edges(dl_var source, dl_var target, Functor& f) { edge_id_vector & edges = m_out_edges[source]; diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 0ec7fe0c0..7af1a87ff 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -41,7 +41,7 @@ namespace smt { } } m_step = 0; - m_tree = alloc(thread_spanning_tree, m_graph); + m_tree = alloc(basic_spanning_tree, m_graph); } template diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index f5f6b624f..bce910b87 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -25,8 +25,8 @@ Notes: namespace smt { template - class thread_spanning_tree : public spanning_tree_base, private Ext { - private: + class thread_spanning_tree : public spanning_tree_base, protected Ext { + protected: typedef dl_var node; typedef dl_edge edge; typedef dl_graph graph; @@ -57,20 +57,29 @@ namespace smt { 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); + virtual void initialize(svector const & tree); void get_descendants(node start, svector & descendants); - void update(edge_id enter_id, edge_id leave_id); + virtual 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(); }; + template + class basic_spanning_tree : public thread_spanning_tree { + private: + graph * m_tree_graph; + + public: + basic_spanning_tree(graph & g); + void initialize(svector const & tree); + void update(edge_id enter_id, edge_id leave_id); + }; + } #endif diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index 281a2cf45..32b971c45 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -412,6 +412,63 @@ namespace smt { SASSERT(children.empty()); return true; } + + // Basic spanning tree + template + basic_spanning_tree::basic_spanning_tree(graph & g) : thread_spanning_tree(g) { + } + + template + void basic_spanning_tree::initialize(svector const & tree) { + unsigned num_nodes = m_graph.get_num_nodes(); + m_tree_graph = alloc(graph); + for (unsigned i = 0; i < num_nodes; ++i) { + m_tree_graph->init_var(i); + } + + vector const & es = m_graph.get_all_edges(); + svector::const_iterator it = tree.begin(), end = tree.end(); + for(; it != end; ++it) { + edge const & e = es[*it]; + m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation()); + } + + node root = num_nodes - 1; + m_tree_graph->bfs_undirected(root, m_pred, m_depth); + m_tree_graph->dfs_undirected(root, m_thread); + } + + template + void basic_spanning_tree::update(edge_id enter_id, edge_id leave_id) { + if (m_tree_graph) + dealloc(m_tree_graph); + m_tree_graph = alloc(graph); + unsigned num_nodes = m_graph.get_num_nodes(); + for (unsigned i = 0; i < num_nodes; ++i) { + m_tree_graph->init_var(i); + } + + vector const & es = m_graph.get_all_edges(); + svector::const_iterator it = m_tree.begin(), end = m_tree.end(); + for(; it != end; ++it) { + edge const & e = es[*it]; + if (leave_id != *it) { + m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation()); + } + } + m_tree_graph->add_edge(m_graph.get_source(enter_id), m_graph.get_target(enter_id), m_graph.get_weight(enter_id), explanation()); + + node root = num_nodes - 1; + 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]) { + edge_id id; + VERIFY(m_graph.get_edge_id(x, m_pred[x], id)); + m_tree[x] = id; + } + } + } #endif \ No newline at end of file