functor (Const : CONST) ->
  sig
    module Const :
      sig
        type t = Const.t
        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