package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Lazy graph polymorphic data structure

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Map
  - Pos
  - Seq
  - Set
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFormula
  - FO
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Make
    
    Base
    
    Map
    
    MyT
    
    Seq
    
    Set
    
    TPTP
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Map
    
    From
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    To
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - S
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - TERM
    
    Seq
    
    Set
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Map
  - Pos
  - Seq
  - Set
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    H
    
    X
  - S
    
    H
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
    
    X
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
    
    X
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
    
    X
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Map
  - Pos
  - Seq
  - Set
  - Tbl
- LogtkSignature
  - SMap
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Map
  - Seq
  - Set
  - TPTP
    
    Arith
  - Tbl
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Map
  - Seq
  - Set
  - Subst
  - Tbl
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

and ('id, 'v, 'e) node =

| Empty
| Node of 'id * 'v * ('e * 'id) Sequence.t
(*
A single node of the graph, with outgoing edges
*)

and ('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

Traversals

module Full : sig ... end

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

admissible (ie, it never overestimates the actual distance);
consistent (ie, h(X) <= dist(X,Y) + h(Y)). Both the distance and the heuristic must always be positive or null.

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, _, _) t -> 'id -> bool

Is the subgraph explorable from the given vertex, a Directed Acyclic Graph?

val is_dag_full : ('id, _, _) t -> 'id Sequence.t -> bool

Is the Graph reachable from the given vertices, a DAG? See is_dag

val find_cycle : ('id, _, '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 flat_map : ('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

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 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