- Generated by
1.8.14
|
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 grapht< abstract_eventt >::is_dag().
|
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 | ) |
Definition at line 327 of file graph.h.
Referenced by grapht< abstract_eventt >::remove_edges().
| void grapht< N >::remove_out_edges | ( | node_indext | n | ) |
Definition at line 342 of file graph.h.
Referenced by grapht< abstract_eventt >::remove_edges().
| 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 |
Definition at line 232 of file graph.h.
Referenced by grapht< abstract_eventt >::shortest_loop(), and grapht< abstract_eventt >::shortest_path().
|
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 |
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().
| void grapht< N >::visit_reachable | ( | node_indext | src | ) |
Definition at line 142 of file graph.h.
Referenced by grapht< abstract_eventt >::add_edge(), grapht< abstract_eventt >::add_node(), grapht< abstract_eventt >::clear(), grapht< abstract_eventt >::edge(), grapht< abstract_eventt >::empty(), grapht< abstract_eventt >::has_edge(), grapht< abstract_eventt >::in(), grapht< abstract_eventt >::operator[](), grapht< abstract_eventt >::out(), grapht< abstract_eventt >::remove_edge(), grapht< abstract_eventt >::resize(), grapht< abstract_eventt >::size(), and grapht< abstract_eventt >::swap().
1.8.14