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

#include <graph.h>

Inheritance diagram for grapht< N >:

Collaboration diagram for grapht< N >:

Classes
class	tarjant

Public Types
typedef N	nodet

typedef nodet::edgest	edgest

typedef std::vector< nodet >	nodest

typedef nodet::edget	edget

typedef nodet::node_indext	node_indext

typedef std::list< node_indext >	patht

Public Member Functions
template<typename... arguments>
node_indext	add_node (arguments &&... values)

void	swap (grapht &other)

bool	has_edge (node_indext i, node_indext j) const

const nodet &	operator[] (node_indext n) const

nodet &	operator[] (node_indext n)

void	resize (node_indext s)

std::size_t	size () const

bool	empty () const

const edgest &	in (node_indext n) const

const edgest &	out (node_indext n) const

void	add_edge (node_indext a, node_indext b)

void	remove_edge (node_indext a, node_indext b)

edget &	edge (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_indext >	get_reachable (node_indext src, bool forwards) const
	Run depth-first search on the graph, starting from a single source node. More...

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. 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_indext >	topsort () 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_indext >	get_predecessors (const node_indext &n) const

std::vector< node_indext >	get_successors (const node_indext &n) const

void	output_dot (std::ostream &out) const

void	for_each_predecessor (const node_indext &n, std::function< void(const node_indext &)> f) 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 from multiple source nodes, to find the nodes reachable within n steps. 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 166 of file graph.h.

Member Typedef Documentation

◆ edgest

template<class N = graph_nodet<empty_edget>>

typedef nodet::edgest grapht< N >::edgest

Definition at line 170 of file graph.h.

◆ edget

template<class N = graph_nodet<empty_edget>>

typedef nodet::edget grapht< N >::edget

Definition at line 172 of file graph.h.

◆ node_indext

template<class N = graph_nodet<empty_edget>>

typedef nodet::node_indext grapht< N >::node_indext

Definition at line 173 of file graph.h.

◆ nodest

template<class N = graph_nodet<empty_edget>>

typedef std::vector<nodet> grapht< N >::nodest

Definition at line 171 of file graph.h.

◆ nodet

template<class N = graph_nodet<empty_edget>>

typedef N grapht< N >::nodet

Definition at line 169 of file graph.h.

◆ patht

template<class N = graph_nodet<empty_edget>>

typedef std::list<node_indext> grapht< N >::patht

Definition at line 265 of file graph.h.

Member Function Documentation

◆ add_edge()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::add_edge	(	node_indext	a,
		node_indext	b
	)

inline

Definition at line 232 of file graph.h.

◆ add_node()

template<class N = graph_nodet<empty_edget>>

template<typename... arguments>

node_indext grapht< N >::add_node ( arguments &&... values )

inline

Definition at line 180 of file graph.h.

◆ add_undirected_edge()

template<class N >

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

Definition at line 365 of file graph.h.

◆ clear()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::clear ( void )

inline

Definition at line 260 of file graph.h.

◆ 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_nr will 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 730 of file graph.h.

◆ depth_limited_search() [1/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

src	The nodes to start the search from.
limit	limit on steps

Returns: a vector of reachable node indices

Definition at line 668 of file graph.h.

◆ 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,
		std::vector< bool > &	visited
	)		const

protected

Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps.

Parameters

src	The nodes to start the search from.
limit	limit on steps
visited	vector of booleans indicating whether a node has been visited

Returns: a vector of reachable node indices

Definition at line 691 of file graph.h.

◆ depth_limited_search() [3/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

src	The node to start the search from.
limit	limit on steps

Returns: a vector of reachable node indices

Definition at line 653 of file graph.h.

◆ disconnect_unreachable() [1/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

src	vector of indices of start nodes

Definition at line 537 of file graph.h.

◆ disconnect_unreachable() [2/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

src	start node

Definition at line 527 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 244 of file graph.h.

◆ empty()

template<class N = graph_nodet<empty_edget>>

bool grapht< N >::empty ( ) const

inline

Definition at line 217 of file graph.h.

◆ for_each_predecessor()

template<class N >

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

Definition at line 968 of file graph.h.

◆ 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 979 of file graph.h.

◆ get_predecessors()

template<class N >

std::vector< typename grapht< N >::node_indext > grapht< N >::get_predecessors ( const node_indext & n ) const

Definition at line 943 of file graph.h.

◆ get_reachable() [1/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

src	The nodes to start the search from.
forwards	true (false) if the forward (backward) reachability should be performed.

Definition at line 616 of file graph.h.

◆ get_reachable() [2/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

src	The node to start the search from.
forwards	true (false) if the forward (backward) reachability should be performed.

Definition at line 602 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 956 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

Definition at line 192 of file graph.h.

◆ in()

template<class N = graph_nodet<empty_edget>>

const edgest& grapht< N >::in ( node_indext n ) const

inline

Definition at line 222 of file graph.h.

◆ is_dag()

template<class N = graph_nodet<empty_edget>>

bool grapht< N >::is_dag ( ) const

inline

Definition at line 308 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 848 of file graph.h.

◆ operator[]() [1/2]

template<class N = graph_nodet<empty_edget>>

nodet& grapht< N >::operator[] ( node_indext n )

inline

Definition at line 202 of file graph.h.

◆ operator[]() [2/2]

template<class N = graph_nodet<empty_edget>>

const nodet& grapht< N >::operator[] ( node_indext n ) const

inline

Definition at line 197 of file graph.h.

◆ out()

template<class N = graph_nodet<empty_edget>>

const edgest& grapht< N >::out ( node_indext n ) const

inline

Definition at line 227 of file graph.h.

◆ output_dot()

template<class N >

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

Definition at line 990 of file graph.h.

◆ remove_edge()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::remove_edge	(	node_indext	a,
		node_indext	b
	)

inline

Definition at line 238 of file graph.h.

◆ remove_edges()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::remove_edges ( node_indext n )

inline

Definition at line 254 of file graph.h.

◆ remove_in_edges()

template<class N >

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

Definition at line 389 of file graph.h.

◆ remove_out_edges()

template<class N >

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

Definition at line 404 of file graph.h.

◆ remove_undirected_edge()

template<class N >

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

Definition at line 378 of file graph.h.

◆ resize()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::resize ( node_indext s )

inline

Definition at line 207 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

[in,out] subgraph_nr 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 832 of file graph.h.

◆ shortest_loop()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::shortest_loop	(	node_indext	node,
		patht &	path
	)		const

inline

Definition at line 275 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

Definition at line 267 of file graph.h.

◆ 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 419 of file graph.h.

◆ size()

template<class N = graph_nodet<empty_edget>>

std::size_t grapht< N >::size ( ) const

inline

Definition at line 212 of file graph.h.

◆ swap()

template<class N = graph_nodet<empty_edget>>

void grapht< N >::swap ( grapht< N > & other )

inline

Definition at line 187 of file graph.h.

◆ tarjan()

template<class N >

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

protected

Definition at line 774 of file graph.h.

◆ topsort()

template<class N >

std::list< typename grapht< N >::node_indext > grapht< N >::topsort

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 879 of file graph.h.

◆ visit_reachable()

template<class N >

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

Definition at line 511 of file graph.h.

Member Data Documentation

◆ nodes

template<class N = graph_nodet<empty_edget>>

nodest grapht< N >::nodes

protected

Definition at line 176 of file graph.h.

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

/home/runner/work/cbmc/cbmc/src/util/graph.h

Classes

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

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

Member Typedef Documentation

◆ edgest

◆ edget

◆ node_indext

◆ nodest

◆ nodet

◆ patht

Member Function Documentation

◆ add_edge()

◆ add_node()

◆ add_undirected_edge()

◆ clear()

◆ connected_subgraphs()

◆ depth_limited_search() [1/3]

◆ depth_limited_search() [2/3]

◆ depth_limited_search() [3/3]

◆ disconnect_unreachable() [1/2]

◆ disconnect_unreachable() [2/2]

◆ edge()

◆ empty()

◆ for_each_predecessor()

◆ for_each_successor()

◆ get_predecessors()

◆ get_reachable() [1/2]

◆ get_reachable() [2/2]

◆ get_successors()

◆ has_edge()

◆ in()

◆ is_dag()

◆ make_chordal()

◆ operator[]() [1/2]

◆ operator[]() [2/2]

◆ out()

◆ output_dot()

◆ remove_edge()

◆ remove_edges()

◆ remove_in_edges()

◆ remove_out_edges()

◆ remove_undirected_edge()

◆ resize()

◆ SCCs()

◆ shortest_loop()

◆ shortest_path() [1/2]

◆ shortest_path() [2/2]

◆ size()

◆ swap()

◆ tarjan()

◆ topsort()

◆ visit_reachable()

Member Data Documentation

◆ nodes

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