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) |
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 | make_chordal () |
std::size_t | connected_subgraphs (std::vector< node_indext > &subgraph_nr) |
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_successors (const node_indext &n) const |
void | output_dot (std::ostream &out) const |
void | for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const |
Protected Member Functions | |
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 |
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 198 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(), call_grapht::get_directed_graph(), 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 146 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[](), function_indicest::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 312 of file graph.h.
Referenced by grapht< abstract_eventt >::make_chordal().
|
inline |
Definition at line 226 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 183 of file graph.h.
Referenced by build_graph(), goto_program2codet::convert_goto_switch(), and grapht< abstract_eventt >::is_dag().
void grapht< N >::for_each_successor | ( | const node_indext & | n, |
std::function< void(const node_indext &)> | f | ||
) | const |
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.
src | The node to start the search from. |
forwards | true (false) if the forward (backward) reachability should be performed. |
Definition at line 503 of file graph.h.
Referenced by get_connected_functions().
std::vector< typename N::node_indext > grapht< N >::get_reachable | ( | const std::vector< node_indext > & | src, |
bool | forwards | ||
) | const |
std::vector< typename grapht< N >::node_indext > grapht< N >::get_successors | ( | const node_indext & | n | ) | const |
|
inline |
Definition at line 158 of file graph.h.
Referenced by call_grapht::get_directed_graph(), event_grapht::has_com_edge(), and event_grapht::has_po_edge().
|
inline |
Definition at line 188 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 193 of file graph.h.
Referenced by build_graph_rec(), event_grapht::com_out(), reachability_slicert::fixedpoint_from_assertions(), call_grapht::get_directed_graph(), get_neighbours(), graphml_witnesst::operator()(), and event_grapht::po_out().
void grapht< N >::output_dot | ( | std::ostream & | out | ) | const |
Definition at line 784 of file graph.h.
Referenced by goto_instrument_parse_optionst::doit(), and static_show_domain().
|
inline |
Definition at line 204 of file graph.h.
Referenced by event_grapht::remove_com_edge(), and event_grapht::remove_po_edge().
|
inline |
Definition at line 220 of file graph.h.
Referenced by grapht< abstract_eventt >::make_chordal().
void grapht< N >::remove_in_edges | ( | node_indext | n | ) |
Definition at line 336 of file graph.h.
Referenced by grapht< abstract_eventt >::remove_edges().
void grapht< N >::remove_out_edges | ( | node_indext | n | ) |
Definition at line 351 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 | ) | 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.
subgraph_nr | [in, out]: should be pre-allocated with enough storage for one entry per graph node. Will be populated with the SCC indices of each node. |
Definition at line 649 of file graph.h.
Referenced by instrumentert::goto2graph_cfg().
|
inline |
|
inline |
Definition at line 233 of file graph.h.
Referenced by grapht< abstract_eventt >::shortest_loop(), and grapht< abstract_eventt >::shortest_path().
|
protected |
|
inline |
Definition at line 178 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(n_edges+n_nodes).
Definition at line 699 of file graph.h.
Referenced by create_static_initializer_wrappers(), and grapht< abstract_eventt >::is_dag().
void grapht< N >::visit_reachable | ( | node_indext | src | ) |
Definition at line 143 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().