sig
  module Univ :
    sig
      type t
      type 'a key
      val new_key :
        ?eq:('a -> 'a -> bool) ->
        ?hash:('a -> int) ->
        ?print:('a -> string) -> unit -> 'a CamlInterface.Univ.key
      val pack : key:'a CamlInterface.Univ.key -> 'a -> CamlInterface.Univ.t
      val unpack :
        key:'a CamlInterface.Univ.key -> CamlInterface.Univ.t -> 'a option
      val compatible :
        key:'a CamlInterface.Univ.key -> CamlInterface.Univ.t -> bool
      val eq : CamlInterface.Univ.t -> CamlInterface.Univ.t -> bool
      val hash : CamlInterface.Univ.t -> int
      val print : CamlInterface.Univ.t -> string
      val string : string CamlInterface.Univ.key
      val int : int CamlInterface.Univ.key
      val float : float CamlInterface.Univ.key
      val bool : bool CamlInterface.Univ.key
      val unit : unit CamlInterface.Univ.key
      val pair :
        'a CamlInterface.Univ.key ->
        'b CamlInterface.Univ.key -> ('a * 'b) CamlInterface.Univ.key
      val list : 'a CamlInterface.Univ.key -> 'a list CamlInterface.Univ.key
      val array :
        'a CamlInterface.Univ.key -> 'a array CamlInterface.Univ.key
    end
  type const = CamlInterface.Univ.t
  val of_string : string -> CamlInterface.const
  val of_int : int -> CamlInterface.const
  module Logic :
    sig
      module Const :
        sig
          type t = const
          val equal : t -> t -> bool
          val hash : t -> int
          val to_string : t -> string
          val of_string : string -> t
          val query : t
        end
      type const = Const.t
      val set_debug : bool -> unit
      module T :
        sig
          type t = private Var of int | Apply of const * t array
          val mk_var : int -> t
          val mk_const : const -> t
          val mk_apply : const -> t array -> t
          val mk_apply_l : const -> t list -> t
          val is_var : t -> bool
          val is_apply : t -> bool
          val is_const : t -> bool
          val eq : t -> t -> bool
          val hash : t -> int
          val ground : t -> bool
          val vars : t -> int list
          val max_var : t -> int
          val head_symbol : t -> const
          val to_string : t -> string
          val pp : out_channel -> t -> unit
          val fmt : Format.formatter -> t -> unit
          val pp_tuple : out_channel -> t list -> unit
          module Tbl :
            sig
              type key = t
              type 'a t
              val create : int -> 'a t
              val clear : 'a t -> unit
              val reset : 'a t -> unit
              val copy : 'a t -> 'a t
              val add : 'a t -> key -> 'a -> unit
              val remove : 'a t -> key -> unit
              val find : 'a t -> key -> 'a
              val find_opt : 'a t -> key -> 'a option
              val find_all : 'a t -> key -> 'a list
              val replace : 'a t -> key -> 'a -> unit
              val mem : 'a t -> key -> bool
              val iter : (key -> 'a -> unit) -> 'a t -> unit
              val filter_map_inplace :
                (key -> 'a -> 'a option) -> 'a t -> unit
              val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
              val length : 'a t -> int
              val stats : 'a t -> Hashtbl.statistics
            end
        end
      module Lit :
        sig
          type aggregate = {
            left : T.t;
            constructor : const;
            var : T.t;
            guard : T.t;
          }
          type t = LitPos of T.t | LitNeg of T.t | LitAggr of aggregate
          val mk_pos : T.t -> t
          val mk_neg : T.t -> t
          val mk : bool -> T.t -> t
          val mk_aggr :
            left:T.t -> constructor:const -> var:T.t -> guard:T.t -> t
          val eq : t -> t -> bool
          val hash : t -> int
          val to_term : t -> T.t
          val fmap : (T.t -> T.t) -> t -> t
          val to_string : t -> string
          val pp : out_channel -> t -> unit
          val fmt : Format.formatter -> t -> unit
        end
      module C :
        sig
          type t = private { head : T.t; body : Lit.t list; }
          exception Unsafe
          val mk_clause : T.t -> Lit.t list -> t
          val mk_fact : T.t -> t
          val eq : t -> t -> bool
          val hash : t -> int
          val head_symbol : t -> const
          val max_var : t -> int
          val fmap : (T.t -> T.t) -> t -> t
          val to_string : t -> string
          val pp : out_channel -> t -> unit
          val fmt : Format.formatter -> t -> unit
          module Tbl :
            sig
              type key = t
              type 'a t
              val create : int -> 'a t
              val clear : 'a t -> unit
              val reset : 'a t -> unit
              val copy : 'a t -> 'a t
              val add : 'a t -> key -> 'a -> unit
              val remove : 'a t -> key -> unit
              val find : 'a t -> key -> 'a
              val find_opt : 'a t -> key -> 'a option
              val find_all : 'a t -> key -> 'a list
              val replace : 'a t -> key -> 'a -> unit
              val mem : 'a t -> key -> bool
              val iter : (key -> 'a -> unit) -> 'a t -> unit
              val filter_map_inplace :
                (key -> 'a -> 'a option) -> 'a t -> unit
              val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
              val length : 'a t -> int
              val stats : 'a t -> Hashtbl.statistics
            end
        end
      module Subst :
        sig
          type t
          type scope = int
          type renaming
          val empty : t
          val bind : t -> T.t -> scope -> T.t -> scope -> t
          val deref : t -> T.t -> scope -> T.t * scope
          val create_renaming : unit -> renaming
          val reset_renaming : renaming -> unit
          val rename : renaming:renaming -> T.t -> scope -> T.t
          val eval : t -> renaming:renaming -> T.t -> scope -> T.t
          val eval_lit : t -> renaming:renaming -> Lit.t -> scope -> Lit.t
          val eval_lits :
            t -> renaming:renaming -> Lit.t list -> scope -> Lit.t list
          val eval_clause : t -> renaming:renaming -> C.t -> scope -> C.t
        end
      type scope = Subst.scope
      exception UnifFail
      val unify :
        ?oc:bool -> ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
      val match_ :
        ?oc:bool -> ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
      val alpha_equiv :
        ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
      val are_alpha_equiv : T.t -> T.t -> bool
      val clause_are_alpha_equiv : C.t -> C.t -> bool
      module BuiltinFun :
        sig
          type t = T.t -> T.t option
          type map
          val create : unit -> map
          val add : map -> Const.t -> t -> unit
          val add_list : map -> (Const.t * t) list -> unit
          val interpreted : map -> Const.t -> bool
          val eval : map -> T.t -> T.t
        end
      module TVariantTbl :
        sig
          type key = T.t
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_opt : 'a t -> key -> 'a option
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
      module CVariantTbl :
        sig
          type key = C.t
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_opt : 'a t -> key -> 'a option
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
      module Index :
        functor (Data : Hashtbl.HashedType) ->
          sig
            type t
            val empty : unit -> t
            val copy : t -> t
            val clear : t -> unit
            val add : t -> T.t -> Data.t -> t
            val remove : t -> T.t -> Data.t -> t
            val generalizations :
              ?oc:bool ->
              t ->
              scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
            val unify :
              ?oc:bool ->
              t ->
              scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
            val iter : t -> (T.t -> Data.t -> unit) -> unit
            val size : t -> int
          end
      module Rewriting :
        sig
          type rule = T.t * T.t
          type t
          val create : unit -> t
          val copy : t -> t
          val add : t -> rule -> unit
          val add_list : t -> rule list -> unit
          val to_list : t -> rule list
          val rewrite_root : t -> T.t -> T.t
          val rewrite : t -> T.t -> T.t
        end
      exception NonStratifiedProgram
      module DB :
        sig
          type t
          type interpreter = T.t -> C.t list
          val create : ?parent:t -> unit -> t
          val copy : t -> t
          val clear : t -> unit
          val add_fact : t -> T.t -> unit
          val add_facts : t -> T.t list -> unit
          val add_clause : t -> C.t -> unit
          val add_clauses : t -> C.t list -> unit
          val interpret : ?help:string -> t -> const -> interpreter -> unit
          val interpret_list :
            t -> (const * string * interpreter) list -> unit
          val is_interpreted : t -> const -> bool
          val add_builtin : t -> Const.t -> BuiltinFun.t -> unit
          val builtin_funs : t -> BuiltinFun.map
          val eval : t -> T.t -> T.t
          val help : t -> string list
          val num_facts : t -> int
          val num_clauses : t -> int
          val size : t -> int
          val find_facts :
            ?oc:bool ->
            t -> scope -> T.t -> scope -> (T.t -> Subst.t -> unit) -> unit
          val find_clauses_head :
            ?oc:bool ->
            t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
          val find_interpretation :
            ?oc:bool ->
            t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
        end
      val ask :
        ?oc:bool ->
        ?with_rules:C.t list ->
        ?with_facts:T.t list -> DB.t -> T.t -> T.t list
      val ask_lits :
        ?oc:bool ->
        ?with_rules:C.t list ->
        ?with_facts:T.t list -> DB.t -> T.t list -> Lit.t list -> T.t list
    end
  module Rel1 :
    sig
      type 'a t
      val name : 'a CamlInterface.Rel1.t -> string
      val create :
        ?k:'a CamlInterface.Univ.key -> string -> 'a CamlInterface.Rel1.t
      val get :
        'a CamlInterface.Rel1.t -> CamlInterface.Logic.T.t -> 'a option
      val make : 'a CamlInterface.Rel1.t -> 'a -> CamlInterface.Logic.T.t
      val apply :
        'a CamlInterface.Rel1.t ->
        CamlInterface.Logic.T.t -> CamlInterface.Logic.T.t
      val find :
        CamlInterface.Logic.DB.t -> 'a CamlInterface.Rel1.t -> 'a list
      val subset :
        CamlInterface.Logic.DB.t ->
        'a CamlInterface.Rel1.t -> 'a CamlInterface.Rel1.t -> unit
      val from_fun :
        CamlInterface.Logic.DB.t ->
        'a CamlInterface.Rel1.t -> ('a -> bool) -> unit
      val add_list :
        CamlInterface.Logic.DB.t ->
        'a CamlInterface.Rel1.t -> 'a list -> unit
      val to_string : 'a CamlInterface.Rel1.t -> string
      val fmt : Format.formatter -> 'a CamlInterface.Rel1.t -> unit
    end
  module Rel2 :
    sig
      type ('a, 'b) t
      val name : ('a, 'b) CamlInterface.Rel2.t -> string
      val create :
        ?k1:'a CamlInterface.Univ.key ->
        ?k2:'b CamlInterface.Univ.key ->
        string -> ('a, 'b) CamlInterface.Rel2.t
      val get :
        ('a, 'b) CamlInterface.Rel2.t ->
        CamlInterface.Logic.T.t -> ('a * 'b) option
      val make :
        ('a, 'b) CamlInterface.Rel2.t -> 'a -> 'b -> CamlInterface.Logic.T.t
      val apply :
        ('a, 'b) CamlInterface.Rel2.t ->
        CamlInterface.Logic.T.t ->
        CamlInterface.Logic.T.t -> CamlInterface.Logic.T.t
      val find :
        CamlInterface.Logic.DB.t ->
        ('a, 'b) CamlInterface.Rel2.t -> ('a * 'b) list
      val subset :
        CamlInterface.Logic.DB.t ->
        ('a, 'b) CamlInterface.Rel2.t ->
        ('a, 'b) CamlInterface.Rel2.t -> unit
      val transitive :
        CamlInterface.Logic.DB.t -> ('a, 'a) CamlInterface.Rel2.t -> unit
      val tc_of :
        CamlInterface.Logic.DB.t ->
        tc:('a, 'a) CamlInterface.Rel2.t ->
        ('a, 'a) CamlInterface.Rel2.t -> unit
      val reflexive :
        CamlInterface.Logic.DB.t -> ('a, 'a) CamlInterface.Rel2.t -> unit
      val symmetry :
        CamlInterface.Logic.DB.t -> ('a, 'a) CamlInterface.Rel2.t -> unit
      val from_fun :
        CamlInterface.Logic.DB.t ->
        ('a, 'b) CamlInterface.Rel2.t -> ('a -> 'b -> bool) -> unit
      val add_list :
        CamlInterface.Logic.DB.t ->
        ('a, 'b) CamlInterface.Rel2.t -> ('a * 'b) list -> unit
      val to_string : ('a, 'b) CamlInterface.Rel2.t -> string
      val fmt : Format.formatter -> ('a, 'b) CamlInterface.Rel2.t -> unit
    end
  module Rel3 :
    sig
      type ('a, 'b, 'c) t
      val name : ('a, 'b, 'c) CamlInterface.Rel3.t -> string
      val create :
        ?k1:'a CamlInterface.Univ.key ->
        ?k2:'b CamlInterface.Univ.key ->
        ?k3:'c CamlInterface.Univ.key ->
        string -> ('a, 'b, 'c) CamlInterface.Rel3.t
      val get :
        ('a, 'b, 'c) CamlInterface.Rel3.t ->
        CamlInterface.Logic.T.t -> ('a * 'b * 'c) option
      val make :
        ('a, 'b, 'c) CamlInterface.Rel3.t ->
        'a -> 'b -> 'c -> CamlInterface.Logic.T.t
      val apply :
        ('a, 'b, 'c) CamlInterface.Rel3.t ->
        CamlInterface.Logic.T.t ->
        CamlInterface.Logic.T.t ->
        CamlInterface.Logic.T.t -> CamlInterface.Logic.T.t
      val find :
        CamlInterface.Logic.DB.t ->
        ('a, 'b, 'c) CamlInterface.Rel3.t -> ('a * 'b * 'c) list
      val subset :
        CamlInterface.Logic.DB.t ->
        ('a, 'b, 'c) CamlInterface.Rel3.t ->
        ('a, 'b, 'c) CamlInterface.Rel3.t -> unit
      val from_fun :
        CamlInterface.Logic.DB.t ->
        ('a, 'b, 'c) CamlInterface.Rel3.t -> ('a -> 'b -> 'c -> bool) -> unit
      val add_list :
        CamlInterface.Logic.DB.t ->
        ('a, 'b, 'c) CamlInterface.Rel3.t -> ('a * 'b * 'c) list -> unit
      val to_string : ('a, 'b, 'c) CamlInterface.Rel3.t -> string
      val fmt : Format.formatter -> ('a, 'b, 'c) CamlInterface.Rel3.t -> unit
    end
  module RelList :
    sig
      type 'a t
      val name : 'a CamlInterface.RelList.t -> string
      val create :
        ?k:'a CamlInterface.Univ.key -> string -> 'a CamlInterface.RelList.t
      val get :
        'a CamlInterface.RelList.t ->
        CamlInterface.Logic.T.t -> 'a list option
      val make :
        'a CamlInterface.RelList.t -> 'a list -> CamlInterface.Logic.T.t
    end
  module Parse :
    sig
      type term = Logic.T.t
      type lit = Logic.Lit.t
      type clause = Logic.C.t
      type name_ctx = (string, term) Hashtbl.t
      val create_ctx : unit -> name_ctx
      val term_of_ast : ctx:name_ctx -> TopDownAst.term -> term
      val lit_of_ast : ctx:name_ctx -> TopDownAst.literal -> lit
      val clause_of_ast : ?ctx:name_ctx -> TopDownAst.clause -> clause
      val clauses_of_ast :
        ?ctx:name_ctx -> TopDownAst.clause list -> clause list
      val parse_chan :
        in_channel -> [ `Error of string | `Ok of clause list ]
      val parse_file : string -> [ `Error of string | `Ok of clause list ]
      val parse_string : string -> [ `Error of string | `Ok of clause list ]
      val clause_of_string : string -> clause
      val term_of_string : string -> term
      val load_chan :
        CamlInterface.Logic.DB.t -> Pervasives.in_channel -> bool
      val load_file : CamlInterface.Logic.DB.t -> string -> bool
      val load_string : CamlInterface.Logic.DB.t -> string -> bool
    end
  val add_builtin : CamlInterface.Logic.DB.t -> unit
end