sig
  module Const : CONST
  type const = Const.t
  val set_debug : bool -> unit
  module T :
    sig
      type t = private
          Var of int
        | Apply of TopDown.S.const * TopDown.S.T.t array
      val mk_var : int -> TopDown.S.T.t
      val mk_const : TopDown.S.const -> TopDown.S.T.t
      val mk_apply : TopDown.S.const -> TopDown.S.T.t array -> TopDown.S.T.t
      val mk_apply_l : TopDown.S.const -> TopDown.S.T.t list -> TopDown.S.T.t
      val is_var : TopDown.S.T.t -> bool
      val is_apply : TopDown.S.T.t -> bool
      val is_const : TopDown.S.T.t -> bool
      val eq : TopDown.S.T.t -> TopDown.S.T.t -> bool
      val hash : TopDown.S.T.t -> int
      val ground : TopDown.S.T.t -> bool
      val vars : TopDown.S.T.t -> int list
      val max_var : TopDown.S.T.t -> int
      val head_symbol : TopDown.S.T.t -> TopDown.S.const
      val to_string : TopDown.S.T.t -> string
      val pp : Pervasives.out_channel -> TopDown.S.T.t -> unit
      val fmt : Format.formatter -> TopDown.S.T.t -> unit
      val pp_tuple : Pervasives.out_channel -> TopDown.S.T.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 : TopDown.S.T.t;
        constructor : TopDown.S.const;
        var : TopDown.S.T.t;
        guard : TopDown.S.T.t;
      }
      type t =
          LitPos of TopDown.S.T.t
        | LitNeg of TopDown.S.T.t
        | LitAggr of TopDown.S.Lit.aggregate
      val mk_pos : TopDown.S.T.t -> TopDown.S.Lit.t
      val mk_neg : TopDown.S.T.t -> TopDown.S.Lit.t
      val mk : bool -> TopDown.S.T.t -> TopDown.S.Lit.t
      val mk_aggr :
        left:TopDown.S.T.t ->
        constructor:TopDown.S.const ->
        var:TopDown.S.T.t -> guard:TopDown.S.T.t -> TopDown.S.Lit.t
      val eq : TopDown.S.Lit.t -> TopDown.S.Lit.t -> bool
      val hash : TopDown.S.Lit.t -> int
      val to_term : TopDown.S.Lit.t -> TopDown.S.T.t
      val fmap :
        (TopDown.S.T.t -> TopDown.S.T.t) ->
        TopDown.S.Lit.t -> TopDown.S.Lit.t
      val to_string : TopDown.S.Lit.t -> string
      val pp : Pervasives.out_channel -> TopDown.S.Lit.t -> unit
      val fmt : Format.formatter -> TopDown.S.Lit.t -> unit
    end
  module C :
    sig
      type t = private { head : TopDown.S.T.t; body : TopDown.S.Lit.t list; }
      exception Unsafe
      val mk_clause : TopDown.S.T.t -> TopDown.S.Lit.t list -> TopDown.S.C.t
      val mk_fact : TopDown.S.T.t -> TopDown.S.C.t
      val eq : TopDown.S.C.t -> TopDown.S.C.t -> bool
      val hash : TopDown.S.C.t -> int
      val head_symbol : TopDown.S.C.t -> TopDown.S.const
      val max_var : TopDown.S.C.t -> int
      val fmap :
        (TopDown.S.T.t -> TopDown.S.T.t) -> TopDown.S.C.t -> TopDown.S.C.t
      val to_string : TopDown.S.C.t -> string
      val pp : Pervasives.out_channel -> TopDown.S.C.t -> unit
      val fmt : Format.formatter -> TopDown.S.C.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 : TopDown.S.Subst.t
      val bind :
        TopDown.S.Subst.t ->
        TopDown.S.T.t ->
        TopDown.S.Subst.scope ->
        TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.Subst.t
      val deref :
        TopDown.S.Subst.t ->
        TopDown.S.T.t ->
        TopDown.S.Subst.scope -> TopDown.S.T.t * TopDown.S.Subst.scope
      val create_renaming : unit -> TopDown.S.Subst.renaming
      val reset_renaming : TopDown.S.Subst.renaming -> unit
      val rename :
        renaming:TopDown.S.Subst.renaming ->
        TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
      val eval :
        TopDown.S.Subst.t ->
        renaming:TopDown.S.Subst.renaming ->
        TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
      val eval_lit :
        TopDown.S.Subst.t ->
        renaming:TopDown.S.Subst.renaming ->
        TopDown.S.Lit.t -> TopDown.S.Subst.scope -> TopDown.S.Lit.t
      val eval_lits :
        TopDown.S.Subst.t ->
        renaming:TopDown.S.Subst.renaming ->
        TopDown.S.Lit.t list -> TopDown.S.Subst.scope -> TopDown.S.Lit.t list
      val eval_clause :
        TopDown.S.Subst.t ->
        renaming:TopDown.S.Subst.renaming ->
        TopDown.S.C.t -> TopDown.S.Subst.scope -> TopDown.S.C.t
    end
  type scope = TopDown.S.Subst.scope
  exception UnifFail
  val unify :
    ?oc:bool ->
    ?subst:TopDown.S.Subst.t ->
    TopDown.S.T.t ->
    TopDown.S.scope -> TopDown.S.T.t -> TopDown.S.scope -> TopDown.S.Subst.t
  val match_ :
    ?oc:bool ->
    ?subst:TopDown.S.Subst.t ->
    TopDown.S.T.t ->
    TopDown.S.scope -> TopDown.S.T.t -> TopDown.S.scope -> TopDown.S.Subst.t
  val alpha_equiv :
    ?subst:TopDown.S.Subst.t ->
    TopDown.S.T.t ->
    TopDown.S.scope -> TopDown.S.T.t -> TopDown.S.scope -> TopDown.S.Subst.t
  val are_alpha_equiv : TopDown.S.T.t -> TopDown.S.T.t -> bool
  val clause_are_alpha_equiv : TopDown.S.C.t -> TopDown.S.C.t -> bool
  module BuiltinFun :
    sig
      type t = TopDown.S.T.t -> TopDown.S.T.t option
      type map
      val create : unit -> TopDown.S.BuiltinFun.map
      val add :
        TopDown.S.BuiltinFun.map -> Const.t -> TopDown.S.BuiltinFun.t -> unit
      val add_list :
        TopDown.S.BuiltinFun.map ->
        (Const.t * TopDown.S.BuiltinFun.t) list -> unit
      val interpreted : TopDown.S.BuiltinFun.map -> Const.t -> bool
      val eval : TopDown.S.BuiltinFun.map -> TopDown.S.T.t -> TopDown.S.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 -> TopDown.S.Index.t
        val copy : TopDown.S.Index.t -> TopDown.S.Index.t
        val clear : TopDown.S.Index.t -> unit
        val add :
          TopDown.S.Index.t -> TopDown.S.T.t -> Data.t -> TopDown.S.Index.t
        val remove :
          TopDown.S.Index.t -> TopDown.S.T.t -> Data.t -> TopDown.S.Index.t
        val generalizations :
          ?oc:bool ->
          TopDown.S.Index.t ->
          TopDown.S.scope ->
          TopDown.S.T.t ->
          TopDown.S.scope -> (Data.t -> TopDown.S.Subst.t -> unit) -> unit
        val unify :
          ?oc:bool ->
          TopDown.S.Index.t ->
          TopDown.S.scope ->
          TopDown.S.T.t ->
          TopDown.S.scope -> (Data.t -> TopDown.S.Subst.t -> unit) -> unit
        val iter :
          TopDown.S.Index.t -> (TopDown.S.T.t -> Data.t -> unit) -> unit
        val size : TopDown.S.Index.t -> int
      end
  module Rewriting :
    sig
      type rule = TopDown.S.T.t * TopDown.S.T.t
      type t
      val create : unit -> TopDown.S.Rewriting.t
      val copy : TopDown.S.Rewriting.t -> TopDown.S.Rewriting.t
      val add : TopDown.S.Rewriting.t -> TopDown.S.Rewriting.rule -> unit
      val add_list :
        TopDown.S.Rewriting.t -> TopDown.S.Rewriting.rule list -> unit
      val to_list : TopDown.S.Rewriting.t -> TopDown.S.Rewriting.rule list
      val rewrite_root :
        TopDown.S.Rewriting.t -> TopDown.S.T.t -> TopDown.S.T.t
      val rewrite : TopDown.S.Rewriting.t -> TopDown.S.T.t -> TopDown.S.T.t
    end
  exception NonStratifiedProgram
  module DB :
    sig
      type t
      type interpreter = TopDown.S.T.t -> TopDown.S.C.t list
      val create : ?parent:TopDown.S.DB.t -> unit -> TopDown.S.DB.t
      val copy : TopDown.S.DB.t -> TopDown.S.DB.t
      val clear : TopDown.S.DB.t -> unit
      val add_fact : TopDown.S.DB.t -> TopDown.S.T.t -> unit
      val add_facts : TopDown.S.DB.t -> TopDown.S.T.t list -> unit
      val add_clause : TopDown.S.DB.t -> TopDown.S.C.t -> unit
      val add_clauses : TopDown.S.DB.t -> TopDown.S.C.t list -> unit
      val interpret :
        ?help:string ->
        TopDown.S.DB.t -> TopDown.S.const -> TopDown.S.DB.interpreter -> unit
      val interpret_list :
        TopDown.S.DB.t ->
        (TopDown.S.const * string * TopDown.S.DB.interpreter) list -> unit
      val is_interpreted : TopDown.S.DB.t -> TopDown.S.const -> bool
      val add_builtin :
        TopDown.S.DB.t -> Const.t -> TopDown.S.BuiltinFun.t -> unit
      val builtin_funs : TopDown.S.DB.t -> TopDown.S.BuiltinFun.map
      val eval : TopDown.S.DB.t -> TopDown.S.T.t -> TopDown.S.T.t
      val help : TopDown.S.DB.t -> string list
      val num_facts : TopDown.S.DB.t -> int
      val num_clauses : TopDown.S.DB.t -> int
      val size : TopDown.S.DB.t -> int
      val find_facts :
        ?oc:bool ->
        TopDown.S.DB.t ->
        TopDown.S.scope ->
        TopDown.S.T.t ->
        TopDown.S.scope ->
        (TopDown.S.T.t -> TopDown.S.Subst.t -> unit) -> unit
      val find_clauses_head :
        ?oc:bool ->
        TopDown.S.DB.t ->
        TopDown.S.scope ->
        TopDown.S.T.t ->
        TopDown.S.scope ->
        (TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
      val find_interpretation :
        ?oc:bool ->
        TopDown.S.DB.t ->
        TopDown.S.scope ->
        TopDown.S.T.t ->
        TopDown.S.scope ->
        (TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
    end
  val ask :
    ?oc:bool ->
    ?with_rules:TopDown.S.C.t list ->
    ?with_facts:TopDown.S.T.t list ->
    TopDown.S.DB.t -> TopDown.S.T.t -> TopDown.S.T.t list
  val ask_lits :
    ?oc:bool ->
    ?with_rules:TopDown.S.C.t list ->
    ?with_facts:TopDown.S.T.t list ->
    TopDown.S.DB.t ->
    TopDown.S.T.t list -> TopDown.S.Lit.t list -> TopDown.S.T.t list
end