Add a basic spanning tree

src/smt/diff_logic.h

@@ -25,6 +25,7 @@ Revision History:
 #include"trace.h"
 #include"warning.h"
 #include"uint_set.h"
+#include<deque>
 
 typedef int dl_var;
 
@@ -953,6 +954,87 @@ public:
         return m_edges;
     }
 
+    void get_neighbours_undirected(dl_var current, svector<dl_var> & 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<dl_var> & threads) {
+        threads.reset();
+        threads.resize(get_num_nodes());
+	    uint_set visited;
+	    svector<dl_var> 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<dl_var> 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<dl_var> & parents, svector<dl_var> & depths) {
+        parents.reset();
+        parents.resize(get_num_nodes());
+        depths.reset();
+        depths.resize(get_num_nodes());
+	    uint_set visited;
+	    std::deque<dl_var> nodes;
+	    visited.insert(start);
+	    nodes.push_front(start);
+	    while(!nodes.empty()) {
+            dl_var current = nodes.back();
+            nodes.pop_back();
+		    SASSERT(visited.contains(current));
+            svector<dl_var> 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<typename Functor>
     void enumerate_edges(dl_var source, dl_var target, Functor& f) {
         edge_id_vector & edges = m_out_edges[source];

src/smt/network_flow_def.h

@@ -41,7 +41,7 @@ namespace smt {
             }
         }
         m_step = 0;
-        m_tree = alloc(thread_spanning_tree<Ext>, m_graph);
+        m_tree = alloc(basic_spanning_tree<Ext>, m_graph);
     }
 
     template<typename Ext>

src/smt/spanning_tree.h

@@ -25,8 +25,8 @@ Notes:
 namespace smt {
 
     template<typename Ext>
-    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<Ext> edge;
         typedef dl_graph<Ext> 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<edge_id> const & tree);
+        virtual void initialize(svector<edge_id> const & tree);
         void get_descendants(node start, svector<node> & 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<edge_id> & path, svector<bool> & against);              
         bool in_subtree_t2(node child);
 
         bool check_well_formed();        
     };
 
+    template<typename Ext>
+    class basic_spanning_tree : public thread_spanning_tree<Ext> {
+    private:
+        graph * m_tree_graph;
+
+    public:
+        basic_spanning_tree(graph & g);
+        void initialize(svector<edge_id> const & tree);
+        void update(edge_id enter_id, edge_id leave_id);
+    };
+
 }
 
 #endif

src/smt/spanning_tree_def.h

@@ -412,6 +412,63 @@ namespace smt {
         SASSERT(children.empty());
         return true;
     }
+
+    // Basic spanning tree
+    template<typename Ext>
+    basic_spanning_tree<Ext>::basic_spanning_tree(graph & g) : thread_spanning_tree<Ext>(g) {        
+    }
+
+    template<typename Ext>
+    void basic_spanning_tree<Ext>::initialize(svector<edge_id> 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<edge> const & es = m_graph.get_all_edges();
+        svector<edge_id>::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<typename Ext>
+    void basic_spanning_tree<Ext>::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<edge> const & es = m_graph.get_all_edges();
+        svector<edge_id>::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