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 <list>
16 #include <stack>
17 #include <map>
18 #include <vector>
19 #include <ostream>
20 #include <cassert>
21 #include <algorithm>
22 #include <queue>
23 
24 #include "invariant.h"
25 
27 {
28 };
29 
32 template<class E=empty_edget>
34 {
35 public:
36  typedef std::size_t node_indext;
37 
38  typedef E edget;
39  typedef std::map<node_indext, edget> edgest;
40 
42 
44  {
45  in.insert(std::pair<node_indext, edget>(n, edget()));
46  }
47 
49  {
50  out.insert(std::pair<node_indext, edget>(n, edget()));
51  }
52 
54  {
55  in.erase(n);
56  }
57 
59  {
60  out.erase(n);
61  }
62 };
63 
65 template<class E>
66 class visited_nodet:public graph_nodet<E>
67 {
68 public:
69  typedef typename graph_nodet<E>::edget edget;
70  typedef typename graph_nodet<E>::edgest edgest;
71 
72  bool visited;
73 
75  {
76  }
77 };
78 
80 template<class E>
82  const typename graph_nodet<E>::edgest &a,
83  const typename graph_nodet<E>::edgest &b,
84  typename graph_nodet<E>::edgest &dest)
85 {
87  it_a=a.begin(),
88  it_b=b.begin();
89 
90  while(it_a!=a.end() && it_b!=b.end())
91  {
92  if(*it_a==*it_b)
93  {
94  dest.insert(*it_a);
95  it_a++;
96  it_b++;
97  }
98  else if(*it_a<*it_b)
99  it_a++;
100  else // *it_a>*it_b
101  it_b++;
102  }
103 }
104 
131 template<class N=graph_nodet<empty_edget> >
132 class grapht
133 {
134 public:
135  typedef N nodet;
136  typedef typename nodet::edgest edgest;
137  typedef std::vector<nodet> nodest;
138  typedef typename nodet::edget edget;
139  typedef typename nodet::node_indext node_indext;
140 
141 protected:
143 
144 public:
146  {
147  node_indext no=nodes.size();
148  nodes.push_back(nodet());
149  return no;
150  }
151 
152  void swap(grapht &other)
153  {
154  nodes.swap(other.nodes);
155  }
156 
158  {
159  return nodes[i].out.find(j)!=nodes[i].out.end();
160  }
161 
162  const nodet &operator[](node_indext n) const
163  {
164  return nodes[n];
165  }
166 
168  {
169  return nodes[n];
170  }
171 
173  {
174  nodes.resize(s);
175  }
176 
177  std::size_t size() const
178  {
179  return nodes.size();
180  }
181 
182  bool empty() const
183  {
184  return nodes.empty();
185  }
186 
187  const edgest &in(node_indext n) const
188  {
189  return nodes[n].in;
190  }
191 
192  const edgest &out(node_indext n) const
193  {
194  return nodes[n].out;
195  }
196 
198  {
199  nodes[a].add_out(b);
200  nodes[b].add_in(a);
201  }
202 
204  {
205  nodes[a].erase_out(b);
206  nodes[b].erase_in(a);
207  }
208 
210  {
211  return nodes[a].out[b];
212  }
213 
218 
220  {
221  remove_in_edges(n);
222  remove_out_edges(n);
223  }
224 
225  void clear()
226  {
227  nodes.clear();
228  }
229 
230  typedef std::list<node_indext> patht;
231 
233  node_indext src,
234  node_indext dest,
235  patht &path) const
236  {
237  shortest_path(src, dest, path, false);
238  }
239 
241  node_indext node,
242  patht &path) const
243  {
244  shortest_path(node, node, path, true);
245  }
246 
247  void visit_reachable(node_indext src);
248 
249  void make_chordal();
250 
251  // return value: number of connected subgraphs
252  std::size_t connected_subgraphs(
253  std::vector<node_indext> &subgraph_nr);
254 
255  // return value: number of SCCs
256  std::size_t SCCs(std::vector<node_indext> &subgraph_nr);
257 
258  bool is_dag() const
259  {
260  return empty() || !topsort().empty();
261  }
262 
263  std::list<node_indext> topsort() const;
264 
265  void output_dot(std::ostream &out) const;
266  void output_dot_node(std::ostream &out, node_indext n) const;
267 
268 protected:
269  class tarjant
270  {
271  public:
272  std::vector<bool> visited;
273  std::vector<unsigned> depth;
274  std::vector<unsigned> lowlink;
275  std::vector<bool> in_scc;
276  std::stack<node_indext> scc_stack;
277  std::vector<node_indext> &subgraph_nr;
278 
279  std::size_t scc_count, max_dfs;
280 
281  tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
282  subgraph_nr(_subgraph_nr)
283  {
284  visited.resize(n, false);
285  depth.resize(n, 0);
286  lowlink.resize(n, 0);
287  in_scc.resize(n, false);
288  max_dfs=scc_count=0;
289  subgraph_nr.resize(n, 0);
290  }
291  };
292 
293  void tarjan(class tarjant &t, node_indext v);
294 
295  void shortest_path(
296  node_indext src,
297  node_indext dest,
298  patht &path,
299  bool non_trivial) const;
300 };
301 
302 template<class N>
304 {
305  assert(a<nodes.size());
306  assert(b<nodes.size());
307  nodet &na=nodes[a];
308  nodet &nb=nodes[b];
309  na.add_out(b);
310  nb.add_out(a);
311  na.add_in(b);
312  nb.add_in(a);
313 }
314 
315 template<class N>
317 {
318  nodet &na=nodes[a];
319  nodet &nb=nodes[b];
320  na.out.erase(b);
321  nb.out.erase(a);
322  na.in.erase(b);
323  nb.in.erase(a);
324 }
325 
326 template<class N>
328 {
329  nodet &node=nodes[n];
330 
331  // delete all incoming edges
332  for(typename edgest::const_iterator
333  it=node.in.begin();
334  it!=node.in.end();
335  it++)
336  nodes[it->first].erase_out(n);
337 
338  node.in.clear();
339 }
340 
341 template<class N>
343 {
344  nodet &node=nodes[n];
345 
346  // delete all outgoing edges
347  for(typename edgest::const_iterator
348  it=node.out.begin();
349  it!=node.out.end();
350  it++)
351  nodes[it->first].erase_in(n);
352 
353  node.out.clear();
354 }
355 
356 template<class N>
358  node_indext src,
359  node_indext dest,
360  patht &path,
361  bool non_trivial) const
362 {
363  std::vector<bool> visited;
364  std::vector<unsigned> distance;
365  std::vector<unsigned> previous;
366 
367  // initialization
368  visited.resize(nodes.size(), false);
369  distance.resize(nodes.size(), (unsigned)(-1));
370  previous.resize(nodes.size(), 0);
371 
372  if(!non_trivial)
373  {
374  distance[src]=0;
375  visited[src]=true;
376  }
377 
378  // does BFS, not Dijkstra
379  // we hope the graph is sparse
380  std::vector<node_indext> frontier_set, new_frontier_set;
381 
382  frontier_set.reserve(nodes.size());
383 
384  frontier_set.push_back(src);
385 
386  unsigned d=0;
387  bool found=false;
388 
389  while(!frontier_set.empty() && !found)
390  {
391  d++;
392 
393  new_frontier_set.clear();
394  new_frontier_set.reserve(nodes.size());
395 
396  for(typename std::vector<node_indext>::const_iterator
397  f_it=frontier_set.begin();
398  f_it!=frontier_set.end() && !found;
399  f_it++)
400  {
401  node_indext i=*f_it;
402  const nodet &n=nodes[i];
403 
404  // do all neighbors
405  for(typename edgest::const_iterator
406  o_it=n.out.begin();
407  o_it!=n.out.end() && !found;
408  o_it++)
409  {
410  node_indext o=o_it->first;
411 
412  if(!visited[o])
413  {
414  distance[o]=d;
415  previous[o]=i;
416  visited[o]=true;
417 
418  if(o==dest)
419  found=true;
420  else
421  new_frontier_set.push_back(o);
422  }
423  }
424  }
425 
426  frontier_set.swap(new_frontier_set);
427  }
428 
429  // compute path
430  // walk towards 0-distance node
431  path.clear();
432 
433  // reachable at all?
434  if(distance[dest]==(unsigned)(-1))
435  return; // nah
436 
437  while(true)
438  {
439  path.push_front(dest);
440  if(distance[dest]==0 ||
441  previous[dest]==src) break; // we are there
442  assert(dest!=previous[dest]);
443  dest=previous[dest];
444  }
445 }
446 
447 template<class N>
449 {
450  // DFS
451 
452  std::stack<node_indext> s;
453  s.push(src);
454 
455  while(!s.empty())
456  {
457  node_indext n=s.top();
458  s.pop();
459 
460  nodet &node=nodes[n];
461  node.visited=true;
462 
463  for(typename edgest::const_iterator
464  it=node.out.begin();
465  it!=node.out.end();
466  it++)
467  if(!nodes[it->first].visited)
468  s.push(it->first);
469  }
470 }
471 
472 template<class N>
474  std::vector<node_indext> &subgraph_nr)
475 {
476  std::vector<bool> visited;
477 
478  visited.resize(nodes.size(), false);
479  subgraph_nr.resize(nodes.size(), 0);
480 
481  std::size_t nr=0;
482 
483  for(node_indext src=0; src<size(); src++)
484  {
485  if(visited[src])
486  continue;
487 
488  // DFS
489 
490  std::stack<node_indext> s;
491  s.push(src);
492 
493  while(!s.empty())
494  {
495  node_indext n=s.top();
496  s.pop();
497 
498  visited[n]=true;
499  subgraph_nr[n]=nr;
500 
501  const nodet &node=nodes[n];
502 
503  for(typename edgest::const_iterator
504  it=node.out.begin();
505  it!=node.out.end();
506  it++)
507  if(!visited[*it])
508  s.push(*it);
509  }
510 
511  nr++;
512  }
513 
514  return nr;
515 }
516 
517 template<class N>
518 void grapht<N>::tarjan(tarjant &t, node_indext v)
519 {
520  t.scc_stack.push(v);
521  t.in_scc[v]=true;
522  t.depth[v]=t.max_dfs;
523  t.lowlink[v]=t.max_dfs;
524  t.visited[v]=true;
525  t.max_dfs++;
526 
527  const nodet &node=nodes[v];
528  for(typename edgest::const_iterator
529  it=node.out.begin();
530  it!=node.out.end();
531  it++)
532  {
533  node_indext vp=it->first;
534  if(!t.visited[vp])
535  {
536  tarjan(t, vp);
537  t.lowlink[v]=std::min(t.lowlink[v], t.lowlink[vp]);
538  }
539  else if(t.in_scc[vp])
540  t.lowlink[v]=std::min(t.lowlink[v], t.depth[vp]);
541  }
542 
543  // check if root of SCC
544  if(t.lowlink[v]==t.depth[v])
545  {
546  while(true)
547  {
548  assert(!t.scc_stack.empty());
549  node_indext vp=t.scc_stack.top();
550  t.scc_stack.pop();
551  t.in_scc[vp]=false;
552  t.subgraph_nr[vp]=t.scc_count;
553  if(vp==v)
554  break;
555  }
556 
557  t.scc_count++;
558  }
559 }
560 
561 template<class N>
562 std::size_t grapht<N>::SCCs(std::vector<node_indext> &subgraph_nr)
563 {
564  tarjant t(nodes.size(), subgraph_nr);
565 
566  for(node_indext v0=0; v0<size(); v0++)
567  if(!t.visited[v0])
568  tarjan(t, v0);
569 
570  return t.scc_count;
571 }
572 
573 template<class N>
575 {
576  grapht tmp(*this);
577 
578  // This assumes an undirected graph.
579  // 1. remove all nodes in tmp, reconnecting the remaining ones
580  // 2. the chordal graph is the old one plus the new edges
581 
582  for(node_indext i=0; i<tmp.size(); i++)
583  {
584  const nodet &n=tmp[i];
585 
586  // connect all the nodes in n.out with each other
587 
588  for(typename edgest::const_iterator
589  it1=n.out.begin();
590  it1!=n.out.end();
591  it1++)
592  for(typename edgest::const_iterator
593  it2=n.out.begin();
594  it2!=n.out.end();
595  it2++)
596  {
597  if(*it1!=*it2)
598  {
599  tmp.add_undirected_edge(*it1, *it2);
600  this->add_undirected_edge(*it1, *it2);
601  }
602  }
603 
604  // remove node from tmp graph
605  tmp.remove_edges(i);
606  }
607 }
608 
611 template<class N>
612 std::list<typename grapht<N>::node_indext> grapht<N>::topsort() const
613 {
614  // list of topologically sorted nodes
615  std::list<node_indext> nodelist;
616  // queue of working set nodes with in-degree zero
617  std::queue<node_indext> indeg0_nodes;
618  // in-degree for each node
619  std::vector<size_t> in_deg(nodes.size(), 0);
620 
621  // abstract graph as in-degree of each node
622  for(node_indext idx=0; idx<nodes.size(); idx++)
623  {
624  in_deg[idx]=in(idx).size();
625  if(in_deg[idx]==0)
626  indeg0_nodes.push(idx);
627  }
628 
629  while(!indeg0_nodes.empty())
630  {
631  node_indext source=indeg0_nodes.front();
632  indeg0_nodes.pop();
633  nodelist.push_back(source);
634 
635  for(const auto &edge : out(source))
636  {
637  const node_indext target=edge.first;
638  INVARIANT(in_deg[target]!=0, "in-degree of node cannot be zero here");
639 
640  // remove edge from graph, by decrementing the in-degree of target
641  // outgoing edges from source will not be traversed again
642  in_deg[target]--;
643  if(in_deg[target]==0)
644  indeg0_nodes.push(target);
645  }
646  }
647 
648  // if all nodes are sorted, the graph is acyclic
649  // return empty list in case of cyclic graph
650  if(nodelist.size()!=nodes.size())
651  nodelist.clear();
652  return nodelist;
653 }
654 
655 template<class N>
656 void grapht<N>::output_dot(std::ostream &out) const
657 {
658  for(node_indext n=0; n<nodes.size(); n++)
659  output_dot_node(out, n);
660 }
661 
662 template<class N>
663 void grapht<N>::output_dot_node(std::ostream &out, node_indext n) const
664 {
665  const nodet &node=nodes[n];
666 
667  for(typename edgest::const_iterator
668  it=node.out.begin();
669  it!=node.out.end();
670  it++)
671  out << n << " -> " << it->first << '\n';
672 }
673 
674 #endif // CPROVER_UTIL_GRAPH_H
void remove_in_edges(node_indext n)
Definition: graph.h:327
std::size_t max_dfs
Definition: graph.h:279
A generic directed graph with a parametric node type.
Definition: graph.h:132
visited_nodet()
Definition: graph.h:74
nodest nodes
Definition: graph.h:142
std::vector< unsigned > lowlink
Definition: graph.h:274
void clear()
Definition: graph.h:225
void add_undirected_edge(node_indext a, node_indext b)
Definition: graph.h:303
std::size_t SCCs(std::vector< node_indext > &subgraph_nr)
Definition: graph.h:562
A node type with an extra bit.
Definition: graph.h:66
std::size_t connected_subgraphs(std::vector< node_indext > &subgraph_nr)
Definition: graph.h:473
bool is_dag() const
Definition: graph.h:258
void visit_reachable(node_indext src)
Definition: graph.h:448
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:202
edgest in
Definition: graph.h:41
void shortest_path(node_indext src, node_indext dest, patht &path) const
Definition: graph.h:232
bool has_edge(node_indext i, node_indext j) const
Definition: graph.h:157
edgest out
Definition: graph.h:41
void remove_edges(node_indext n)
Definition: graph.h:219
nodet::edget edget
Definition: graph.h:138
void erase_in(node_indext n)
Definition: graph.h:53
std::vector< bool > visited
Definition: graph.h:272
N nodet
Definition: graph.h:135
bool visited
Definition: graph.h:72
const edgest & out(node_indext n) const
Definition: graph.h:192
std::list< path_nodet > patht
Definition: path.h:45
bool empty() const
Definition: graph.h:182
std::vector< bool > in_scc
Definition: graph.h:275
std::size_t size() const
Definition: graph.h:177
std::list< node_indext > patht
Definition: graph.h:230
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:612
nodet::node_indext node_indext
Definition: graph.h:139
void tarjan(class tarjant &t, node_indext v)
Definition: graph.h:518
void remove_undirected_edge(node_indext a, node_indext b)
Definition: graph.h:316
void add_in(node_indext n)
Definition: graph.h:43
edget & edge(node_indext a, node_indext b)
Definition: graph.h:209
std::size_t node_indext
Definition: graph.h:36
void output_dot(std::ostream &out) const
Definition: graph.h:656
std::map< node_indext, edget > edgest
Definition: graph.h:39
void make_chordal()
Definition: graph.h:574
void erase_out(node_indext n)
Definition: graph.h:58
void remove_edge(node_indext a, node_indext b)
Definition: graph.h:203
const nodet & operator[](node_indext n) const
Definition: graph.h:162
std::size_t scc_count
Definition: graph.h:279
std::vector< node_indext > & subgraph_nr
Definition: graph.h:277
node_indext add_node()
Definition: graph.h:145
void output_dot_node(std::ostream &out, node_indext n) const
Definition: graph.h:663
void remove_out_edges(node_indext n)
Definition: graph.h:342
std::stack< node_indext > scc_stack
Definition: graph.h:276
nodet::edgest edgest
Definition: graph.h:136
void shortest_loop(node_indext node, patht &path) const
Definition: graph.h:240
void add_edge(node_indext a, node_indext b)
Definition: graph.h:197
std::vector< unsigned > depth
Definition: graph.h:273
void add_out(node_indext n)
Definition: graph.h:48
const edgest & in(node_indext n) const
Definition: graph.h:187
void swap(grapht &other)
Definition: graph.h:152
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:81
std::vector< nodet > nodest
Definition: graph.h:137
tarjant(std::size_t n, std::vector< node_indext > &_subgraph_nr)
Definition: graph.h:281
void resize(node_indext s)
Definition: graph.h:172
E edget
Definition: graph.h:38
nodet & operator[](node_indext n)
Definition: graph.h:167
graph_nodet< E >::edgest edgest
Definition: graph.h:70
This class represents a node in a directed graph.
Definition: graph.h:33
graph_nodet< E >::edget edget
Definition: graph.h:69