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)
 
void make_chordal ()
 
std::size_t connected_subgraphs (std::vector< node_indext > &subgraph_nr)
 
std::size_t SCCs (std::vector< node_indext > &subgraph_nr)
 
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...
 
void output_dot (std::ostream &out) const
 
void output_dot_node (std::ostream &out, node_indext n) const
 

Protected Member Functions

void tarjan (class tarjant &t, node_indext v)
 
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 132 of file graph.h.

Member Typedef Documentation

◆ edgest

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

Definition at line 136 of file graph.h.

◆ edget

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

Definition at line 138 of file graph.h.

◆ node_indext

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

Definition at line 139 of file graph.h.

◆ nodest

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

Definition at line 137 of file graph.h.

◆ nodet

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

Definition at line 135 of file graph.h.

◆ patht

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

Definition at line 230 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 303 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 225 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)

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

◆ empty()

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

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

Referenced by event_grapht::has_com_edge(), and event_grapht::has_po_edge().

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

◆ make_chordal()

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

Definition at line 574 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 162 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 167 of file graph.h.

◆ out()

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

◆ output_dot()

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

Definition at line 656 of file graph.h.

Referenced by goto_instrument_parse_optionst::doit().

◆ output_dot_node()

template<class N >
void grapht< N >::output_dot_node ( std::ostream &  out,
node_indext  n 
) const

Definition at line 663 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 203 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 219 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 327 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 342 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 316 of file graph.h.

◆ resize()

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

Definition at line 172 of file graph.h.

◆ SCCs()

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

Definition at line 562 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 240 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 357 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 152 of file graph.h.

◆ tarjan()

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

Definition at line 518 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(#edges+nodes).

Definition at line 612 of file graph.h.

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

◆ visit_reachable()

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

Definition at line 448 of file graph.h.

Member Data Documentation

◆ nodes


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