cprover
grapht< N > Class Template Reference

A generic directed graph with a parametric node type. More...

#include <graph.h>

Inheritance diagram for grapht< N >:
[legend]
Collaboration diagram for grapht< N >:
[legend]

Classes

class  tarjant
 

Public Types

typedef N nodet
 
typedef nodet::edgest edgest
 
typedef std::vector< nodetnodest
 
typedef nodet::edget edget
 
typedef nodet::node_indext node_indext
 
typedef std::list< node_indextpatht
 

Public Member Functions

node_indext add_node ()
 
void swap (grapht &other)
 
bool has_edge (node_indext i, node_indext j) const
 
const nodetoperator[] (node_indext n) const
 
nodetoperator[] (node_indext n)
 
void resize (node_indext s)
 
std::size_t size () const
 
bool empty () const
 
const edgestin (node_indext n) const
 
const edgestout (node_indext n) const
 
void add_edge (node_indext a, node_indext b)
 
void remove_edge (node_indext a, node_indext b)
 
edgetedge (node_indext a, node_indext b)
 
void add_undirected_edge (node_indext a, node_indext b)
 
void remove_undirected_edge (node_indext a, node_indext b)
 
void remove_in_edges (node_indext n)
 
void remove_out_edges (node_indext n)
 
void remove_edges (node_indext n)
 
void clear ()
 
void shortest_path (node_indext src, node_indext dest, patht &path) const
 
void shortest_loop (node_indext node, patht &path) const
 
void visit_reachable (node_indext src)
 
std::vector< node_indextget_reachable (node_indext src, bool forwards) const
 Run depth-first search on the graph, starting from a single source node. More...
 
std::vector< node_indextget_reachable (const std::vector< node_indext > &src, bool forwards) const
 Run depth-first search on the graph, starting from multiple source nodes. More...
 
void disconnect_unreachable (node_indext src)
 Removes any edges between nodes in a graph that are unreachable from a given start node. More...
 
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. More...
 
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, to find the nodes reachable within n steps. More...
 
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, to find the nodes reachable within n steps. More...
 
void make_chordal ()
 Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges. More...
 
std::size_t connected_subgraphs (std::vector< node_indext > &subgraph_nr)
 Find connected subgraphs in an undirected graph. More...
 
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 to components indices. More...
 
bool is_dag () const
 
std::list< node_indexttopsort () const
 Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph. More...
 
std::vector< node_indextget_successors (const node_indext &n) const
 
void output_dot (std::ostream &out) const
 
void for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const
 

Protected Member Functions

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. More...
 
void tarjan (class tarjant &t, node_indext v) const
 
void shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const
 

Protected Attributes

nodest nodes
 

Detailed Description

template<class N = graph_nodet<empty_edget>>
class grapht< N >

A generic directed graph with a parametric node type.

The nodes of the graph are stored in the only field of the class, a std::vector named nodes. Nodes are instances of class graph_nodet<E> or a subclass of it. Graph edges contain a payload object of parametric type E (which has to be default-constructible). By default E is instantiated with an empty class (empty_edget).

Each node is identified by its offset inside the nodes vector. The incoming and outgoing edges of a node are stored as std::maps in the fields in and out of the graph_nodet<E>. These maps associate a node identifier (the offset) to the edge payload (of type E).

In fact, observe that two instances of E are stored per edge of the graph. For instance, assume that we want to create a graph with two nodes, A and B, and one edge from A to B, labelled by object e. We achieve this by inserting the pair (offsetof(B),e) in the map A.out and the pair (offsetof(A),e) in the map B.in.

Nodes are inserted in the graph using grapht::add_node(), which returns the identifier (offset) of the inserted node. Edges between nodes are created by grapht::add_edge(a,b), where a and b are the identifiers of nodes. Method add_edges adds a default-constructed payload object of type E. Adding a payload objet e to an edge seems to be only possibly by manually inserting e in the std::maps in and out of the two nodes associated to the edge.

Definition at line 133 of file graph.h.

Member Typedef Documentation

◆ edgest

template<class N = graph_nodet<empty_edget>>
typedef nodet::edgest grapht< N >::edgest

Definition at line 137 of file graph.h.

◆ edget

template<class N = graph_nodet<empty_edget>>
typedef nodet::edget grapht< N >::edget

Definition at line 139 of file graph.h.

◆ node_indext

template<class N = graph_nodet<empty_edget>>
typedef nodet::node_indext grapht< N >::node_indext

Definition at line 140 of file graph.h.

◆ nodest

template<class N = graph_nodet<empty_edget>>
typedef std::vector<nodet> grapht< N >::nodest

Definition at line 138 of file graph.h.

◆ nodet

template<class N = graph_nodet<empty_edget>>
typedef N grapht< N >::nodet

Definition at line 136 of file graph.h.

◆ patht

