sig
  module type S =
    sig module TD : TopDown.S val setup_handlers : TD.DB.t -> unit end
  module Make :
    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 = '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 -> '-> unit
                    val remove : 'a t -> key -> unit
                    val find : 'a t -> key -> 'a
                    val find_all : 'a t -> key -> 'a list
                    val replace : 'a t -> key -> '-> unit
                    val mem : 'a t -> key -> bool
                    val iter : (key -> '-> unit) -> 'a t -> unit
                    val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 = '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 -> '-> unit
                    val remove : 'a t -> key -> unit
                    val find : 'a t -> key -> 'a
                    val find_all : 'a t -> key -> 'a list
                    val replace : 'a t -> key -> '-> unit
                    val mem : 'a t -> key -> bool
                    val iter : (key -> '-> unit) -> 'a t -> unit
                    val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 = '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 -> '-> unit
                val remove : 'a t -> key -> unit
                val find : 'a t -> key -> 'a
                val find_all : 'a t -> key -> 'a list
                val replace : 'a t -> key -> '-> unit
                val mem : 'a t -> key -> bool
                val iter : (key -> '-> unit) -> 'a t -> unit
                val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                val length : 'a t -> int
                val stats : 'a t -> Hashtbl.statistics
              end
            module CVariantTbl :
              sig
                type key = C.t
                type 'a t = '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 -> '-> unit
                val remove : 'a t -> key -> unit
                val find : 'a t -> key -> 'a
                val find_all : 'a t -> key -> 'a list
                val replace : 'a t -> key -> '-> unit
                val mem : 'a t -> key -> bool
                val iter : (key -> '-> unit) -> 'a t -> unit
                val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 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 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
  module Default :
    sig
      module TD :
        sig
          module Const :
            sig
              type t = TopDown.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 -> '-> unit
                  val remove : 'a t -> key -> unit
                  val find : 'a t -> key -> 'a
                  val find_all : 'a t -> key -> 'a list
                  val replace : 'a t -> key -> '-> unit
                  val mem : 'a t -> key -> bool
                  val iter : (key -> '-> unit) -> 'a t -> unit
                  val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> unit
                  val remove : 'a t -> key -> unit
                  val find : 'a t -> key -> 'a
                  val find_all : 'a t -> key -> 'a list
                  val replace : 'a t -> key -> '-> unit
                  val mem : 'a t -> key -> bool
                  val iter : (key -> '-> unit) -> 'a t -> unit
                  val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> unit
              val remove : 'a t -> key -> unit
              val find : 'a t -> key -> 'a
              val find_all : 'a t -> key -> 'a list
              val replace : 'a t -> key -> '-> unit
              val mem : 'a t -> key -> bool
              val iter : (key -> '-> unit) -> 'a t -> unit
              val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> unit
              val remove : 'a t -> key -> unit
              val find : 'a t -> key -> 'a
              val find_all : 'a t -> key -> 'a list
              val replace : 'a t -> key -> '-> unit
              val mem : 'a t -> key -> bool
              val iter : (key -> '-> unit) -> 'a t -> unit
              val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 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 = TopDown.Default.DB.t
              type interpreter = T.t -> C.t list
              val create : ?parent:t -> unit -> t
              val copy : t -> t
              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
end