|
CBMC
|
A Template Class for Graphs. More...
#include <algorithm>#include <functional>#include <iosfwd>#include <list>#include <map>#include <queue>#include <sstream>#include <stack>#include <vector>#include "invariant.h"
Include dependency graph for graph.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | empty_edget |
| class | graph_nodet< E > |
| This class represents a node in a directed graph. More... | |
| class | visited_nodet< E > |
| A node type with an extra bit. More... | |
| class | grapht< N > |
| A generic directed graph with a parametric node type. More... | |
| class | grapht< N >::tarjant |
Functions | |
| template<class E > | |
| 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. | |
| template<class Container , typename nodet = typename Container::value_type> | |
| 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. | |
| template<typename node_index_type > | |
| 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) |
A Template Class for Graphs.
Definition in file graph.h.
| 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.
This implements a depth first search using a stack: at each step we pop a node, and push on the stack all its successors that have not yet been visited.
| set | set of source nodes, must be a container with an insert(const value_type&) method. |
| for_each_successor | function which given a node n and a function f, applies f on all successors of n. |
| void intersection | ( | const typename graph_nodet< E >::edgest & | a, |
| const typename graph_nodet< E >::edgest & | b, | ||
| typename graph_nodet< E >::edgest & | dest | ||
| ) |
| 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 | ||
| ) |