cprover
graph.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: A Template Class for Graphs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_GRAPH_H
13 #define CPROVER_UTIL_GRAPH_H
14 
15 #include <algorithm>
16 #include <cassert>
17 #include <functional>
18 #include <iosfwd>
19 #include <list>
20 #include <map>
21 #include <queue>
22 #include <sstream>
23 #include <stack>
24 #include <vector>
25 
26 #include "invariant.h"
27 
29 {
30 };
31 
34 template<class E=empty_edget>
36 {
37 public:
38  typedef std::size_t node_indext;
39 
40  typedef E edget;
41  typedef std::map<node_indext, edget> edgest;
42 
44 
46  {
47  in.insert(std::pair<node_indext, edget>(n, edget()));
48  }
49 
51  {
52  out.insert(std::pair<node_indext, edget>(n, edget()));
53  }
54 
56  {
57  in.erase(n);
58  }
59 
61  {
62  out.erase(n);
63  }
64 
65 private:
81  virtual std::string dot_attributes(const node_indext &) const
82  {
83  return "";
84  }
85 
86 public:
87  std::string pretty(const node_indext &idx) const
88  {
89  std::stringstream ss;
90  ss << std::to_string(idx) << " " << dot_attributes(idx);
91  return ss.str();
92  }
93 
94  virtual ~graph_nodet()
95  {
96  }
97 };
98 
100 template<class E>
101 class visited_nodet:public graph_nodet<E>
102 {
103 public:
104  typedef typename graph_nodet<E>::edget edget;
105  typedef typename graph_nodet<E>::edgest edgest;
106 
107  bool visited;
108 
110  {
111  }
112 };
113 
115 template<class E>
117  const typename graph_nodet<E>::edgest &a,
118  const typename graph_nodet<E>::edgest &b,
119  typename graph_nodet<E>::edgest &dest)
120 {
122  it_a=a.begin(),
123  it_b=b.begin();
124 
125  while(it_a!=a.end() && it_b!=b.end())
126  {
127  if(*it_a==*it_b)
128  {
129  dest.insert(*it_a);
130  it_a++;
131  it_b++;
132  }
133  else if(*it_a<*it_b)
134  it_a++;
135  else // *it_a>*it_b
136  it_b++;
137  }
138 }
139 
166 template<class N=graph_nodet<empty_edget> >
167 class grapht
168 {
169 public:
170  typedef N nodet;
171  typedef typename nodet::edgest edgest;
172  typedef std::vector<nodet> nodest;
173  typedef typename nodet::edget edget;
174  typedef typename nodet::node_indext node_indext;
175 
176 protected:
178 
179 public:
180  template <typename... arguments>
181  node_indext add_node(arguments &&... values)
182  {
183  node_indext no=nodes.size();
184  nodes.emplace_back(std::forward<arguments>(values)...);
185  return no;
186  }
187 
188  void swap(grapht &other)
189  {
190  nodes.swap(other.nodes);
191  }
192 
194  {
195  return nodes[i].out.find(j)!=nodes[i].out.end();
196  }
197 
198  const nodet &operator[](node_indext n) const
199  {
200  return nodes[n];
201  }
202 
204  {
205  return nodes[n];
206  }
207 
209  {
210  nodes.resize(s);
211  }
212 
213  std::size_t size() const
214  {
215  return nodes.size();
216  }
217 
218  bool empty() const
219  {
220  return nodes.empty();
221  }
222 
223  const edgest &in(node_indext n) const
224  {
225  return nodes[n].in;
226  }
227 
228  const edgest &out(node_indext n) const
229  {
230  return nodes[n].out;
231  }
232 
234  {
235  nodes[a].add_out(b);
236  nodes[b].add_in(a);
237  }
238 
240  {
241  nodes[a].erase_out(b);
242  nodes[b].erase_in(a);
243  }
244 
246  {
247  return nodes[a].out[b];
248  }
249 
254 
256  {
257  remove_in_edges(n);
258  remove_out_edges(n);
259  }
260 
261  void clear()
262  {
263  nodes.clear();
264  }
265 
266  typedef std::list<node_indext> patht;
267 
269  node_indext src,
270  node_indext dest,
271  patht &path) const
272  {
273  shortest_path(src, dest, path, false);
274  }
275 
277  node_indext node,
278  patht &path) const
279  {
280  shortest_path(node, node, path, true);
281  }
282 
284 
285  std::vector<node_indext> get_reachable(node_indext src, bool forwards) const;
286 
287  std::vector<node_indext>
288  get_reachable(const std::vector<node_indext> &src, bool forwards) const;
289 
291  void disconnect_unreachable(const std::vector<node_indext> &src);
292 
293  std::vector<typename N::node_indext>
294  depth_limited_search(typename N::node_indext src, std::size_t limit) const;
295 
296  std::vector<typename N::node_indext> depth_limited_search(
297  std::vector<typename N::node_indext> &src,
298  std::size_t limit) const;
299 
300  void make_chordal();
301 
302  // return value: number of connected subgraphs
303  std::size_t connected_subgraphs(
304  std::vector<node_indext> &subgraph_nr);
305 
306  // return value: number of SCCs
307  std::size_t SCCs(std::vector<node_indext> &subgraph_nr) const;
308 
309  bool is_dag() const
310  {
311  return empty() || !topsort().empty();
312  }
313 
314  std::list<node_indext> topsort() const;
315 
316  std::vector<node_indext> get_successors(const node_indext &n) const;
317  void output_dot(std::ostream &out) const;
319  const node_indext &n,
320  std::function<void(const node_indext &)> f) const;
321 
322 protected:
323  std::vector<typename N::node_indext> depth_limited_search(
324  std::vector<typename N::node_indext> &src,
325  std::size_t limit,
326  std::vector<bool> &visited) const;
327 
328  class tarjant
329  {
330  public:
331  std::vector<bool> visited;
332  std::vector<unsigned> depth;
333  std::vector<unsigned> lowlink;
334  std::vector<bool> in_scc;
335  std::stack<node_indext> scc_stack;
336  std::vector<node_indext> &subgraph_nr;
337 
338  std::size_t scc_count, max_dfs;
339 
340  tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
341  subgraph_nr(_subgraph_nr)
342  {
343  visited.resize(n, false);
344  depth.resize(n, 0);
345  lowlink.resize(n, 0);
346  in_scc.resize(n, false);
347  max_dfs=scc_count=0;
348  subgraph_nr.resize(n, 0);
349  }
350  };
351 
352  void tarjan(class tarjant &t, node_indext v) const;
353 
355  node_indext src,
356  node_indext dest,
357  patht &path,
358  bool non_trivial) const;
359 };
360 
361 template<class N>
363 {
364  PRECONDITION(a < nodes.size());
365  PRECONDITION(b < nodes.size());
366  nodet &na=nodes[a];
367  nodet &nb=nodes[b];
368  na.add_out(b);
369  nb.add_out(a);
370  na.add_in(b);
371  nb.add_in(a);
372 }
373 
374 template<class N>
376 {
377  nodet &na=nodes[a];
378  nodet &nb=nodes[b];
379  na.out.erase(b);
380  nb.out.erase(a);
381  na.in.erase(b);
382  nb.in.erase(a);
383 }
384 
385 template<class N>
387 {
388  nodet &node=nodes[n];
389 
390  // delete all incoming edges
391  for(typename edgest::const_iterator
392  it=node.in.begin();
393  it!=node.in.end();
394  it++)
395  nodes[it->first].erase_out(n);
396 
397  node.in.clear();
398 }
399 
400 template<class N>
402 {
403  nodet &node=nodes[n];
404 
405  // delete all outgoing edges
406  for(typename edgest::const_iterator
407  it=node.out.begin();
408  it!=node.out.end();
409  it++)
410  nodes[it->first].erase_in(n);
411 
412  node.out.clear();
413 }
414 
415 template<class N>
417  node_indext src,
418  node_indext dest,
419  patht &path,
420  bool non_trivial) const
421 {
422  std::vector<bool> visited;
423  std::vector<unsigned> distance;
424  std::vector<unsigned> previous;
425 
426  // initialization
427  visited.resize(nodes.size(), false);
428  distance.resize(nodes.size(), (unsigned)(-1));
429  previous.resize(nodes.size(), 0);
430 
431  if(!non_trivial)
432  {
433  distance[src]=0;
434  visited[src]=true;
435  }
436 
437  // does BFS, not Dijkstra
438  // we hope the graph is sparse
439  std::vector<node_indext> frontier_set, new_frontier_set;
440 
441  frontier_set.reserve(nodes.size());
442 
443  frontier_set.push_back(src);
444 
445  unsigned d=0;
446  bool found=false;
447 
448  while(!frontier_set.empty() && !found)
449  {
450  d++;
451 
452  new_frontier_set.clear();
453  new_frontier_set.reserve(nodes.size());
454 
455  for(typename std::vector<node_indext>::const_iterator
456  f_it=frontier_set.begin();
457  f_it!=frontier_set.end() && !found;
458  f_it++)
459  {
460  node_indext i=*f_it;
461  const nodet &n=nodes[i];
462 
463  // do all neighbors
464  for(typename edgest::const_iterator
465  o_it=n.out.begin();
466  o_it!=n.out.end() && !found;
467  o_it++)
468  {
469  node_indext o=o_it->first;
470 
471  if(!visited[o])
472  {
473  distance[o]=d;
474  previous[o]=i;
475  visited[o]=true;
476 
477  if(o==dest)
478  found=true;
479  else
480  new_frontier_set.push_back(o);
481  }
482  }
483  }
484 
485  frontier_set.swap(new_frontier_set);
486  }
487 
488  // compute path
489  // walk towards 0-distance node
490  path.clear();
491 
492  // reachable at all?
493  if(distance[dest]==(unsigned)(-1))
494  return; // nah
495 
496  while(true)
497  {
498  path.push_front(dest);
499  if(distance[dest]==0 ||
500  previous[dest]==src) break; // we are there
501  INVARIANT(
502  dest != previous[dest], "loops cannot be part of the shortest path");
503  dest=previous[dest];
504  }
505 }
506 
507 template<class N>
509 {
510  std::vector<node_indext> reachable = get_reachable(src, true);
511  for(const auto index : reachable)
512  nodes[index].visited = true;
513 }
514 
523 template <class N>
525 {
526  const std::vector<node_indext> source_nodes(1, src);
527  disconnect_unreachable(source_nodes);
528 }
529 
533 template <class N>
534 void grapht<N>::disconnect_unreachable(const std::vector<node_indext> &src)
535 {
536  std::vector<node_indext> reachable = get_reachable(src, true);
537  std::sort(reachable.begin(), reachable.end());
538  std::size_t reachable_idx = 0;
539  for(std::size_t i = 0; i < nodes.size(); i++)
540  {
541  // Holds since `reachable` contains node indices (i.e., all elements are
542  // smaller than `nodes.size()`), `reachable` is sorted, indices from `0` to
543  // `nodes.size()-1` are iterated over by variable i in order, and
544  // `reachable_idx` is only incremented when `i == reachable[reachable_idx]`
545  // holds.
546  INVARIANT(
547  reachable_idx >= reachable.size() || i <= reachable[reachable_idx],
548  "node index i is smaller or equal to the node index at "
549  "reachable[reachable_idx], when reachable_idx is within bounds");
550 
551  if(reachable_idx >= reachable.size())
552  remove_edges(i);
553  else if(i == reachable[reachable_idx])
554  reachable_idx++;
555  else
556  remove_edges(i);
557  }
558 }
559 
569 template <class Container, typename nodet = typename Container::value_type>
571  Container &set,
572  const std::function<void(
573  const typename Container::value_type &,
574  const std::function<void(const typename Container::value_type &)> &)>
575  &for_each_successor)
576 {
577  std::vector<nodet> stack;
578  for(const auto &elt : set)
579  stack.push_back(elt);
580 
581  while(!stack.empty())
582  {
583  auto n = stack.back();
584  stack.pop_back();
585  for_each_successor(n, [&](const nodet &node) {
586  if(set.insert(node).second)
587  stack.push_back(node);
588  });
589  }
590 }
591 
597 template<class N>
598 std::vector<typename N::node_indext>
599 grapht<N>::get_reachable(node_indext src, bool forwards) const
600 {
601  std::vector<node_indext> src_vector;
602  src_vector.push_back(src);
603 
604  return get_reachable(src_vector, forwards);
605 }
606 
612 template <class N>
613 std::vector<typename N::node_indext> grapht<N>::get_reachable(
614  const std::vector<node_indext> &src,
615  bool forwards) const
616 {
617  std::vector<node_indext> result;
618  std::vector<bool> visited(size(), false);
619 
620  std::stack<node_indext, std::vector<node_indext>> s(src);
621 
622  while(!s.empty())
623  {
624  node_indext n = s.top();
625  s.pop();
626 
627  if(visited[n])
628  continue;
629 
630  result.push_back(n);
631  visited[n] = true;
632 
633  const auto &node = nodes[n];
634  const auto &succs = forwards ? node.out : node.in;
635  for(const auto &succ : succs)
636  if(!visited[succ.first])
637  s.push(succ.first);
638  }
639 
640  return result;
641 }
642 
649 template <class N>
650 std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
651  const typename N::node_indext src,
652  std::size_t limit) const
653 {
654  std::vector<node_indext> start_vector(1, src);
655  return depth_limited_search(start_vector, limit);
656 }
657 
664 template <class N>
665 std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
666  std::vector<typename N::node_indext> &src,
667  std::size_t limit) const
668 {
669  std::vector<bool> visited(nodes.size(), false);
670 
671  for(const auto &node : src)
672  {
673  PRECONDITION(node < nodes.size());
674  visited[node] = true;
675  }
676 
677  return depth_limited_search(src, limit, visited);
678 }
679 
687 template <class N>
688 std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
689  std::vector<typename N::node_indext> &src,
690  std::size_t limit,
691  std::vector<bool> &visited) const
692 {
693  if(limit == 0)
694  return src;
695 
696  std::vector<node_indext> next_ring;
697 
698  for(const auto &n : src)
699  {
700  for(const auto &o : nodes[n].out)
701  {
702  if(!visited[o.first])
703  {
704  next_ring.push_back(o.first);
705  visited[o.first] = true;
706  }
707  }
708  }
709 
710  if(next_ring.empty())
711  return src;
712 
713  limit--;
714 
715  for(const auto &succ : depth_limited_search(next_ring, limit, visited))
716  src.push_back(succ);
717 
718  return src;
719 }
720 
726 template<class N>
728  std::vector<node_indext> &subgraph_nr)
729 {
730  std::vector<bool> visited;
731 
732  visited.resize(nodes.size(), false);
733  subgraph_nr.resize(nodes.size(), 0);
734 
735  std::size_t nr=0;
736 
737  for(node_indext src=0; src<size(); src++)
738  {
739  if(visited[src])
740  continue;
741 
742  // DFS
743 
744  std::stack<node_indext> s;
745  s.push(src);
746 
747  while(!s.empty())
748  {
749  node_indext n=s.top();
750  s.pop();
751 
752  visited[n]=true;
753  subgraph_nr[n]=nr;
754 
755  const nodet &node=nodes[n];
756 
757  for(const auto &o : node.out)
758  {
759  if(!visited[o.first])
760  s.push(o.first);
761  }
762  }
763 
764  nr++;
765  }
766 
767  return nr;
768 }
769 
770 template<class N>
772 {
773  t.scc_stack.push(v);
774  t.in_scc[v]=true;
775  t.depth[v]=t.max_dfs;
776  t.lowlink[v]=t.max_dfs;
777  t.visited[v]=true;
778  t.max_dfs++;
779 
780  const nodet &node=nodes[v];
781  for(typename edgest::const_iterator
782  it=node.out.begin();
783  it!=node.out.end();
784  it++)
785  {
786  node_indext vp=it->first;
787  if(!t.visited[vp])
788  {
789  tarjan(t, vp);
790  t.lowlink[v]=std::min(t.lowlink[v], t.lowlink[vp]);
791  }
792  else if(t.in_scc[vp])
793  t.lowlink[v]=std::min(t.lowlink[v], t.depth[vp]);
794  }
795 
796  // check if root of SCC
797  if(t.lowlink[v]==t.depth[v])
798  {
799  while(true)
800  {
801  INVARIANT(
802  !t.scc_stack.empty(),
803  "stack of strongly connected components should have another component");
804  node_indext vp=t.scc_stack.top();
805  t.scc_stack.pop();
806  t.in_scc[vp]=false;
807  t.subgraph_nr[vp]=t.scc_count;
808  if(vp==v)
809  break;
810  }
811 
812  t.scc_count++;
813  }
814 }
815 
828 template<class N>
829 std::size_t grapht<N>::SCCs(std::vector<node_indext> &subgraph_nr) const
830 {
831  tarjant t(nodes.size(), subgraph_nr);
832 
833  for(node_indext v0=0; v0<size(); v0++)
834  if(!t.visited[v0])
835  tarjan(t, v0);
836 
837  return t.scc_count;
838 }
839 
844 template<class N>
846 {
847  grapht tmp(*this);
848 
849  // This assumes an undirected graph.
850  // 1. remove all nodes in tmp, reconnecting the remaining ones
851  // 2. the chordal graph is the old one plus the new edges
852 
853  for(node_indext i=0; i<tmp.size(); i++)
854  {
855  const nodet &n=tmp[i];
856 
857  // connect all the nodes in n.out with each other
858  for(const auto &o1 : n.out)
859  for(const auto &o2 : n.out)
860  {
861  if(o1.first!=o2.first)
862  {
863  tmp.add_undirected_edge(o1.first, o2.first);
864  this->add_undirected_edge(o1.first, o2.first);
865  }
866  }
867 
868  // remove node from tmp graph
869  tmp.remove_edges(i);
870  }
871 }
872 
875 template<class N>
877 {
878  // list of topologically sorted nodes
879  std::list<node_indext> nodelist;
880  // queue of working set nodes with in-degree zero
881  std::queue<node_indext> indeg0_nodes;
882  // in-degree for each node
883  std::vector<size_t> in_deg(nodes.size(), 0);
884 
885  // abstract graph as in-degree of each node
886  for(node_indext idx=0; idx<nodes.size(); idx++)
887  {
888  in_deg[idx]=in(idx).size();
889  if(in_deg[idx]==0)
890  indeg0_nodes.push(idx);
891  }
892 
893  while(!indeg0_nodes.empty())
894  {
895  node_indext source=indeg0_nodes.front();
896  indeg0_nodes.pop();
897  nodelist.push_back(source);
898 
899  for(const auto &edge : out(source))
900  {
901  const node_indext target=edge.first;
902  INVARIANT(in_deg[target]!=0, "in-degree of node cannot be zero here");
903 
904  // remove edge from graph, by decrementing the in-degree of target
905  // outgoing edges from source will not be traversed again
906  in_deg[target]--;
907  if(in_deg[target]==0)
908  indeg0_nodes.push(target);
909  }
910  }
911 
912  // if all nodes are sorted, the graph is acyclic
913  // return empty list in case of cyclic graph
914  if(nodelist.size()!=nodes.size())
915  nodelist.clear();
916  return nodelist;
917 }
918 
919 template <typename node_index_type>
921  std::ostream &out,
922  const std::function<void(std::function<void(const node_index_type &)>)>
923  &for_each_node,
924  const std::function<
925  void(const node_index_type &, std::function<void(const node_index_type &)>)>
926  &for_each_succ,
927  const std::function<std::string(const node_index_type &)> node_to_string,
928  const std::function<std::string(const node_index_type &)> node_to_pretty)
929 {
930  for_each_node([&](const node_index_type &i) {
931  out << node_to_pretty(i) << ";\n";
932  for_each_succ(i, [&](const node_index_type &n) {
933  out << node_to_string(i) << " -> " << node_to_string(n) << '\n';
934  });
935  });
936 }
937 
938 template <class N>
941 {
942  std::vector<node_indext> result;
943  std::transform(
944  nodes[n].out.begin(),
945  nodes[n].out.end(),
946  std::back_inserter(result),
947  [&](const std::pair<node_indext, edget> &edge) { return edge.first; });
948  return result;
949 }
950 
951 template <class N>
953  const node_indext &n,
954  std::function<void(const node_indext &)> f) const
955 {
956  std::for_each(
957  nodes[n].out.begin(),
958  nodes[n].out.end(),
959  [&](const std::pair<node_indext, edget> &edge) { f(edge.first); });
960 }
961 
962 template <class N>
963 void grapht<N>::output_dot(std::ostream &out) const
964 {
965  const auto for_each_node =
966  [this](const std::function<void(const node_indext &)> &f) {
967  for(node_indext i = 0; i < nodes.size(); ++i)
968  f(i);
969  };
970 
971  const auto for_each_succ = [&](
972  const node_indext &i, const std::function<void(const node_indext &)> &f) {
973  for_each_successor(i, f);
974  };
975 
976  const auto to_string = [](const node_indext &i) { return std::to_string(i); };
977  const auto to_pretty_string = [this](const node_indext &i) {
978  return nodes[i].pretty(i);
979  };
980  output_dot_generic<node_indext>(
981  out, for_each_node, for_each_succ, to_string, to_pretty_string);
982 }
983 
984 #endif // CPROVER_UTIL_GRAPH_H
grapht::make_chordal
void make_chordal()
Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra ...
Definition: graph.h:845
empty_edget
Definition: graph.h:29
grapht::nodest
std::vector< nodet > nodest
Definition: graph.h:172
grapht::size
std::size_t size() const
Definition: graph.h:213
grapht::get_reachable
std::vector< node_indext > get_reachable(const std::vector< node_indext > &src, bool forwards) const
Run depth-first search on the graph, starting from multiple source nodes.
Definition: graph.h:613
grapht::remove_undirected_edge
void remove_undirected_edge(node_indext a, node_indext b)
Definition: graph.h:375
grapht::has_edge
bool has_edge(node_indext i, node_indext j) const
Definition: graph.h:193
graph_nodet::dot_attributes
virtual std::string dot_attributes(const node_indext &) const
Node with attributes suitable for Graphviz DOT format.
Definition: graph.h:81
grapht
A generic directed graph with a parametric node type.
Definition: graph.h:168
grapht::operator[]
const nodet & operator[](node_indext n) const
Definition: graph.h:198
grapht::tarjant::lowlink
std::vector< unsigned > lowlink
Definition: graph.h:333
grapht::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:181
grapht::disconnect_unreachable
void disconnect_unreachable(const std::vector< node_indext > &src)
Removes any edges between nodes in a graph that are unreachable from a vector of start nodes.
Definition: graph.h:534
grapht::shortest_loop
void shortest_loop(node_indext node, patht &path) const
Definition: graph.h:276
grapht::swap
void swap(grapht &other)
Definition: graph.h:188
graph_nodet::~graph_nodet
virtual ~graph_nodet()
Definition: graph.h:94
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
graph_nodet::add_out
void add_out(node_indext n)
Definition: graph.h:50
grapht::for_each_successor
void for_each_successor(const node_indext &n, std::function< void(const node_indext &)> f) const
Definition: graph.h:952
node_indext
std::size_t node_indext
Definition: destructor_tree.h:15
grapht::edgest
nodet::edgest edgest
Definition: graph.h:171
grapht::topsort
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.
Definition: graph.h:876
grapht::node_indext
nodet::node_indext node_indext
Definition: graph.h:174
grapht::connected_subgraphs
std::size_t connected_subgraphs(std::vector< node_indext > &subgraph_nr)
Find connected subgraphs in an undirected graph.
Definition: graph.h:727
graph_nodet::in
edgest in
Definition: graph.h:43
grapht::in
const edgest & in(node_indext n) const
Definition: graph.h:223
grapht::resize
void resize(node_indext s)
Definition: graph.h:208
grapht::shortest_path
void shortest_path(node_indext src, node_indext dest, patht &path, bool non_trivial) const
Definition: graph.h:416
intersection
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.
Definition: graph.h:116
graph_nodet::out
edgest out
Definition: graph.h:43
cfg_base_nodet::edgest
graph_nodet< empty_edget >::edgest edgest
Definition: cfg.h:30
visited_nodet
A node type with an extra bit.
Definition: graph.h:102
grapht::tarjant
Definition: graph.h:329
grapht::shortest_path
void shortest_path(node_indext src, node_indext dest, patht &path) const
Definition: graph.h:268
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
graph_nodet::add_in
void add_in(node_indext n)
Definition: graph.h:45
grapht::tarjant::scc_count
std::size_t scc_count
Definition: graph.h:338
get_reachable
void get_reachable(Container &set, const std::function< void(const typename Container::value_type &, const std::function< void(const typename Container::value_type &)> &)> &for_each_successor)
Add to set, nodes that are reachable from set.
Definition: graph.h:570
grapht::nodes
nodest nodes
Definition: graph.h:177
grapht::tarjant::visited
std::vector< bool > visited
Definition: graph.h:331
grapht::add_edge
void add_edge(node_indext a, node_indext b)
Definition: graph.h:233
output_dot_generic
void output_dot_generic(std::ostream &out, const std::function< void(std::function< void(const node_index_type &)>)> &for_each_node, const std::function< void(const node_index_type &, std::function< void(const node_index_type &)>)> &for_each_succ, const std::function< std::string(const node_index_type &)> node_to_string, const std::function< std::string(const node_index_type &)> node_to_pretty)
Definition: graph.h:920
graph_nodet::edgest
std::map< node_indext, edget > edgest
Definition: graph.h:41
grapht::tarjant::subgraph_nr
std::vector< node_indext > & subgraph_nr
Definition: graph.h:336
visited_nodet::visited
bool visited
Definition: graph.h:107
grapht::empty
bool empty() const
Definition: graph.h:218
grapht::SCCs
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
Definition: graph.h:829
grapht::tarjant::in_scc
std::vector< bool > in_scc
Definition: graph.h:334
visited_nodet::edgest
graph_nodet< E >::edgest edgest
Definition: graph.h:105
grapht::out
const edgest & out(node_indext n) const
Definition: graph.h:228
visited_nodet::edget
graph_nodet< E >::edget edget
Definition: graph.h:104
grapht::patht
std::list< node_indext > patht
Definition: graph.h:266
graph_nodet::pretty
std::string pretty(const node_indext &idx) const
Definition: graph.h:87
graph_nodet::edget
E edget
Definition: graph.h:40
graph_nodet
This class represents a node in a directed graph.
Definition: graph.h:36
grapht::operator[]
nodet & operator[](node_indext n)
Definition: graph.h:203
grapht::edge
edget & edge(node_indext a, node_indext b)
Definition: graph.h:245
grapht::tarjan
void tarjan(class tarjant &t, node_indext v) const
Definition: graph.h:771
grapht::get_successors
std::vector< node_indext > get_successors(const node_indext &n) const
Definition: graph.h:940
cfg_base_nodet::edget
graph_nodet< empty_edget >::edget edget
Definition: cfg.h:29
grapht::visit_reachable
void visit_reachable(node_indext src)
Definition: graph.h:508
grapht::disconnect_unreachable
void disconnect_unreachable(node_indext src)
Removes any edges between nodes in a graph that are unreachable from a given start node.
Definition: graph.h:524
invariant.h
grapht::is_dag
bool is_dag() const
Definition: graph.h:309
grapht::get_reachable
std::vector< node_indext > get_reachable(node_indext src, bool forwards) const
Run depth-first search on the graph, starting from a single source node.
Definition: graph.h:599
grapht::tarjant::scc_stack
std::stack< node_indext > scc_stack
Definition: graph.h:335
grapht::output_dot
void output_dot(std::ostream &out) const
Definition: graph.h:963
cfg_base_nodet
Definition: cfg.h:28
grapht::tarjant::tarjant
tarjant(std::size_t n, std::vector< node_indext > &_subgraph_nr)
Definition: graph.h:340
grapht::remove_in_edges
void remove_in_edges(node_indext n)
Definition: graph.h:386
graph_nodet::node_indext
std::size_t node_indext
Definition: graph.h:38
grapht::depth_limited_search
std::vector< typename N::node_indext > depth_limited_search(std::vector< typename N::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const
Run recursive depth-limited search on the graph, starting from multiple source nodes,...
Definition: graph.h:688
grapht::remove_edge
void remove_edge(node_indext a, node_indext b)
Definition: graph.h:239
graph_nodet::erase_in
void erase_in(node_indext n)
Definition: graph.h:55
grapht::clear
void clear()
Definition: graph.h:261
grapht::tarjant::max_dfs
std::size_t max_dfs
Definition: graph.h:338
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
grapht::remove_edges
void remove_edges(node_indext n)
Definition: graph.h:255
grapht::depth_limited_search
std::vector< typename N::node_indext > depth_limited_search(typename N::node_indext src, std::size_t limit) const
Run recursive depth-limited search on the graph, starting from multiple source nodes,...
Definition: graph.h:650
grapht::add_undirected_edge
void add_undirected_edge(node_indext a, node_indext b)
Definition: graph.h:362
grapht::edget
nodet::edget edget
Definition: graph.h:173
grapht::remove_out_edges
void remove_out_edges(node_indext n)
Definition: graph.h:401
grapht::tarjant::depth
std::vector< unsigned > depth
Definition: graph.h:332
grapht::depth_limited_search
std::vector< typename N::node_indext > depth_limited_search(std::vector< typename N::node_indext > &src, std::size_t limit) const
Run recursive depth-limited search on the graph, starting from multiple source nodes,...
Definition: graph.h:665
visited_nodet::visited_nodet
visited_nodet()
Definition: graph.h:109
grapht::nodet
N nodet
Definition: graph.h:170
graph_nodet::erase_out
void erase_out(node_indext n)
Definition: graph.h:60