Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Directed graphs (can of course simulate undirected graphs).
Represented as adjacency maps in direction from source to target.
Each source node maps to an adjacency map of outgoing edges, which is a map from target nodes to edges.
Listed time complexities are for the worst case (and possibly amortised), with n standing for the number of nodes in the graph and e standing for the number of edges. Comparisons, predicates etc. are assumed to take constant time (unless otherwise stated).
Synopsis
- newtype Graph n e = Graph {}
- invariant :: Ord n => Graph n e -> Bool
- data Edge n e = Edge {}
- lookup :: Ord n => n -> n -> Graph n e -> Maybe e
- edges :: Graph n e -> [Edge n e]
- neighbours :: Ord n => n -> Graph n e -> [(n, e)]
- neighboursMap :: Ord n => n -> Graph n e -> Map n e
- edgesFrom :: Ord n => Graph n e -> [n] -> [Edge n e]
- edgesTo :: Ord n => Graph n e -> [n] -> [Edge n e]
- diagonal :: Ord n => Graph n e -> [Edge n e]
- nodes :: Graph n e -> Set n
- sourceNodes :: Graph n e -> Set n
- targetNodes :: Ord n => Graph n e -> Set n
- isolatedNodes :: Ord n => Graph n e -> Set n
- data Nodes n = Nodes {}
- computeNodes :: Ord n => Graph n e -> Nodes n
- discrete :: Null e => Graph n e -> Bool
- acyclic :: Ord n => Graph n e -> Bool
- fromNodes :: Ord n => [n] -> Graph n e
- fromNodeSet :: Ord n => Set n -> Graph n e
- fromEdges :: Ord n => [Edge n e] -> Graph n e
- fromEdgesWith :: Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
- empty :: Graph n e
- singleton :: Ord n => n -> n -> e -> Graph n e
- insert :: Ord n => n -> n -> e -> Graph n e -> Graph n e
- insertWith :: Ord n => (e -> e -> e) -> n -> n -> e -> Graph n e -> Graph n e
- insertEdge :: Ord n => Edge n e -> Graph n e -> Graph n e
- insertEdgeWith :: Ord n => (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
- union :: Ord n => Graph n e -> Graph n e -> Graph n e
- unionWith :: Ord n => (e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
- unions :: Ord n => [Graph n e] -> Graph n e
- unionsWith :: Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
- mapWithEdge :: (Edge n e -> e') -> Graph n e -> Graph n e'
- transposeEdge :: Edge n e -> Edge n e
- transpose :: Ord n => Graph n e -> Graph n e
- clean :: Null e => Graph n e -> Graph n e
- removeNode :: Ord n => n -> Graph n e -> Graph n e
- removeNodes :: Ord n => Set n -> Graph n e -> Graph n e
- removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e
- filterNodes :: Ord n => (n -> Bool) -> Graph n e -> Graph n e
- filterEdges :: (Edge n e -> Bool) -> Graph n e -> Graph n e
- filterNodesKeepingEdges :: forall n e. (Ord n, SemiRing e) => (n -> Bool) -> Graph n e -> Graph n e
- renameNodes :: Ord n2 => (n1 -> n2) -> Graph n1 e -> Graph n2 e
- renameNodesMonotonic :: (Ord n1, Ord n2) => (n1 -> n2) -> Graph n1 e -> Graph n2 e
- data WithUniqueInt n = WithUniqueInt {
- uniqueInt :: !Int
- otherValue :: !n
- addUniqueInts :: forall n e. Ord n => Graph n e -> Graph (WithUniqueInt n) e
- unzip :: Graph n (e, e') -> (Graph n e, Graph n e')
- composeWith :: Ord n => (c -> d -> e) -> (e -> e -> e) -> Graph n c -> Graph n d -> Graph n e
- sccs' :: Ord n => Graph n e -> [SCC n]
- sccs :: Ord n => Graph n e -> [[n]]
- data DAG n = DAG {
- dagGraph :: Graph
- dagComponentMap :: IntMap (SCC n)
- dagNodeMap :: Map n Int
- dagInvariant :: Ord n => DAG n -> Bool
- oppositeDAG :: DAG n -> DAG n
- reachable :: Ord n => DAG n -> SCC n -> [n]
- sccDAG' :: forall n e. Ord n => Graph n e -> [SCC n] -> DAG n
- sccDAG :: Ord n => Graph n e -> DAG n
- reachableFrom :: Ord n => Graph n e -> n -> Map n (Int, [Edge n e])
- reachableFromSet :: Ord n => Graph n e -> Set n -> Set n
- walkSatisfying :: Ord n => (Edge n e -> Bool) -> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
- longestPaths :: forall n e. Ord n => Graph n e -> Graph n (Int, [[Edge n e]])
- gaussJordanFloydWarshallMcNaughtonYamada :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> (Graph n e, [SCC n])
- gaussJordanFloydWarshallMcNaughtonYamadaReference :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e
- transitiveClosure :: (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e
- transitiveReduction :: Ord n => Graph n e -> Graph n ()
- complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> Graph n e
- completeIter :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> [(Graph n e, Graph n e)]
Graphs and edges
Graph n e
is a type of directed graphs with nodes in n
and
edges in e
.
At most one edge is allowed between any two nodes. Multigraphs
can be simulated by letting the edge type e
be a collection
type.
The graphs are represented as adjacency maps (adjacency lists, but using finite maps instead of arrays and lists). This makes it possible to compute a node's outgoing edges in logarithmic time (O(log n)). However, computing the incoming edges may be more expensive.
Note that neither the number of nodes nor the number of edges may
exceed
.maxBound
:: Int
Instances
(Ord r, Ord f) => SetToInfty f (ConGraph r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> ConGraph r f -> ConGraph r f Source # | |
Functor (Graph n) Source # | |
(PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e) Source # | |
Defined in Agda.TypeChecking.Pretty | |
(Ord n, Pretty n, Pretty e) => Pretty (Graph n e) Source # | |
(Ord n, Show n, Show e) => Show (Graph n e) Source # | |
(Eq n, Eq e) => Eq (Graph n e) Source # | |
(Ord r, Ord f, Negative a) => Negative (Graph r f a) Source # | A graph is |
(Ord r, Ord f, Negative a) => Negative (Graphs r f a) Source # | |
Edges.
Instances
Eq f => SetToInfty f (Edge' r f a) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> Edge' r f a -> Edge' r f a Source # | |
Functor (Edge n) Source # | |
Collection (Call cinfo) (CallGraph cinfo) Source # | |
Singleton (Call cinfo) (CallGraph cinfo) Source # | |
(Pretty n, Pretty e) => Pretty (Edge n e) Source # | |
(Show n, Show e) => Show (Edge n e) Source # | |
(Eq n, Eq e) => Eq (Edge n e) Source # | |
(Ord n, Ord e) => Ord (Edge n e) Source # | |
Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional | |
(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) Source # | |
(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) Source # | |
(Ord r, Ord f, Top a) => Top (Edge' r f a) Source # | |
Negative a => Negative (Edge' r f a) Source # | An edge is negative if its label is. |
Queries
lookup :: Ord n => n -> n -> Graph n e -> Maybe e Source #
If there is an edge from s
to t
, then lookup s t g
is
, where Just
ee
is the edge's label. O(log n).
neighbours :: Ord n => n -> Graph n e -> [(n, e)] Source #
neighbours u g
consists of all nodes v
for which there is an
edge from u
to v
in g
, along with the corresponding edge
labels. O(log n + |neighbours u g
|).
neighboursMap :: Ord n => n -> Graph n e -> Map n e Source #
neighboursMap u g
consists of all nodes v
for which there is
an edge from u
to v
in g
, along with the corresponding edge
labels. O(log n).
edgesFrom :: Ord n => Graph n e -> [n] -> [Edge n e] Source #
edgesFrom g ns
is a list containing all edges originating in
the given nodes (i.e., all outgoing edges for the given nodes). If
ns
does not contain duplicates, then the resulting list does not
contain duplicates. O(|ns
| log |n
| + |edgesFrom g ns
|).
edgesTo :: Ord n => Graph n e -> [n] -> [Edge n e] Source #
edgesTo g ns
is a list containing all edges ending in the given
nodes (i.e., all incoming edges for the given nodes). If ns
does
not contain duplicates, then the resulting list does not contain
duplicates. O(|ns
| n log n).
sourceNodes :: Graph n e -> Set n Source #
Nodes with outgoing edges. O(n).
isolatedNodes :: Ord n => Graph n e -> Set n Source #
Nodes without incoming or outgoing edges. O(n + e log n).
Various kinds of nodes.
discrete :: Null e => Graph n e -> Bool Source #
Checks whether the graph is discrete (containing no edges other
than null
edges). O(n + e).
Construction
fromNodes :: Ord n => [n] -> Graph n e Source #
Constructs a completely disconnected graph containing the given nodes. O(n log n).
fromNodeSet :: Ord n => Set n -> Graph n e Source #
Constructs a completely disconnected graph containing the given nodes. O(n).
fromEdges :: Ord n => [Edge n e] -> Graph n e Source #
fromEdges es
is a graph containing the edges in es
, with the
caveat that later edges overwrite earlier edges. O(|es
| log n).
fromEdgesWith :: Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e Source #
fromEdgesWith f es
is a graph containing the edges in es
.
Later edges are combined with earlier edges using the supplied
function. O(|es
| log n).
singleton :: Ord n => n -> n -> e -> Graph n e Source #
A graph with two nodes and a single connecting edge. O(1).
insert :: Ord n => n -> n -> e -> Graph n e -> Graph n e Source #
Inserts an edge into the graph. O(log n).
insertWith :: Ord n => (e -> e -> e) -> n -> n -> e -> Graph n e -> Graph n e Source #
insertWith f s t new
inserts an edge from s
to t
into the
graph. If there is already an edge from s
to t
with label old
,
then this edge gets replaced by an edge with label f new old
, and
otherwise the edge's label is new
. O(log n).
insertEdge :: Ord n => Edge n e -> Graph n e -> Graph n e Source #
Inserts an edge into the graph. O(log n).
insertEdgeWith :: Ord n => (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e Source #
A variant of insertWith
. O(log n).
union :: Ord n => Graph n e -> Graph n e -> Graph n e Source #
Left-biased union.
Time complexity: See unionWith
.
unionWith :: Ord n => (e -> e -> e) -> Graph n e -> Graph n e -> Graph n e Source #
Union. The function is used to combine edge labels for edges that occur in both graphs (labels from the first graph are given as the first argument to the function).
Time complexity: O(n₁ log (n₂n₁ + 1) + e₁ log e₂, where n₁/ is the number of nodes in the graph with the smallest number of nodes and n₂ is the number of nodes in the other graph, and e₁ is the number of edges in the graph with the smallest number of edges and e₂ is the number of edges in the other graph.
Less complicated time complexity: O((n + e) log n (where n and e refer to the resulting graph).
unions :: Ord n => [Graph n e] -> Graph n e Source #
Union. O((n + e) log n (where n and e refer to the resulting graph).
unionsWith :: Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e Source #
Union. The function is used to combine edge labels for edges that occur in several graphs. O((n + e) log n (where n and e refer to the resulting graph).
Transformation
mapWithEdge :: (Edge n e -> e') -> Graph n e -> Graph n e' Source #
A variant of fmap
that provides extra information to the
function argument. O(n + e).
transposeEdge :: Edge n e -> Edge n e Source #
Reverses an edge. O(1).
transpose :: Ord n => Graph n e -> Graph n e Source #
The opposite graph (with all edges reversed). O((n + e) log n).
removeNode :: Ord n => n -> Graph n e -> Graph n e Source #
removeNode n g
removes the node n
(and all corresponding
edges) from g
. O(n + e).
removeNodes :: Ord n => Set n -> Graph n e -> Graph n e Source #
removeNodes ns g
removes the nodes in ns
(and all
corresponding edges) from g
. O((n + e) log |ns
|).
removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e Source #
removeEdge s t g
removes the edge going from s
to t
, if any.
O(log n).
filterNodes :: Ord n => (n -> Bool) -> Graph n e -> Graph n e Source #
The graph filterNodes p g
contains exactly those nodes from g
that satisfy the predicate p
. Edges to or from nodes that are
removed are also removed. O(n + e).
filterEdges :: (Edge n e -> Bool) -> Graph n e -> Graph n e Source #
Keep only the edges that satisfy the predicate. O(n + e).
filterNodesKeepingEdges :: forall n e. (Ord n, SemiRing e) => (n -> Bool) -> Graph n e -> Graph n e Source #
Removes the nodes that do not satisfy the predicate from the graph, but keeps the edges: if there is a path in the original graph between two nodes that are retained, then there is a path between these two nodes also in the resulting graph.
Precondition: The graph must be acyclic.
Worst-case time complexity: O(e n log n) (this has not been verified carefully).
renameNodes :: Ord n2 => (n1 -> n2) -> Graph n1 e -> Graph n2 e Source #
Renames the nodes.
Precondition: The renaming function must be injective.
Time complexity: O((n + e) log n).
data WithUniqueInt n Source #
WithUniqueInt n
consists of pairs of (unique) Int
s and values
of type n
.
Values of this type are compared by comparing the Int
s.
WithUniqueInt | |
|
Instances
addUniqueInts :: forall n e. Ord n => Graph n e -> Graph (WithUniqueInt n) e Source #
composeWith :: Ord n => (c -> d -> e) -> (e -> e -> e) -> Graph n c -> Graph n d -> Graph n e Source #
composeWith times plus g g'
finds all edges
s --c_i--> t_i --d_i--> u
and constructs the
result graph from edge(s,u) = sum_i (c_i times d_i)
.
Complexity: For each edge s --> t
in g
we look up
all edges starting with t
in g'
.
Precondition: The two graphs must have exactly the same nodes.
Strongly connected components
sccs' :: Ord n => Graph n e -> [SCC n] Source #
The graph's strongly connected components, in reverse topological order.
The time complexity is likely O(n + e log n) (but this depends on
the, at the time of writing undocumented, time complexity of
stronglyConnComp
).
sccs :: Ord n => Graph n e -> [[n]] Source #
The graph's strongly connected components, in reverse topological order.
The time complexity is likely O(n + e log n) (but this depends on
the, at the time of writing undocumented, time complexity of
stronglyConnComp
).
SCC DAGs.
The maps map SCC indices to and from SCCs/nodes.
DAG | |
|
oppositeDAG :: DAG n -> DAG n Source #
The opposite DAG.
Constructs a DAG containing the graph's strongly connected components.
sccDAG :: Ord n => Graph n e -> DAG n Source #
Constructs a DAG containing the graph's strongly connected components.
Reachability
reachableFrom :: Ord n => Graph n e -> n -> Map n (Int, [Edge n e]) Source #
reachableFrom g n
is a map containing all nodes reachable from
n
in g
. For each node a simple path to the node is given, along
with its length (the number of edges). The paths are as short as
possible (in terms of the number of edges).
Precondition: n
must be a node in g
. The number of nodes in the
graph must not be larger than
.maxBound
:: Int
Amortised time complexity (assuming that comparisons take constant time): O(e log n), if the lists are not inspected. Inspection of a prefix of a list is linear in the length of the prefix.
walkSatisfying :: Ord n => (Edge n e -> Bool) -> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e] Source #
walkSatisfying every some g from to
determines if there is a
walk from from
to to
in g
, in which every edge satisfies the
predicate every
, and some edge satisfies the predicate some
. If
there are several such walks, then a shortest one (in terms of the
number of edges) is returned.
Precondition: from
and to
must be nodes in g
. The number of
nodes in the graph must not be larger than
.maxBound
:: Int
Amortised time complexity (assuming that comparisons and the predicates take constant time to compute): O(n + e log n).
longestPaths :: forall n e. Ord n => Graph n e -> Graph n (Int, [[Edge n e]]) Source #
Constructs a graph g'
with the same nodes as the original graph
g
. In g'
there is an edge from n1
to n2
if and only if
there is a (possibly empty) simple path from n1
to n2
in g
.
In that case the edge is labelled with all of the longest (in terms
of numbers of edges) simple paths from n1
to n2
in g
, as well
as the lengths of these paths.
Precondition: The graph must be acyclic. The number of nodes in the
graph must not be larger than
.maxBound
:: Int
Worst-case time complexity (if the paths are not inspected): O(e n log n) (this has not been verified carefully).
The algorithm is based on one found on Wikipedia.
Transitive closure
gaussJordanFloydWarshallMcNaughtonYamada :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> (Graph n e, [SCC n]) Source #
Computes the transitive closure of the graph.
Uses the Gauss-Jordan-Floyd-Warshall-McNaughton-Yamada algorithm
(as described by Russell O'Connor in "A Very General Method of
Computing Shortest Paths"
http://r6.ca/blog/20110808T035622Z.html), implemented using
Graph
, and with some shortcuts:
- Zero edge differences are not added to the graph, thus avoiding some zero edges.
- Strongly connected components are used to avoid computing some zero edges.
The graph's strongly connected components (in reverse topological order) are returned along with the transitive closure.
gaussJordanFloydWarshallMcNaughtonYamadaReference :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e Source #
Computes the transitive closure of the graph.
Uses the Gauss-Jordan-Floyd-Warshall-McNaughton-Yamada algorithm (as described by Russell O'Connor in "A Very General Method of Computing Shortest Paths" http://r6.ca/blog/20110808T035622Z.html), implemented using matrices.
The resulting graph does not contain any zero edges.
This algorithm should be seen as a reference implementation. In
practice gaussJordanFloydWarshallMcNaughtonYamada
is likely to be
more efficient.
transitiveClosure :: (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e Source #
The transitive closure. Using gaussJordanFloydWarshallMcNaughtonYamada
.
NOTE: DO NOT USE () AS EDGE LABEL SINCE THIS MEANS EVERY EDGE IS CONSIDERED A ZERO EDGE AND NO
NEW EDGES WILL BE ADDED! Use 'Maybe ()' instead.
transitiveReduction :: Ord n => Graph n e -> Graph n () Source #
The transitive reduction of the graph: a graph with the same reachability relation as the graph, but with as few edges as possible.
Precondition: The graph must be acyclic. The number of nodes in the
graph must not be larger than
.maxBound
:: Int
Worst-case time complexity: O(e n log n) (this has not been verified carefully).
The algorithm is based on one found on Wikipedia.
complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> Graph n e Source #
Transitive closure ported from Agda.Termination.CallGraph.
Relatively efficient, see Issue 1560.
completeIter :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> [(Graph n e, Graph n e)] Source #
Version of complete
that produces a list of intermediate results
paired to the left with a difference that lead to the new intermediat result.
The last element in the list is the transitive closure, paired with the empty graph.
complete g = snd $ last $ completeIter g