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 | disconnect_unreachable (node_indext src) |
Removes any edges between nodes in a graph that are unreachable from a given start node. More... | |
void | disconnect_unreachable (const std::vector< node_indext > &src) |
Removes any edges between nodes in a graph that are unreachable from a vector of start nodes. More... | |
std::vector< typename N::node_indext > | depth_limited_search (typename N::node_indext src, std::size_t limit) const |
Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More... | |
std::vector< typename N::node_indext > | depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit) const |
Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More... | |
void | make_chordal () |
Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges. More... | |
std::size_t | connected_subgraphs (std::vector< node_indext > &subgraph_nr) |
Find connected subgraphs in an undirected graph. More... | |
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 | |
std::vector< typename N::node_indext > | depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const |
Run recursive depth-limited search on the graph, starting. More... | |
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 327 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 | ) |
Find connected subgraphs in an undirected graph.
[out] | subgraph_nr | will be resized to graph.size() and populated to map node indices onto subgraph numbers. The subgraph numbers are dense, in the range 0 - (number of subgraphs - 1) |
std::vector< typename N::node_indext > grapht< N >::depth_limited_search | ( | typename N::node_indext | src, |
std::size_t | limit | ||
) | const |
Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps.
This function initialises the search.
src | The node to start the search from. |
limit | limit on steps |
Definition at line 606 of file graph.h.
Referenced by get_functions_reachable_within_n_steps().
std::vector< typename N::node_indext > grapht< N >::depth_limited_search | ( | std::vector< typename N::node_indext > & | src, |
std::size_t | limit | ||
) | const |
Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps.
This function initialises the search.
src | The nodes to start the search from. |
limit | limit on steps |
|
protected |
void grapht< N >::disconnect_unreachable | ( | node_indext | src | ) |
Removes any edges between nodes in a graph that are unreachable from a given start node.
Used for computing cone of influence, by disconnecting unreachable nodes and then performing backwards reachability. Note nodes are not actually removed from the vector nodes, because this requires renumbering node indices. This copies the way nodes are "removed" in make_chordal.
src | start node |
Definition at line 488 of file graph.h.
Referenced by disconnect_unreachable_functions().
void grapht< N >::disconnect_unreachable | ( | const std::vector< node_indext > & | src | ) |
|
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 555 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 |
void grapht< N >::make_chordal | ( | ) |
Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges.
Note this adds more edges than are required, including to acyclic graphs or acyclic subgraphs of cyclic graphs, but does at least ensure the graph is not chordal.
|
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 914 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 351 of file graph.h.
Referenced by grapht< abstract_eventt >::remove_edges().
void grapht< N >::remove_out_edges | ( | node_indext | n | ) |
Definition at line 366 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 782 of file graph.h.
Referenced by instrumentert::goto2graph_cfg().
|
inline |
|
inline |
Definition at line 233 of file graph.h.
Referenced by get_shortest_function_path(), 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 829 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().