functor (TD : TopDown.S) ->
  sig
    module TD :
      sig
        module Const :
          sig
            type t = TD.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 = TD.T.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 = 'a TD.T.Tbl.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 =
              TD.Lit.aggregate = {
              left : T.t;
              constructor : const;
              var : T.t;
              guard : T.t;
            }
            type t =
              TD.Lit.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 = TD.C.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 = 'a TD.C.Tbl.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 = TD.Subst.t
            type scope = int
            type renaming = TD.Subst.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 = TD.BuiltinFun.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 = 'a TD.TVariantTbl.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 = 'a TD.CVariantTbl.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 = TD.Index(Data).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 = TD.Rewriting.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 = TD.DB.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
    val setup_handlers : TD.DB.t -> unit
  end