Agda.Utils.Graph.AdjacencyMap

Directed graphs (can of course simulate undirected graphs).

Represented as adjacency maps.

Each source node maps to a adjacency map, which is a map from target nodes to edges.

This allows to get the outgoing edges in O(log n) time where n is the number of nodes in the graph. However, the set of incoming edges can only be obtained in O(n log n), or O(e) where e is the total number of edges.

Documentation

newtype Graph n e

Graph n e is a directed graph with nodes in n and edges in e.

Only one edge between any two nodes.

Represented as "adjacency list", or rather, adjacency map. This allows to get all outgoing edges for a node in O(log n) time where n is the number of nodes of the graph. Incoming edges can only be computed in O(n + e) time where e is the number of edges.

Constructors

Graph

Fields

unGraph :: Map n (Map n e)

Instances

Functor (Graph n)

(Eq n, Eq e) => Eq (Graph n e)

(Show n, Show e) => Show (Graph n e)

(Ord n, SemiRing e, Arbitrary n, Arbitrary e) => Arbitrary (Graph n e)

(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e)

invariant :: Ord n => Graph n e -> Bool

A structural invariant for the graphs.

The set of nodes is obtained by Map.keys . unGraph meaning that each node, be it only the target of an edge, must be assigned an adjacency map, albeit it could be empty.

See singleton.

edges :: Ord n => Graph n e -> [(n, n, e)]

Turn a graph into a list of edges. O(n + e)

edgesFrom :: Ord n => Graph n e -> [n] -> [(n, n, e)]

All edges originating in the given nodes. (I.e., all outgoing edges for the given nodes.)

Roughly linear in the length of the result list O(result).

nodes :: Ord n => Graph n e -> Set n

Returns all the nodes in the graph. O(n).

filterEdges :: Ord n => (e -> Bool) -> Graph n e -> Graph n e

fromNodes :: Ord n => [n] -> Graph n e

Constructs a completely disconnected graph containing the given nodes. O(n).

fromList :: (SemiRing e, Ord n) => [(n, n, e)] -> Graph n e

Constructs a graph from a list of edges. O(e)

empty :: Graph n e

Empty graph (no nodes, no edges).

singleton :: Ord n => n -> n -> e -> Graph n e

A graph with two nodes and a single connecting edge.

insert :: (SemiRing e, Ord n) => n -> n -> e -> Graph n e -> Graph n e

Insert an edge into the graph.

removeNode :: Ord n => n -> Graph n e -> Graph n e

Removes the given node, and all corresponding edges, from the graph.

removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e

removeEdge n1 n2 g removes the edge going from n1 to n2, if any.

union :: (SemiRing e, Ord n) => Graph n e -> Graph n e -> Graph n e

unions :: (SemiRing e, Ord n) => [Graph n e] -> Graph n e

lookup :: Ord n => n -> n -> Graph n e -> Maybe e

neighbours :: Ord n => n -> Graph n e -> [(n, e)]

sccs' :: Ord n => Graph n e -> [SCC n]

The graph's strongly connected components, in reverse topological order.

sccs :: Ord n => Graph n e -> [[n]]

The graph's strongly connected components, in reverse topological order.

acyclic :: Ord n => Graph n e -> Bool

Returns True iff the graph is acyclic.

transitiveClosure1 :: (Eq e, SemiRing e, Ord n) => Graph n e -> Graph n e

Computes the transitive closure of the graph.

Note that this algorithm is not guaranteed to be correct (or terminate) for arbitrary semirings.

This function operates on the entire graph at once.

transitiveClosure :: (Eq e, SemiRing e, Ord n) => Graph n e -> Graph n e

Computes the transitive closure of the graph.

Note that this algorithm is not guaranteed to be correct (or terminate) for arbitrary semirings.

This function operates on one strongly connected component at a time.

findPath :: (SemiRing e, Ord n) => (e -> Bool) -> n -> n -> Graph n e -> Maybe e

allPaths :: (SemiRing e, Ord n, Ord c) => (e -> c) -> n -> n -> Graph n e -> [e]

allPaths classify a b g returns a list of pathes (accumulated edge weights) from node a to node b in g. Alternative intermediate pathes are only considered if they are distinguished by the classify function.

nodeIn :: (Ord n, Arbitrary n) => Graph n e -> Gen n

Generates a node from the graph. (Unless the graph is empty.)

edgeIn :: (Ord n, Arbitrary n, Arbitrary e) => Graph n e -> Gen (n, n, e)

Generates an edge from the graph. (Unless the graph contains no edges.)

tests :: IO Bool

All tests.