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 <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 
66 template<class E>
67 class visited_nodet:public graph_nodet<E>
68 {
69 public:
70  typedef typename graph_nodet<E>::edget edget;
71  typedef typename graph_nodet<E>::edgest edgest;
72 
73  bool visited;
74 
76  {
77  }
78 };
79 
81 template<class E>
83  const typename graph_nodet<E>::edgest &a,
84  const typename graph_nodet<E>::edgest &b,
85  typename graph_nodet<E>::edgest &dest)
86 {
88  it_a=a.begin(),
89  it_b=b.begin();
90 
91  while(it_a!=a.end() && it_b!=b.end())
92  {
93  if(*it_a==*it_b)
94  {
95  dest.insert(*it_a);
96  it_a++;
97  it_b++;
98  }
99  else if(*it_a<*it_b)
100  it_a++;
101  else // *it_a>*it_b
102  it_b++;
103  }
104 }
105 
132 template<class N=graph_nodet<empty_edget> >
133 class grapht
134 {
135 public:
136  typedef N nodet;
137  typedef typename nodet::edgest edgest;
138  typedef std::vector<nodet> nodest;
139  typedef typename nodet::edget edget;
140  typedef typename nodet::node_indext node_indext;
141 
142 protected:
144 
145 public:
147  {
148  node_indext no=nodes.size();
149  nodes.push_back(nodet());
150  return no;
151  }
152 
153  void swap(grapht &other)
154  {
155  nodes.swap(other.nodes);
156  }
157 
159  {
160  return nodes[i].out.find(j)!=nodes[i].out.end();
161  }
162 
163  const nodet &operator[](node_indext n) const
164  {
165  return nodes[n];
166  }
167 
169  {
170  return nodes[n];
171  }
172 
174  {
175  nodes.resize(s);
176  }
177 
178  std::size_t size() const
179  {
180  return nodes.size();
181  }
182 
183  bool empty() const
184  {
185  return nodes.empty();
186  }
187 
188  const edgest &in(node_indext n) const
189  {
190  return nodes[n].in;
191  }
192 
193  const edgest &out(node_indext n) const
194  {
195  return nodes[n].out;
196  }
197 
199  {
200  nodes[a].add_out(b);
201  nodes[b].add_in(a);
202  }
203 
205  {
206  nodes[a].erase_out(b);
207  nodes[b].erase_in(a);
208  }
209 
211  {
212  return nodes[a].out[b];
213  }
214 
219 
221  {
222  remove_in_edges(n);
223  remove_out_edges(n);
224  }
225 
226  void clear()
227  {
228  nodes.clear();
229  }
230 
231  typedef std::list<node_indext> patht;
232 
234  node_indext src,
235  node_indext dest,
236  patht &path) const
237  {
238  shortest_path(src, dest, path, false);
239  }
240 
242  node_indext node,
243  patht &path) const
244  {
245  shortest_path(node, node, path, true);
246  }
247 
248  void visit_reachable(node_indext src);
249 
250  std::vector<node_indext> get_reachable(node_indext src, bool forwards) const;
251 
252  std::vector<node_indext>
253  get_reachable(const std::vector<node_indext> &src, bool forwards) const;
254 
255  void make_chordal();
256 
257  // return value: number of connected subgraphs
258  std::size_t connected_subgraphs(
259  std::vector<node_indext> &subgraph_nr);
260 
261  // return value: number of SCCs
262  std::size_t SCCs(std::vector<node_indext> &subgraph_nr) const;
263 
264  bool is_dag() const
265  {
266  return empty() || !topsort().empty();
267  }
268 
269  std::list<node_indext> topsort() const;
270 
271  std::vector<node_indext> get_successors(const node_indext &n) const;
272  void output_dot(std::ostream &out) const;
273  void for_each_successor(
274  const node_indext &n,
275  std::function<void(const node_indext &)> f) const;
276 
277 protected:
278  class tarjant
279  {
280  public:
281  std::vector<bool> visited;
282  std::vector<unsigned> depth;
283  std::vector<unsigned> lowlink;
284  std::vector<bool> in_scc;
285  std::stack<node_indext> scc_stack;
286  std::vector<node_indext> &subgraph_nr;
287 
288  std::size_t scc_count, max_dfs;
289 
290  tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
291  subgraph_nr(_subgraph_nr)
292  {
293  visited.resize(n, false);
294  depth.resize(n, 0);
295  lowlink.resize(n, 0);
296  in_scc.resize(n, false);
297  max_dfs=scc_count=0;
298  subgraph_nr.resize(n, 0);
299  }
300  };
301 
302  void tarjan(class tarjant &t, node_indext v) const;
303 
304  void shortest_path(
305  node_indext src,
306  node_indext dest,
307  patht &path,
308  bool non_trivial) const;
309 };
310 
311 template<class N>
313 {
314  assert(a<nodes.size());
315  assert(b<nodes.size());
316  nodet &na=nodes[a];
317  nodet &nb=nodes[b];
318  na.add_out(b);
319  nb.add_out(a);
320  na.add_in(b);
321  nb.add_in(a);
322 }
323 
324 template<class N>
326 {
327  nodet &na=nodes[a];
328  nodet &nb=nodes[b];
329  na.out.erase(b);
330  nb.out.erase(a);
331  na.in.erase(b);
332  nb.in.erase(a);
333 }
334 
335 template<class N>
337 {
338  nodet &node=nodes[n];
339 
340  // delete all incoming edges
341  for(typename edgest::const_iterator
342  it=node.in.begin();
343  it!=node.in.end();
344  it++)
345  nodes[it->first].erase_out(n);
346 
347  node.in.clear();
348 }
349 
350 template<class N>
352 {
353  nodet &node=nodes[n];
354 
355  // delete all outgoing edges
356  for(typename edgest::const_iterator
357  it=node.out.begin();
358  it!=node.out.end();
359  it++)
360  nodes[it->first].erase_in(n);
361 
362  node.out.clear();
363 }
364 
365 template<class N>
367  node_indext src,
368  node_indext dest,
369  patht &path,
370  bool non_trivial) const
371 {
372  std::vector<bool> visited;
373  std::vector<unsigned> distance;
374  std::vector<unsigned> previous;
375 
376  // initialization
377  visited.resize(nodes.size(), false);
378  distance.resize(nodes.size(), (unsigned)(-1));
379  previous.resize(nodes.size(), 0);
380 
381  if(!non_trivial)
382  {
383  distance[src]=0;
384  visited[src]=true;
385  }
386 
387  // does BFS, not Dijkstra
388  // we hope the graph is sparse
389  std::vector<node_indext> frontier_set, new_frontier_set;
390 
391  frontier_set.reserve(nodes.size());
392 
393  frontier_set.push_back(src);
394 
395  unsigned d=0;
396  bool found=false;
397 
398  while(!frontier_set.empty() && !found)
399  {
400  d++;
401 
402  new_frontier_set.clear();
403  new_frontier_set.reserve(nodes.size());
404 
405  for(typename std::vector<node_indext>::const_iterator
406  f_it=frontier_set.begin();
407  f_it!=frontier_set.end() && !found;
408  f_it++)
409  {
410  node_indext i=*f_it;
411  const nodet &n=nodes[i];
412 
413  // do all neighbors
414  for(typename edgest::const_iterator
415  o_it=n.out.begin();
416  o_it!=n.out.end() && !found;
417  o_it++)
418  {
419  node_indext o=o_it->first;
420 
421  if(!visited[o])
422  {
423  distance[o]=d;
424  previous[o]=i;
425  visited[o]=true;
426 
427  if(o==dest)
428  found=true;
429  else
430  new_frontier_set.push_back(o);
431  }
432  }
433  }
434 
435  frontier_set.swap(new_frontier_set);
436  }
437 
438  // compute path
439  // walk towards 0-distance node
440  path.clear();
441 
442  // reachable at all?
443  if(distance[dest]==(unsigned)(-1))
444  return; // nah
445 
446  while(true)
447  {
448  path.push_front(dest);
449  if(distance[dest]==0 ||
450  previous[dest]==src) break; // we are there
451  assert(dest!=previous[dest]);
452  dest=previous[dest];
453  }
454 }
455 
456 template<class N>
458 {
459  std::vector<node_indext> reachable = get_reachable(src, true);
460  for(const auto index : reachable)
461  nodes[index].visited = true;
462 }
463 
473 template <class Container, typename nodet = typename Container::value_type>
475  Container &set,
476  const std::function<void(
477  const typename Container::value_type &,
478  const std::function<void(const typename Container::value_type &)> &)>
479  &for_each_successor)
480 {
481  std::vector<nodet> stack;
482  for(const auto &elt : set)
483  stack.push_back(elt);
484 
485  while(!stack.empty())
486  {
487  auto n = stack.back();
488  stack.pop_back();
489  for_each_successor(n, [&](const nodet &node) {
490  if(set.insert(node).second)
491  stack.push_back(node);
492  });
493  }
494 }
495 
501 template<class N>
502 std::vector<typename N::node_indext>
503 grapht<N>::get_reachable(node_indext src, bool forwards) const
504 {
505  std::vector<node_indext> src_vector;
506  src_vector.push_back(src);
507 
508  return get_reachable(src_vector, forwards);
509 }
510 
516 template <class N>
517 std::vector<typename N::node_indext> grapht<N>::get_reachable(
518  const std::vector<node_indext> &src,
519  bool forwards) const
520 {
521  std::vector<node_indext> result;
522  std::vector<bool> visited(size(), false);
523 
524  std::stack<node_indext, std::vector<node_indext>> s(src);
525 
526  while(!s.empty())
527  {
528  node_indext n = s.top();
529  s.pop();
530 
531  if(visited[n])
532  continue;
533 
534  result.push_back(n);
535  visited[n] = true;
536 
537  const auto &node = nodes[n];
538  const auto &succs = forwards ? node.out : node.in;
539  for(const auto succ : succs)
540  if(!visited[succ.first])
541  s.push(succ.first);
542  }
543 
544  return result;
545 }
546 
547 template<class N>
549  std::vector<node_indext> &subgraph_nr)
550 {
551  std::vector<bool> visited;
552 
553  visited.resize(nodes.size(), false);
554  subgraph_nr.resize(nodes.size(), 0);
555 
556  std::size_t nr=0;
557 
558  for(node_indext src=0; src<size(); src++)
559  {
560  if(visited[src])
561  continue;
562 
563  // DFS
564 
565  std::stack<node_indext> s;
566  s.push(src);
567 
568  while(!s.empty())
569  {
570  node_indext n=s.top();
571  s.pop();
572 
573  visited[n]=true;
574  subgraph_nr[n]=nr;
575 
576  const nodet &node=nodes[n];
577 
578  for(typename edgest::const_iterator
579  it=node.out.begin();
580  it!=node.out.end();
581  it++)
582  if(!visited[*it])
583  s.push(*it);
584  }
585 
586  nr++;
587  }
588 
589  return nr;
590 }
591 
592 template<class N>
593 void grapht<N>::tarjan(tarjant &t, node_indext v) const
594 {
595  t.scc_stack.push(v);
596  t.in_scc[v]=true;
597  t.depth[v]=t.max_dfs;
598  t.lowlink[v]=t.max_dfs;
599  t.visited[v]=true;
600  t.max_dfs++;
601 
602  const nodet &node=nodes[v];
603  for(typename edgest::const_iterator
604  it=node.out.begin();
605  it!=node.out.end();
606  it++)
607  {
608  node_indext vp=it->first;
609  if(!t.visited[vp])
610  {
611  tarjan(t, vp);
612  t.lowlink[v]=std::min(t.lowlink[v], t.lowlink[vp]);
613  }
614  else if(t.in_scc[vp])
615  t.lowlink[v]=std::min(t.lowlink[v], t.depth[vp]);
616  }
617 
618  // check if root of SCC
619  if(t.lowlink[v]==t.depth[v])
620  {
621  while(true)
622  {
623  assert(!t.scc_stack.empty());
624  node_indext vp=t.scc_stack.top();
625  t.scc_stack.pop();
626  t.in_scc[vp]=false;
627  t.subgraph_nr[vp]=t.scc_count;
628  if(vp==v)
629  break;
630  }
631 
632  t.scc_count++;
633  }
634 }
635 
648 template<class N>
649 std::size_t grapht<N>::SCCs(std::vector<node_indext> &subgraph_nr) const
650 {
651  tarjant t(nodes.size(), subgraph_nr);
652 
653  for(node_indext v0=0; v0<size(); v0++)
654  if(!t.visited[v0])
655  tarjan(t, v0);
656 
657  return t.scc_count;
658 }
659 
660 template<class N>
662 {
663  grapht tmp(*this);
664 
665  // This assumes an undirected graph.
666  // 1. remove all nodes in tmp, reconnecting the remaining ones
667  // 2. the chordal graph is the old one plus the new edges
668 
669  for(node_indext i=0; i<tmp.size(); i++)
670  {
671  const nodet &n=tmp[i];
672 
673  // connect all the nodes in n.out with each other
674 
675  for(typename edgest::const_iterator
676  it1=n.out.begin();
677  it1!=n.out.end();
678  it1++)
679  for(typename edgest::const_iterator
680  it2=n.out.begin();
681  it2!=n.out.end();
682  it2++)
683  {
684  if(*it1!=*it2)
685  {
686  tmp.add_undirected_edge(*it1, *it2);
687  this->add_undirected_edge(*it1, *it2);
688  }
689  }
690 
691  // remove node from tmp graph
692  tmp.remove_edges(i);
693  }
694 }
695 
698 template<class N>
699 std::list<typename grapht<N>::node_indext> grapht<N>::topsort() const
700 {
701  // list of topologically sorted nodes
702  std::list<node_indext> nodelist;
703  // queue of working set nodes with in-degree zero
704  std::queue<node_indext> indeg0_nodes;
705  // in-degree for each node
706  std::vector<size_t> in_deg(nodes.size(), 0);
707 
708  // abstract graph as in-degree of each node
709  for(node_indext idx=0; idx<nodes.size(); idx++)
710  {
711  in_deg[idx]=in(idx).size();
712  if(in_deg[idx]==0)
713  indeg0_nodes.push(idx);
714  }
715 
716  while(!indeg0_nodes.empty())
717  {
718  node_indext source=indeg0_nodes.front();
719  indeg0_nodes.pop();
720  nodelist.push_back(source);
721 
722  for(const auto &edge : out(source))
723  {
724  const node_indext target=edge.first;
725  INVARIANT(in_deg[target]!=0, "in-degree of node cannot be zero here");
726 
727  // remove edge from graph, by decrementing the in-degree of target
728  // outgoing edges from source will not be traversed again
729  in_deg[target]--;
730  if(in_deg[target]==0)
731  indeg0_nodes.push(target);
732  }
733  }
734 
735  // if all nodes are sorted, the graph is acyclic
736  // return empty list in case of cyclic graph
737  if(nodelist.size()!=nodes.size())
738  nodelist.clear();
739  return nodelist;
740 }
741 
742 template <typename node_index_type>
744  std::ostream &out,
745  const std::function<void(std::function<void(const node_index_type &)>)>
746  &for_each_node,
747  const std::function<
748  void(const node_index_type &, std::function<void(const node_index_type &)>)>
749  &for_each_succ,
750  const std::function<std::string(const node_index_type &)> node_to_string)
751 {
752  for_each_node([&](const node_index_type &i) {
753  for_each_succ(i, [&](const node_index_type &n) {
754  out << node_to_string(i) << " -> " << node_to_string(n) << '\n';
755  });
756  });
757 }
758 
759 template <class N>
760 std::vector<typename grapht<N>::node_indext>
762 {
763  std::vector<node_indext> result;
764  std::transform(
765  nodes[n].out.begin(),
766  nodes[n].out.end(),
767  std::back_inserter(result),
768  [&](const std::pair<node_indext, edget> &edge) { return edge.first; });
769  return result;
770 }
771 
772 template <class N>
774  const node_indext &n,
775  std::function<void(const node_indext &)> f) const
776 {
777  std::for_each(
778  nodes[n].out.begin(),
779  nodes[n].out.end(),
780  [&](const std::pair<node_indext, edget> &edge) { f(edge.first); });
781 }
782 
783 template <class N>
784 void grapht<N>::output_dot(std::ostream &out) const
785 {
786  const auto for_each_node =
787  [&](const std::function<void(const node_indext &)> &f) {
788  for(node_indext i = 0; i < nodes.size(); ++i)
789  f(i);
790  };
791 
792  const auto for_each_succ = [&](
793  const node_indext &i, const std::function<void(const node_indext &)> &f) {
794  for_each_successor(i, f);
795  };
796 
797  const auto to_string = [](const node_indext &i) { return std::to_string(i); };
798  output_dot_generic<node_indext>(out, for_each_node, for_each_succ, to_string);
799 }
800 
801 #endif // CPROVER_UTIL_GRAPH_H
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)
Definition: graph.h:743
void remove_in_edges(node_indext n)
Definition: graph.h:336
std::size_t max_dfs
Definition: graph.h:288
A generic directed graph with a parametric node type.
Definition: graph.h:133
visited_nodet()
Definition: graph.h:75
nodest nodes
Definition: graph.h:143
std::vector< unsigned > lowlink
Definition: graph.h:283
void clear()
Definition: graph.h:226
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:649
void add_undirected_edge(node_indext a, node_indext b)
Definition: graph.h:312
A node type with an extra bit.
Definition: graph.h:67
std::size_t connected_subgraphs(std::vector< node_indext > &subgraph_nr)
Definition: graph.h:548
bool is_dag() const
Definition: graph.h:264
void visit_reachable(node_indext src)
Definition: graph.h:457
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
edgest in
Definition: graph.h:42
void shortest_path(node_indext src, node_indext dest, patht &path) const
Definition: graph.h:233
bool has_edge(node_indext i, node_indext j) const
Definition: graph.h:158
edgest out
Definition: graph.h:42
void remove_edges(node_indext n)
Definition: graph.h:220
nodet::edget edget
Definition: graph.h:139
void erase_in(node_indext n)
Definition: graph.h:54
std::vector< bool > visited
Definition: graph.h:281
N nodet
Definition: graph.h:136
bool visited
Definition: graph.h:73
const edgest & out(node_indext n) const
Definition: graph.h:193
std::list< path_nodet > patht
Definition: path.h:45
bool empty() const
Definition: graph.h:183
std::vector< bool > in_scc
Definition: graph.h:284
std::size_t size() const
Definition: graph.h:178
std::list< node_indext > patht
Definition: graph.h:231
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:699
nodet::node_indext node_indext
Definition: graph.h:140
void remove_undirected_edge(node_indext a, node_indext b)
Definition: graph.h:325
std::vector< node_indext > get_successors(const node_indext &n) const
Definition: graph.h:761
void add_in(node_indext n)
Definition: graph.h:44
edget & edge(node_indext a, node_indext b)
Definition: graph.h:210
std::size_t node_indext
Definition: graph.h:37
void output_dot(std::ostream &out) const
Definition: graph.h:784
std::map< node_indext, edget > edgest
Definition: graph.h:40
void tarjan(class tarjant &t, node_indext v) const
Definition: graph.h:593
void make_chordal()
Definition: graph.h:661
void erase_out(node_indext n)
Definition: graph.h:59
void remove_edge(node_indext a, node_indext b)
Definition: graph.h:204
const nodet & operator[](node_indext n) const
Definition: graph.h:163
std::size_t scc_count
Definition: graph.h:288
std::vector< node_indext > & subgraph_nr
Definition: graph.h:286
node_indext add_node()
Definition: graph.h:146
void for_each_successor(const node_indext &n, std::function< void(const node_indext &)> f) const
Definition: graph.h:773
void remove_out_edges(node_indext n)
Definition: graph.h:351
std::stack< node_indext > scc_stack
Definition: graph.h:285
nodet::edgest edgest
Definition: graph.h:137
void shortest_loop(node_indext node, patht &path) const
Definition: graph.h:241
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void add_edge(node_indext a, node_indext b)
Definition: graph.h:198
std::vector< unsigned > depth
Definition: graph.h:282
void add_out(node_indext n)
Definition: graph.h:49
const edgest & in(node_indext n) const
Definition: graph.h:188
void swap(grapht &other)
Definition: graph.h:153
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:82
std::vector< nodet > nodest
Definition: graph.h:138
tarjant(std::size_t n, std::vector< node_indext > &_subgraph_nr)
Definition: graph.h:290
void resize(node_indext s)
Definition: graph.h:173
E edget
Definition: graph.h:39
nodet & operator[](node_indext n)
Definition: graph.h:168
graph_nodet< E >::edgest edgest
Definition: graph.h:71
#define stack(x)
Definition: parser.h:144
This class represents a node in a directed graph.
Definition: graph.h:34
graph_nodet< E >::edget edget
Definition: graph.h:70
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:503
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:474