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