package datalog

Legend:
Library
Module
Module type
Parameter
Class
Class type
`type ('a, 'b) t`
`val name : (_, _) t -> string`
`val create : ?k1:'a Univ.key -> ?k2:'b Univ.key -> string -> ('a, 'b) t`
`val get : ('a, 'b) t -> Logic.T.t -> ('a * 'b) option`
`val make : ('a, 'b) t -> 'a -> 'b -> Logic.T.t`
`val apply : (_, _) t -> Logic.T.t -> Logic.T.t -> Logic.T.t`
`val find : Logic.DB.t -> ('a, 'b) t -> ('a * 'b) list`
`val subset : Logic.DB.t -> ('a, 'b) t -> ('a, 'b) t -> unit`

`subset db r1 r2` adds to `db` the axiom that `r2(X,Y) :- r1(X,Y)`; in other words, `r1` is a subset of `r2` as a relation

`val transitive : Logic.DB.t -> ('a, 'a) t -> unit`

Axioms for transitivity are added to the DB

`val tc_of : Logic.DB.t -> tc:('a, 'a) t -> ('a, 'a) t -> unit`

`tc_of db ~tc r` adds to `db` axioms that make the relation `tc` the transitive closure of the relation `r`.

`val reflexive : Logic.DB.t -> ('a, 'a) t -> unit`

`reflexive db r` makes `r` reflexive in `db`, ie for all `X`, `r(X,X)` holds in `db`.

`val symmetry : Logic.DB.t -> ('a, 'a) t -> unit`

Axiom for symmetry (ie "r(X,Y) <=> r(Y,X)") added to the DB

`val from_fun : Logic.DB.t -> ('a, 'b) t -> ('a -> 'b -> bool) -> unit`

The given function decides of the given relation (if it returns true for a couple of constants, then the relation holds for those constants)

`val add_list : Logic.DB.t -> ('a, 'b) t -> ('a * 'b) list -> unit`

`val to_string : (_, _) t -> string`
`val fmt : Format.formatter -> (_, _) t -> unit`