template<class N = graph_nodet<empty_edget>>
typedef std::list<node_indext> grapht< N >::patht

Definition at line 231 of file graph.h.

Member Function Documentation

◆ add_edge()

◆ add_node()

◆ add_undirected_edge()

template<class N >
void grapht< N >::add_undirected_edge ( node_indext  a,
node_indext  b 
)

Definition at line 327 of file graph.h.

Referenced by grapht< abstract_eventt >::make_chordal().

◆ clear()

template<class N = graph_nodet<empty_edget>>
void grapht< N >::clear ( void  )
inline

Definition at line 226 of file graph.h.

Referenced by event_grapht::clear().

◆ connected_subgraphs()

template<class N >
std::size_t grapht< N >::connected_subgraphs ( std::vector< node_indext > &  subgraph_nr)

Find connected subgraphs in an undirected graph.

Parameters
[out]subgraph_nrwill be resized to graph.size() and populated to map node indices onto subgraph numbers. The subgraph numbers are dense, in the range 0 - (number of subgraphs - 1)
Returns
Number of subgraphs found.

Definition at line 682 of file graph.h.

◆ depth_limited_search() [1/3]

template<class N>
std::vector< typename N::node_indext > grapht< N >::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, to find the nodes reachable within n steps.

This function initialises the search.

Parameters
srcThe node to start the search from.
limitlimit on steps
Returns
a vector of reachable node indices

Definition at line 606 of file graph.h.

Referenced by get_functions_reachable_within_n_steps().

◆ depth_limited_search() [2/3]

template<class N>
std::vector< typename N::node_indext > grapht< N >::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, to find the nodes reachable within n steps.

This function initialises the search.

Parameters
srcThe nodes to start the search from.
limitlimit on steps
Returns
a vector of reachable node indices

Definition at line 621 of file graph.h.

◆ depth_limited_search() [3/3]

template<class N>
std::vector< typename N::node_indext > grapht< N >::depth_limited_search ( std::vector< typename N::node_indext > &  src,
std::size_t  limit,
std::vector< bool > &  visited 
) const
protected

Run recursive depth-limited search on the graph, starting.

Parameters
srcThe nodes to start the search from.
limitlimit on steps
visitedvector of booleans indicating whether a node has been visited
Returns
a vector of reachable node indices

Definition at line 643 of file graph.h.

◆ disconnect_unreachable() [1/2]

template<class N >
void grapht< N >::disconnect_unreachable ( node_indext  src)

Removes any edges between nodes in a graph that are unreachable from a given start node.

Used for computing cone of influence, by disconnecting unreachable nodes and then performing backwards reachability. Note nodes are not actually removed from the vector nodes, because this requires renumbering node indices. This copies the way nodes are "removed" in make_chordal.

Parameters
srcstart node

Definition at line 488 of file graph.h.

Referenced by disconnect_unreachable_functions().

◆ disconnect_unreachable() [2/2]

template<class N >
void grapht< N >::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.

Parameters
srcvector of indices of start nodes

Definition at line 498 of file graph.h.

◆ edge()

template<class N = graph_nodet<empty_edget>>
edget& grapht< N >::edge ( node_indext  a,
node_indext  b 
)
inline

Definition at line 210 of file graph.h.

◆ empty()

template<class N = graph_nodet<empty_edget>>
bool grapht< N >::empty ( ) const
inline

◆ for_each_successor()

template<class N >
void grapht< N >::for_each_successor ( const node_indext n,
std::function< void(const node_indext &)>  f 
) const

Definition at line 903 of file graph.h.

◆ get_reachable() [1/2]

template<class N >
std::vector< typename N::node_indext > grapht< N >::get_reachable ( node_indext  src,
bool  forwards 
) const

Run depth-first search on the graph, starting from a single source node.

Parameters
srcThe node to start the search from.
forwardstrue (false) if the forward (backward) reachability should be performed.

Definition at line 555 of file graph.h.

Referenced by get_connected_functions().

◆ get_reachable() [2/2]

template<class N >
std::vector< typename N::node_indext > grapht< N >::get_reachable ( const std::vector< node_indext > &  src,
bool  forwards 
) const

Run depth-first search on the graph, starting from multiple source nodes.

Parameters
srcThe nodes to start the search from.
forwardstrue (false) if the forward (backward) reachability should be performed.

Definition at line 569 of file graph.h.

◆ get_successors()

template<class N >
std::vector< typename grapht< N >::node_indext > grapht< N >::get_successors ( const node_indext n) const

Definition at line 891 of file graph.h.

◆ has_edge()

template<class N = graph_nodet<empty_edget>>
bool grapht< N >::has_edge ( node_indext  i,
node_indext  j 
) const
inline

◆ in()

template<class N = graph_nodet<empty_edget>>
const edgest& grapht< N >::in ( node_indext  n) const
inline

◆ is_dag()

