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 -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_opt : 'a t -> key -> 'a option
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
    end
  module Lit :
    sig
      type aggregate = {
        left : T.t;
        constructor : const;
        var : T.t;
        guard : T.t;
      }
      type t = LitPos of T.t | LitNeg of T.t | LitAggr of aggregate
      val mk_pos : T.t -> t
      val mk_neg : T.t -> t
      val mk : bool -> T.t -> t
      val mk_aggr :
        left:T.t -> constructor:const -> var:T.t -> guard:T.t -> t
      val eq : t -> t -> bool
      val hash : t -> int
      val to_term : t -> T.t
      val fmap : (T.t -> T.t) -> t -> t
      val to_string : t -> string
      val pp : out_channel -> t -> unit
      val fmt : Format.formatter -> t -> unit
    end
  module C :
    sig
      type t = private { head : T.t; body : Lit.t list; }
      exception Unsafe
      val mk_clause : T.t -> Lit.t list -> t
      val mk_fact : T.t -> t
      val eq : t -> t -> bool
      val hash : t -> int
      val head_symbol : t -> const
      val max_var : t -> int
      val fmap : (T.t -> T.t) -> t -> t
      val to_string : t -> string
      val pp : out_channel -> t -> unit
      val fmt : Format.formatter -> t -> unit
      module Tbl :
        sig
          type key = t
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_opt : 'a t -> key -> 'a option
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
    end
  module Subst :
    sig
      type t
      type scope = int
      type renaming
      val empty : t
      val bind : t -> T.t -> scope -> T.t -> scope -> t
      val deref : t -> T.t -> scope -> T.t * scope
      val create_renaming : unit -> renaming
      val reset_renaming : renaming -> unit
      val rename : renaming:renaming -> T.t -> scope -> T.t
      val eval : t -> renaming:renaming -> T.t -> scope -> T.t
      val eval_lit : t -> renaming:renaming -> Lit.t -> scope -> Lit.t
      val eval_lits :
        t -> renaming:renaming -> Lit.t list -> scope -> Lit.t list
      val eval_clause : t -> renaming:renaming -> C.t -> scope -> C.t
    end
  type scope = Subst.scope
  exception UnifFail
  val unify :
    ?oc:bool -> ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
  val match_ :
    ?oc:bool -> ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
  val alpha_equiv : ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
  val are_alpha_equiv : T.t -> T.t -> bool
  val clause_are_alpha_equiv : C.t -> C.t -> bool
  module BuiltinFun :
    sig
      type t = T.t -> T.t option
      type map
      val create : unit -> map
      val add : map -> Const.t -> t -> unit
      val add_list : map -> (Const.t * t) list -> unit
      val interpreted : map -> Const.t -> bool
      val eval : map -> T.t -> T.t
    end
  module TVariantTbl :
    sig
      type key = T.t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  module CVariantTbl :
    sig
      type key = C.t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  module Index :
    functor (Data : Hashtbl.HashedType) ->
      sig
        type t
        val empty : unit -> t
        val copy : t -> t
        val clear : t -> unit
        val add : t -> T.t -> Data.t -> t
        val remove : t -> T.t -> Data.t -> t
        val generalizations :
          ?oc:bool ->
          t -> scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
        val unify :
          ?oc:bool ->
          t -> scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
        val iter : t -> (T.t -> Data.t -> unit) -> unit
        val size : t -> int
      end
  module Rewriting :
    sig
      type rule = T.t * T.t
      type t
      val create : unit -> t
      val copy : t -> t
      val add : t -> rule -> unit
      val add_list : t -> rule list -> unit
      val to_list : t -> rule list
      val rewrite_root : t -> T.t -> T.t
      val rewrite : t -> T.t -> T.t
    end
  exception NonStratifiedProgram
  module DB :
    sig
      type t
      type interpreter = T.t -> C.t list
      val create : ?parent:t -> unit -> t
      val copy : t -> t
      val clear : t -> unit
      val add_fact : t -> T.t -> unit
      val add_facts : t -> T.t list -> unit
      val add_clause : t -> C.t -> unit
      val add_clauses : t -> C.t list -> unit
      val interpret : ?help:string -> t -> const -> interpreter -> unit
      val interpret_list : t -> (const * string * interpreter) list -> unit
      val is_interpreted : t -> const -> bool
      val add_builtin : t -> Const.t -> BuiltinFun.t -> unit
      val builtin_funs : t -> BuiltinFun.map
      val eval : t -> T.t -> T.t
      val help : t -> string list
      val num_facts : t -> int
      val num_clauses : t -> int
      val size : t -> int
      val find_facts :
        ?oc:bool ->
        t -> scope -> T.t -> scope -> (T.t -> Subst.t -> unit) -> unit
      val find_clauses_head :
        ?oc:bool ->
        t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
      val find_interpretation :
        ?oc:bool ->
        t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
    end
  val ask :
    ?oc:bool ->
    ?with_rules:C.t list -> ?with_facts:T.t list -> DB.t -> T.t -> T.t list
  val ask_lits :
    ?oc:bool ->
    ?with_rules:C.t list ->
    ?with_facts:T.t list -> DB.t -> T.t list -> Lit.t list -> T.t list
  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
  val term_of_string : string -> term
end