Module CamlInterface.Rel2

module Rel2: sig .. end

type ('a, 'b) t

val name : ('a, 'b) t -> string

val create : ?k1:'a CamlInterface.Univ.key ->
       ?k2:'b CamlInterface.Univ.key -> string -> ('a, 'b) t

val get : ('a, 'b) t -> CamlInterface.Logic.T.t -> ('a * 'b) option

val make : ('a, 'b) t -> 'a -> 'b -> CamlInterface.Logic.T.t

val apply : ('a, 'b) t ->
       CamlInterface.Logic.T.t -> CamlInterface.Logic.T.t -> CamlInterface.Logic.T.t

val find : CamlInterface.Logic.DB.t -> ('a, 'b) t -> ('a * 'b) list

val subset : CamlInterface.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 : CamlInterface.Logic.DB.t -> ('a, 'a) t -> unit

Axioms for transitivity are added to the DB

val tc_of : CamlInterface.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 : CamlInterface.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 : CamlInterface.Logic.DB.t -> ('a, 'a) t -> unit

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

val from_fun : CamlInterface.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 : CamlInterface.Logic.DB.t ->
       ('a, 'b) t -> ('a * 'b) list -> unit

Add given list of axioms

val to_string : ('a, 'b) t -> string

val fmt : Format.formatter -> ('a, 'b) t -> unit