cprover
|
A generic directed graph with a parametric node type. More...
#include <graph.h>
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 | |
node_indext | add_node () |
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) |
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_indext > | topsort () 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 |
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.
typedef nodet::node_indext grapht< N >::node_indext |
typedef std::list<node_indext> grapht< N >::patht |
|
inline |
Definition at line 197 of file graph.h.
Referenced by event_grapht::add_com_edge(), event_grapht::add_po_back_edge(), event_grapht::add_po_edge(), alt_copy_segment(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_backedge(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
|
inline |
Definition at line 145 of file graph.h.
Referenced by add_node(), event_grapht::add_node(), graphmlt::add_node_if_not_exists(), graphml_witnesst::operator()(), cfg_baset< T, P, I >::entry_mapt::operator[](), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
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().
|
inline |
Definition at line 225 of file graph.h.
Referenced by event_grapht::clear().
std::size_t grapht< N >::connected_subgraphs | ( | std::vector< node_indext > & | subgraph_nr | ) |
|
inline |
|
inline |
Definition at line 182 of file graph.h.
Referenced by build_graph(), goto_program2codet::convert_goto_switch(), and cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false >::fixedpoint().
|
inline |
Definition at line 157 of file graph.h.
Referenced by event_grapht::has_com_edge(), and event_grapht::has_po_edge().
|
inline |
Definition at line 187 of file graph.h.
Referenced by full_slicert::add_function_calls(), build_graph_rec(), event_grapht::com_in(), graphml_witnesst::operator()(), and event_grapht::po_in().
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 192 of file graph.h.
Referenced by build_graph_rec(), event_grapht::com_out(), graphml_witnesst::operator()(), and event_grapht::po_out().
void grapht< N >::output_dot | ( | std::ostream & | out | ) | const |
Definition at line 656 of file graph.h.
Referenced by goto_instrument_parse_optionst::doit().
void grapht< N >::output_dot_node | ( | std::ostream & | out, |
node_indext | n | ||
) | const |
|
inline |
Definition at line 203 of file graph.h.
Referenced by event_grapht::remove_com_edge(), and event_grapht::remove_po_edge().
|
inline |
Definition at line 219 of file graph.h.
Referenced by grapht< abstract_eventt >::make_chordal().
void grapht< N >::remove_in_edges | ( | node_indext | n | ) |
void grapht< N >::remove_out_edges | ( | node_indext | n | ) |
void grapht< N >::remove_undirected_edge | ( | node_indext | a, |
node_indext | b | ||
) |
|
inline |
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().
|
inline |
|
inline |
|
protected |
|
inline |
Definition at line 177 of file graph.h.
Referenced by full_slicert::add_jumps(), build_graph(), full_slicert::fixedpoint(), instrumentert::goto2graph_cfg(), grapht< abstract_eventt >::make_chordal(), event_grapht::size(), and write_graphml().
|
protected |
std::list< typename grapht< N >::node_indext > grapht< N >::topsort | ( | ) | const |
void grapht< N >::visit_reachable | ( | node_indext | src | ) |
Definition at line 142 of file graph.h.
Referenced by grapht< abstract_eventt >::swap().