12 #ifndef CPROVER_UTIL_GRAPH_H 13 #define CPROVER_UTIL_GRAPH_H 32 template<
class E=empty_edget>
39 typedef std::map<node_indext, edget>
edgest;
45 in.insert(std::pair<node_indext, edget>(n, edget()));
50 out.insert(std::pair<node_indext, edget>(n, edget()));
90 while(it_a!=a.end() && it_b!=b.end())
131 template<
class N=graph_nodet<empty_edget> >
147 node_indext no=nodes.size();
148 nodes.push_back(nodet());
154 nodes.swap(other.
nodes);
159 return nodes[i].out.find(j)!=nodes[i].out.end();
184 return nodes.empty();
187 const edgest &
in(node_indext n)
const 192 const edgest &
out(node_indext n)
const 205 nodes[a].erase_out(b);
206 nodes[b].erase_in(a);
209 edget &
edge(node_indext a, node_indext b)
211 return nodes[a].out[b];
214 void add_undirected_edge(node_indext a, node_indext b);
215 void remove_undirected_edge(node_indext a, node_indext b);
216 void remove_in_edges(node_indext n);
217 void remove_out_edges(node_indext n);
230 typedef std::list<node_indext>
patht;
237 shortest_path(src, dest, path,
false);
244 shortest_path(node, node, path,
true);
247 void visit_reachable(node_indext src);
252 std::size_t connected_subgraphs(
253 std::vector<node_indext> &subgraph_nr);
256 std::size_t SCCs(std::vector<node_indext> &subgraph_nr);
260 return empty() || !topsort().empty();
263 std::list<node_indext> topsort()
const;
265 void output_dot(std::ostream &out)
const;
266 void output_dot_node(std::ostream &out, node_indext n)
const;
281 tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
282 subgraph_nr(_subgraph_nr)
284 visited.resize(n,
false);
286 lowlink.resize(n, 0);
287 in_scc.resize(n,
false);
289 subgraph_nr.resize(n, 0);
293 void tarjan(
class tarjant &t, node_indext v);
299 bool non_trivial)
const;
305 assert(a<nodes.size());
306 assert(b<nodes.size());
329 nodet &node=nodes[n];
332 for(
typename edgest::const_iterator
344 nodet &node=nodes[n];
347 for(
typename edgest::const_iterator
361 bool non_trivial)
const 363 std::vector<bool> visited;
364 std::vector<unsigned> distance;
365 std::vector<unsigned> previous;
368 visited.resize(nodes.size(),
false);
369 distance.resize(nodes.size(), (unsigned)(-1));
370 previous.resize(nodes.size(), 0);
380 std::vector<node_indext> frontier_set, new_frontier_set;
382 frontier_set.reserve(nodes.size());
384 frontier_set.push_back(src);
389 while(!frontier_set.empty() && !found)
393 new_frontier_set.clear();
394 new_frontier_set.reserve(nodes.size());
396 for(
typename std::vector<node_indext>::const_iterator
397 f_it=frontier_set.begin();
398 f_it!=frontier_set.end() && !found;
402 const nodet &n=nodes[i];
405 for(
typename edgest::const_iterator
407 o_it!=n.
out.end() && !found;
421 new_frontier_set.push_back(o);
426 frontier_set.swap(new_frontier_set);
434 if(distance[dest]==(
unsigned)(-1))
439 path.push_front(dest);
440 if(distance[dest]==0 ||
441 previous[dest]==src)
break;
442 assert(dest!=previous[dest]);
452 std::stack<node_indext> s;
460 nodet &node=nodes[n];
463 for(
typename edgest::const_iterator
467 if(!nodes[it->first].visited)
474 std::vector<node_indext> &subgraph_nr)
476 std::vector<bool> visited;
478 visited.resize(nodes.size(),
false);
479 subgraph_nr.resize(nodes.size(), 0);
490 std::stack<node_indext> s;
501 const nodet &node=nodes[n];
503 for(
typename edgest::const_iterator
522 t.depth[v]=t.max_dfs;
523 t.lowlink[v]=t.max_dfs;
527 const nodet &node=nodes[v];
528 for(
typename edgest::const_iterator
537 t.lowlink[v]=std::min(t.lowlink[v], t.lowlink[vp]);
539 else if(t.in_scc[vp])
540 t.lowlink[v]=std::min(t.lowlink[v], t.depth[vp]);
544 if(t.lowlink[v]==t.depth[v])
548 assert(!t.scc_stack.empty());
552 t.subgraph_nr[vp]=t.scc_count;
564 tarjant t(nodes.size(), subgraph_nr);
584 const nodet &n=tmp[i];
588 for(
typename edgest::const_iterator
592 for(
typename edgest::const_iterator
600 this->add_undirected_edge(*it1, *it2);
615 std::list<node_indext> nodelist;
617 std::queue<node_indext> indeg0_nodes;
619 std::vector<size_t> in_deg(nodes.size(), 0);
624 in_deg[idx]=in(idx).size();
626 indeg0_nodes.push(idx);
629 while(!indeg0_nodes.empty())
633 nodelist.push_back(source);
635 for(
const auto &edge : out(source))
638 INVARIANT(in_deg[target]!=0,
"in-degree of node cannot be zero here");
643 if(in_deg[target]==0)
644 indeg0_nodes.push(target);
650 if(nodelist.size()!=nodes.size())
659 output_dot_node(out, n);
665 const nodet &node=nodes[n];
667 for(
typename edgest::const_iterator
671 out << n <<
" -> " << it->first <<
'\n';
674 #endif // CPROVER_UTIL_GRAPH_H void remove_in_edges(node_indext n)
A generic directed graph with a parametric node type.
std::vector< unsigned > lowlink
void add_undirected_edge(node_indext a, node_indext b)
std::size_t SCCs(std::vector< node_indext > &subgraph_nr)
A node type with an extra bit.
std::size_t connected_subgraphs(std::vector< node_indext > &subgraph_nr)
void visit_reachable(node_indext src)
#define INVARIANT(CONDITION, REASON)
void shortest_path(node_indext src, node_indext dest, patht &path) const
bool has_edge(node_indext i, node_indext j) const
void remove_edges(node_indext n)
void erase_in(node_indext n)
std::vector< bool > visited
const edgest & out(node_indext n) const
std::vector< bool > in_scc
std::list< node_indext > patht
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph...
nodet::node_indext node_indext
void tarjan(class tarjant &t, node_indext v)
void remove_undirected_edge(node_indext a, node_indext b)
void add_in(node_indext n)
edget & edge(node_indext a, node_indext b)
void output_dot(std::ostream &out) const
std::map< node_indext, edget > edgest
void erase_out(node_indext n)
void remove_edge(node_indext a, node_indext b)
const nodet & operator[](node_indext n) const
std::vector< node_indext > & subgraph_nr
void output_dot_node(std::ostream &out, node_indext n) const
void remove_out_edges(node_indext n)
std::stack< node_indext > scc_stack
void shortest_loop(node_indext node, patht &path) const
void add_edge(node_indext a, node_indext b)
std::vector< unsigned > depth
void add_out(node_indext n)
const edgest & in(node_indext n) const
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.
std::vector< nodet > nodest
tarjant(std::size_t n, std::vector< node_indext > &_subgraph_nr)
void resize(node_indext s)
nodet & operator[](node_indext n)
graph_nodet< E >::edgest edgest
This class represents a node in a directed graph.
graph_nodet< E >::edget edget