template<class N = graph_nodet<empty_edget>>
bool grapht< N >::is_dag ( ) const
inline

Definition at line 274 of file graph.h.

◆ make_chordal()

template<class N >
void grapht< N >::make_chordal ( )

Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges.

Note this adds more edges than are required, including to acyclic graphs or acyclic subgraphs of cyclic graphs, but does at least ensure the graph is not chordal.

Definition at line 798 of file graph.h.

◆ operator[]() [1/2]

template<class N = graph_nodet<empty_edget>>
const nodet& grapht< N >::operator[] ( node_indext  n) const
inline

Definition at line 163 of file graph.h.

◆ operator[]() [2/2]

template<class N = graph_nodet<empty_edget>>
nodet& grapht< N >::operator[] ( node_indext  n)
inline

Definition at line 168 of file graph.h.

◆ out()

◆ output_dot()

template<class N >
void grapht< N >::output_dot ( std::ostream &  out) const

Definition at line 914 of file graph.h.

Referenced by goto_instrument_parse_optionst::doit(), and static_show_domain().

◆ remove_edge()

template<class N = graph_nodet<empty_edget>>
void grapht< N >::remove_edge ( node_indext  a,
node_indext  b 
)
inline

Definition at line 204 of file graph.h.

Referenced by event_grapht::remove_com_edge(), and event_grapht::remove_po_edge().

◆ remove_edges()

template<class N = graph_nodet<empty_edget>>
void grapht< N >::remove_edges ( node_indext  n)
inline

Definition at line 220 of file graph.h.

Referenced by grapht< abstract_eventt >::make_chordal().

◆ remove_in_edges()

template<class N >
void grapht< N >::remove_in_edges ( node_indext  n)

Definition at line 351 of file graph.h.

Referenced by grapht< abstract_eventt >::remove_edges().

◆ remove_out_edges()

template<class N >
void grapht< N >::remove_out_edges ( node_indext  n)

Definition at line 366 of file graph.h.

Referenced by grapht< abstract_eventt >::remove_edges().

◆ remove_undirected_edge()

template<class N >
void grapht< N >::remove_undirected_edge ( node_indext  a,
node_indext  b 
)

Definition at line 340 of file graph.h.

◆ resize()

template<class N = graph_nodet<empty_edget>>
void grapht< N >::resize ( node_indext  s)
inline

Definition at line 173 of file graph.h.

◆ SCCs()

template<class N >
std::size_t grapht< N >::SCCs ( std::vector< node_indext > &  subgraph_nr) const

Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes to components indices.

For example, if nodes 1 and 3 are in SCC 0, and nodes 0, 2 and 4 are in SCC 1, this will leave subgraph_nr holding { 1, 0, 1, 0, 1 }, and the function will return 2 (the number of distinct SCCs). Lower-numbered SCCs are closer to the leaves, so in the particular case of a DAG, sorting by SCC number gives a topological sort, and for a cyclic graph the SCCs are topologically sorted but arbitrarily ordered internally.

Parameters
subgraph_nr[in, out]: should be pre-allocated with enough storage for one entry per graph node. Will be populated with the SCC indices of each node.
Returns
the number of distinct SCCs.

Definition at line 782 of file graph.h.

Referenced by instrumentert::goto2graph_cfg().

◆ shortest_loop()

template<class N = graph_nodet<empty_edget>>
void grapht< N >::shortest_loop ( node_indext  node,
patht path 
) const
inline

Definition at line 241 of file graph.h.

◆ shortest_path() [1/2]

template<class N = graph_nodet<empty_edget>>
void grapht< N >::shortest_path ( node_indext  src,
node_indext  dest,
patht path 
) const
inline

◆ shortest_path() [2/2]

template<class N >
void grapht< N >::shortest_path ( node_indext  src,
node_indext  dest,
patht path,
bool  non_trivial 
) const
protected

Definition at line 381 of file graph.h.

◆ size()

template<class N = graph_nodet<empty_edget>>
std::size_t grapht< N >::size ( ) const
inline

◆ swap()

template<class N = graph_nodet<empty_edget>>
void grapht< N >::swap ( grapht< N > &  other)
inline

Definition at line 153 of file graph.h.

◆ tarjan()

template<class N >
void grapht< N >::tarjan ( class tarjant t,
node_indext  v 
) const
protected

Definition at line 726 of file graph.h.

◆ topsort()

template<class N >
std::list< typename grapht< N >::node_indext > grapht< N >::topsort ( ) const

Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.

Uses Kahn's algorithm running in O(n_edges+n_nodes).

Definition at line 829 of file graph.h.

Referenced by create_static_initializer_wrappers(), and grapht< abstract_eventt >::is_dag().

◆ visit_reachable()

template<class N >
void grapht< N >::visit_reachable ( node_indext  src)

Definition at line 472 of file graph.h.

Member Data Documentation

◆ nodes


The documentation for this class was generated from the following file: