CBMC
Public Types | Public Member Functions | Public Attributes | Private Member Functions | List of all members
graph_nodet< E > Class Template Reference

This class represents a node in a directed graph. More...

#include <graph.h>

+ Inheritance diagram for graph_nodet< E >:
+ Collaboration diagram for graph_nodet< E >:

Public Types

typedef std::size_t node_indext
 
typedef E edget
 
typedef std::map< node_indext, edget > edgest
 

Public Member Functions

void add_in (node_indext n)
 
void add_out (node_indext n)
 
void erase_in (node_indext n)
 
void erase_out (node_indext n)
 
std::string pretty (const node_indext &idx) const
 
virtual ~graph_nodet ()
 

Public Attributes

edgest in
 
edgest out
 

Private Member Functions

virtual std::string dot_attributes (const node_indext &) const
 Node with attributes suitable for Graphviz DOT format. More...
 

Detailed Description

template<class E = empty_edget>
class graph_nodet< E >

This class represents a node in a directed graph.

See grapht for more information.

Definition at line 34 of file graph.h.

Member Typedef Documentation

◆ edgest

template<class E = empty_edget>
typedef std::map<node_indext, edget> graph_nodet< E >::edgest

Definition at line 40 of file graph.h.

◆ edget

template<class E = empty_edget>
typedef E graph_nodet< E >::edget

Definition at line 39 of file graph.h.

◆ node_indext

template<class E = empty_edget>
typedef std::size_t graph_nodet< E >::node_indext

Definition at line 37 of file graph.h.

Constructor & Destructor Documentation

◆ ~graph_nodet()

template<class E = empty_edget>
virtual graph_nodet< E >::~graph_nodet ( )
inlinevirtual

Definition at line 93 of file graph.h.

Member Function Documentation

◆ add_in()

template<class E = empty_edget>
void graph_nodet< E >::add_in ( node_indext  n)
inline

Definition at line 44 of file graph.h.

◆ add_out()

template<class E = empty_edget>
void graph_nodet< E >::add_out ( node_indext  n)
inline

Definition at line 49 of file graph.h.

◆ dot_attributes()

template<class E = empty_edget>
virtual std::string graph_nodet< E >::dot_attributes ( const node_indext &  ) const
inlineprivatevirtual

Node with attributes suitable for Graphviz DOT format.

Derived types may override this function to produce more informative DOT diagrams than the default implementation, which displays only the node index. The return value should be a list of node attributes within square brackets that can be parsed by dot. Here is a sample implementation for a fictional node type with is_evil() and is_pink() functions: 

std::stringstream ss;
ss << "[shape=\"" << is_evil() ? "box" : "diamond"
   << "\", color=\"" << is_pink() ? "#e91e63" : "#9c27b0"
   << "\", label=\"this is node " << std::to_string(idx)
   << "\"]";
return ss.str();

Reimplemented in scope_treet::scope_nodet.

Definition at line 80 of file graph.h.

◆ erase_in()

template<class E = empty_edget>
void graph_nodet< E >::erase_in ( node_indext  n)
inline

Definition at line 54 of file graph.h.

◆ erase_out()

template<class E = empty_edget>
void graph_nodet< E >::erase_out ( node_indext  n)
inline

Definition at line 59 of file graph.h.

◆ pretty()

template<class E = empty_edget>
std::string graph_nodet< E >::pretty ( const node_indext &  idx) const
inline

Definition at line 86 of file graph.h.

Member Data Documentation

◆ in

template<class E = empty_edget>
edgest graph_nodet< E >::in

Definition at line 42 of file graph.h.

◆ out

template<class E = empty_edget>
edgest graph_nodet< E >::out

Definition at line 42 of file graph.h.

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