sig
  module type CONST =
    sig
      type t
      val equal : TopDown.CONST.t -> TopDown.CONST.t -> bool
      val hash : TopDown.CONST.t -> int
      val to_string : TopDown.CONST.t -> string
      val of_string : string -> TopDown.CONST.t
      val query : TopDown.CONST.t
    end
  module type S =
    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 -> '-> 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 : 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 -> '-> 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 : 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 -> '-> 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 -> TopDown.S.Index.t
            val copy : TopDown.S.Index.t -> TopDown.S.Index.t
            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 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
  module Make :
    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 -> '-> 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
            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
  module type PARSABLE_CONST =
    sig
      type t
      val of_string : string -> TopDown.PARSABLE_CONST.t
      val of_int : int -> TopDown.PARSABLE_CONST.t
    end
  module type PARSE =
    sig
      type term
      type lit
      type clause
      type name_ctx = (string, TopDown.PARSE.term) Hashtbl.t
      val create_ctx : unit -> TopDown.PARSE.name_ctx
      val term_of_ast :
        ctx:TopDown.PARSE.name_ctx -> TopDownAst.term -> TopDown.PARSE.term
      val lit_of_ast :
        ctx:TopDown.PARSE.name_ctx -> TopDownAst.literal -> TopDown.PARSE.lit
      val clause_of_ast :
        ?ctx:TopDown.PARSE.name_ctx ->
        TopDownAst.clause -> TopDown.PARSE.clause
      val clauses_of_ast :
        ?ctx:TopDown.PARSE.name_ctx ->
        TopDownAst.clause list -> TopDown.PARSE.clause list
      val parse_chan :
        Pervasives.in_channel ->
        [ `Error of string | `Ok of TopDown.PARSE.clause list ]
      val parse_file :
        string -> [ `Error of string | `Ok of TopDown.PARSE.clause list ]
      val parse_string :
        string -> [ `Error of string | `Ok of TopDown.PARSE.clause list ]
      val clause_of_string : string -> TopDown.PARSE.clause
    end
  module MakeParse :
    functor (C : PARSABLE_CONST->
      functor
        (TD : sig
                module Const :
                  sig
                    type t = C.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 -> '-> 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
                    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->
        sig
          type term = TD.T.t
          type lit = TD.Lit.t
          type clause = TD.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
        end
  type const = Int of int | String of string
  module Default :
    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 -> '-> 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
          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
      val default_interpreters :
        (TopDown.const * string * DB.interpreter) list
      val builtin : (TopDown.const * BuiltinFun.t) list
      val setup_default : DB.t -> unit
      type term = T.t
      type lit = Lit.t
      type clause = 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
    end
end