Module LogtkLazyGraph

module LogtkLazyGraph: sig .. end

Lazy graph polymorphic data structure

This module serves to represent directed graphs in a lazy fashion. Such a graph is always accessed from a given initial node (so only connected components can be represented by a single value of type ('v,'e) t).

The default equality considered here is (=), and the default hash function is Hashtbl.hash.

LogtkType definitions

type ('id, 'v, 'e) t = {
   eq : 'id -> 'id -> bool;
   hash : 'id -> int;
   force : 'id -> ('id, 'v, 'e) node;
Lazy graph structure. Vertices, that have unique identifiers of type 'id, are annotated with values of type 'v, and edges are annotated by type 'e. A graph is a function that maps each identifier to a label and some edges to other vertices, or to Empty if the identifier is not part of the graph.
type ('id, 'v, 'e) node = 
| Empty
| Node of 'id * 'v * ('e * 'id) Sequence.t (*
A single node of the graph, with outgoing edges
type ('id, 'e) path = ('id * 'e * 'id) list 
A reverse path (from the last element of the path to the first).

Basic constructors

It is difficult to provide generic combinators to build graphs. The problem is that if one wants to "update" a node, it's still very hard to update how other nodes re-generate the current node at the same time. The best way to do it is to build one function that maps the underlying structure of the type vertex to a graph (for instance, a concrete data structure, or an URL...).
val empty : ('id, 'v, 'e) t
Empty graph
val singleton : ?eq:('id -> 'id -> bool) ->
?hash:('id -> int) -> 'id -> 'v -> ('id, 'v, 'e) t
Trivial graph, composed of one node
val make : ?eq:('id -> 'id -> bool) ->
?hash:('id -> int) ->
('id -> ('id, 'v, 'e) node) -> ('id, 'v, 'e) t
Build a graph from the force function
val from_enum : ?eq:('id -> 'id -> bool) ->
?hash:('id -> int) ->
vertices:('id * 'v) Sequence.t ->
edges:('id * 'e * 'id) Sequence.t -> ('id, 'v, 'e) t
Concrete (eager) representation of a Graph
val from_list : ?eq:('id -> 'id -> bool) ->
?hash:('id -> int) ->
('id * 'e * 'id) list -> ('id, 'id, 'e) t
Simple way to generate a graph, from a list of edges
val from_fun : ?eq:('id -> 'id -> bool) ->
?hash:('id -> int) ->
('id -> ('v * ('e * 'id) list) option) -> ('id, 'v, 'e) t
Convenient semi-lazy implementation of graphs

Mutable concrete implementation

type ('id, 'v, 'e) graph = ('id, 'v, 'e) t 
module Mutable: sig .. end


module Full: sig .. end
Full interface to traversals

The traversal functions assign a unique ID to every traversed node
val bfs : ('id, 'v, 'e) t -> 'id -> ('id * 'v * int) Sequence.t
Lazy traversal in breadth first
val dfs : ('id, 'v, 'e) t -> 'id -> ('id * 'v * int) Sequence.t
Lazy traversal in depth first
module Heap: sig .. end
val a_star : ('id, 'v, 'e) t ->
?on_explore:('id -> unit) ->
?ignore:('id -> bool) ->
?heuristic:('id -> float) ->
?distance:('id -> 'e -> 'id -> float) ->
goal:('id -> bool) ->
'id -> (float * ('id, 'e) path) Sequence.t
Shortest path from the first node to nodes that satisfy goal, according to the given (positive!) distance function. The distance is also returned. ignore allows one to ignore some vertices during exploration. heuristic indicates the estimated distance to some goal, and must be
val dijkstra : ('id, 'v, 'e) t ->
?on_explore:('id -> unit) ->
?ignore:('id -> bool) ->
?distance:('id -> 'e -> 'id -> float) ->
'id -> 'id -> float * ('id, 'e) path
Shortest path from the first node to the second one, according to the given (positive!) distance function. ignore allows one to ignore some vertices during exploration. This raises Not_found if no path could be found.
val is_dag : ('id, 'a, 'b) t -> 'id -> bool
Is the subgraph explorable from the given vertex, a Directed Acyclic Graph?
val is_dag_full : ('id, 'a, 'b) t -> 'id Sequence.t -> bool
Is the Graph reachable from the given vertices, a DAG? See LogtkLazyGraph.is_dag
val find_cycle : ('id, 'a, 'e) t -> 'id -> ('id, 'e) path
Find a cycle in the given graph.
Raises Not_found if the graph is acyclic
val rev_path : ('id, 'e) path -> ('id, 'e) path
Reverse the path

Lazy transformations

val union : ?combine:('v -> 'v -> 'v) ->
('id, 'v, 'e) t ->
('id, 'v, 'e) t -> ('id, 'v, 'e) t
Lazy union of the two graphs. If they have common vertices, combine is used to combine the labels. By default, the second label is dropped and only the first is kept
val map : vertices:('v -> 'v2) ->
edges:('e -> 'e2) ->
('id, 'v, 'e) t -> ('id, 'v2, 'e2) t
Map vertice and edge labels
val flatMap : ('id -> 'id Sequence.t) ->
('id, 'v, 'e) t -> ('id, 'v, 'e) t
Replace each vertex by some vertices. By mapping v' to f v'=v1,...,vn, whenever v ---e---> v', then v --e--> vi for i=1,...,n. Optional functions can be used to transform labels for edges and vertices.
val filter : ?vertices:('id -> 'v -> bool) ->
?edges:('id -> 'e -> 'id -> bool) ->
('id, 'v, 'e) t -> ('id, 'v, 'e) t
Filter out vertices and edges that do not satisfy the given predicates. The default predicates always return true.
val product : ('id1, 'v1, 'e1) t ->
('id2, 'v2, 'e2) t ->
('id1 * 'id2, 'v1 * 'v2, 'e1 * 'e2) t
Cartesian product of the two graphs
module Infix: sig .. end
module Dot: sig .. end
Pretty printing in the DOT (graphviz) format

Example of graphs

val divisors_graph : (int, int, unit) t
val collatz_graph : (int, int, unit) t
If n is even, n points to n/2, otherwise to 3n+1
val collatz_graph_bis : (int, int, bool) t
Same as LogtkLazyGraph.collatz_graph, but also with reverse edges (n -> n*2, and n -> (n-1)/3 if n mod 3 = 1. Direct edges annotated with true, reverse edges with false
val heap_graph : (int, int, unit) t
maps an integer i to 2*i and 2*i+1