sig
  module Univ :
    sig
      type t
      type 'a embedding
      val embed : unit -> 'a BottomUp.Univ.embedding
      val pack : 'a BottomUp.Univ.embedding -> 'a -> BottomUp.Univ.t
      val unpack : 'a BottomUp.Univ.embedding -> BottomUp.Univ.t -> 'a option
      val compatible : 'a BottomUp.Univ.embedding -> BottomUp.Univ.t -> bool
    end
  module type S =
    sig
      type symbol
      type term = private Var of int | Const of BottomUp.S.symbol
      val mk_var : int -> BottomUp.S.term
      val mk_const : BottomUp.S.symbol -> BottomUp.S.term
      type literal
      type clause
      type soft_lit = BottomUp.S.symbol * BottomUp.S.term list
      type soft_clause = BottomUp.S.soft_lit * BottomUp.S.soft_lit list
      val mk_literal :
        BottomUp.S.symbol -> BottomUp.S.term list -> BottomUp.S.literal
      val of_soft_lit : BottomUp.S.soft_lit -> BottomUp.S.literal
      val open_literal : BottomUp.S.literal -> BottomUp.S.soft_lit
      val mk_clause :
        BottomUp.S.literal -> BottomUp.S.literal list -> BottomUp.S.clause
      val of_soft_clause : BottomUp.S.soft_clause -> BottomUp.S.clause
      val open_clause : BottomUp.S.clause -> BottomUp.S.soft_clause
      val is_ground : BottomUp.S.literal -> bool
      val arity : BottomUp.S.literal -> int
      val eq_term : BottomUp.S.term -> BottomUp.S.term -> bool
      val eq_literal : BottomUp.S.literal -> BottomUp.S.literal -> bool
      val hash_literal : BottomUp.S.literal -> int
      val check_safe : BottomUp.S.clause -> bool
      val is_fact : BottomUp.S.clause -> bool
      val eq_clause : BottomUp.S.clause -> BottomUp.S.clause -> bool
      val hash_clause : BottomUp.S.clause -> int
      val pp_term : Format.formatter -> BottomUp.S.term -> unit
      val pp_literal : Format.formatter -> BottomUp.S.literal -> unit
      val pp_clause : Format.formatter -> BottomUp.S.clause -> unit
      val quantify1 : (BottomUp.S.term -> 'a) -> 'a
      val quantify2 : (BottomUp.S.term -> BottomUp.S.term -> 'a) -> 'a
      val quantify3 :
        (BottomUp.S.term -> BottomUp.S.term -> BottomUp.S.term -> 'a) -> 'a
      val quantify4 :
        (BottomUp.S.term ->
         BottomUp.S.term -> BottomUp.S.term -> BottomUp.S.term -> 'a) ->
        'a
      val quantifyn : int -> (BottomUp.S.term list -> 'a) -> 'a
      exception UnsafeClause
      type db
      type explanation =
          Axiom
        | Resolution of BottomUp.S.clause * BottomUp.S.literal
        | ExtExplanation of string * BottomUp.Univ.t
      val db_create : unit -> BottomUp.S.db
      val db_copy : BottomUp.S.db -> BottomUp.S.db
      val db_mem : BottomUp.S.db -> BottomUp.S.clause -> bool
      val db_add :
        ?expl:BottomUp.S.explanation ->
        BottomUp.S.db -> BottomUp.S.clause -> unit
      val db_add_fact :
        ?expl:BottomUp.S.explanation ->
        BottomUp.S.db -> BottomUp.S.literal -> unit
      val db_goal : BottomUp.S.db -> BottomUp.S.literal -> unit
      val db_match :
        BottomUp.S.db ->
        BottomUp.S.literal -> (BottomUp.S.literal -> unit) -> unit
      val db_query :
        BottomUp.S.db ->
        BottomUp.S.literal ->
        int list -> (BottomUp.S.symbol list -> unit) -> unit
      val db_size : BottomUp.S.db -> int
      val db_fold :
        ('a -> BottomUp.S.clause -> 'a) -> 'a -> BottomUp.S.db -> 'a
      type fact_handler = BottomUp.S.literal -> unit
      type goal_handler = BottomUp.S.literal -> unit
      val db_subscribe_fact :
        BottomUp.S.db -> BottomUp.S.symbol -> BottomUp.S.fact_handler -> unit
      val db_subscribe_all_facts :
        BottomUp.S.db -> BottomUp.S.fact_handler -> unit
      val db_subscribe_goal :
        BottomUp.S.db -> BottomUp.S.goal_handler -> unit
      type user_fun = BottomUp.S.soft_lit -> BottomUp.S.soft_lit
      val db_add_fun :
        BottomUp.S.db -> BottomUp.S.symbol -> BottomUp.S.user_fun -> unit
      val db_goals : BottomUp.S.db -> (BottomUp.S.literal -> unit) -> unit
      val db_explain :
        BottomUp.S.db -> BottomUp.S.literal -> BottomUp.S.literal list
      val db_premises :
        BottomUp.S.db ->
        BottomUp.S.literal -> BottomUp.S.clause * BottomUp.S.literal list
      val db_explanations :
        BottomUp.S.db -> BottomUp.S.clause -> BottomUp.S.explanation list
      module Query :
        sig
          type set
          val ask :
            BottomUp.S.db ->
            ?neg:BottomUp.S.literal list ->
            int array -> BottomUp.S.literal list -> BottomUp.S.Query.set
          val iter :
            BottomUp.S.Query.set -> (BottomUp.S.term array -> unit) -> unit
          val to_list : BottomUp.S.Query.set -> BottomUp.S.term array list
          val cardinal : BottomUp.S.Query.set -> int
          val pp_plan : Format.formatter -> BottomUp.S.Query.set -> unit
        end
    end
  module type SymbolType =
    sig
      type t
      val equal : t -> t -> bool
      val hash : t -> int
      val to_string : t -> string
    end
  module Hashcons :
    functor (S : SymbolType) ->
      sig
        type t = S.t
        val equal : t -> t -> bool
        val hash : t -> int
        val to_string : t -> string
        val make : S.t -> S.t
      end
  module Make :
    functor (Symbol : SymbolType) ->
      sig
        type symbol = Symbol.t
        type term = private Var of int | Const of symbol
        val mk_var : int -> term
        val mk_const : symbol -> term
        type literal
        type clause
        type soft_lit = symbol * term list
        type soft_clause = soft_lit * soft_lit list
        val mk_literal : symbol -> term list -> literal
        val of_soft_lit : soft_lit -> literal
        val open_literal : literal -> soft_lit
        val mk_clause : literal -> literal list -> clause
        val of_soft_clause : soft_clause -> clause
        val open_clause : clause -> soft_clause
        val is_ground : literal -> bool
        val arity : literal -> int
        val eq_term : term -> term -> bool
        val eq_literal : literal -> literal -> bool
        val hash_literal : literal -> int
        val check_safe : clause -> bool
        val is_fact : clause -> bool
        val eq_clause : clause -> clause -> bool
        val hash_clause : clause -> int
        val pp_term : Format.formatter -> term -> unit
        val pp_literal : Format.formatter -> literal -> unit
        val pp_clause : Format.formatter -> clause -> unit
        val quantify1 : (term -> 'a) -> 'a
        val quantify2 : (term -> term -> 'a) -> 'a
        val quantify3 : (term -> term -> term -> 'a) -> 'a
        val quantify4 : (term -> term -> term -> term -> 'a) -> 'a
        val quantifyn : int -> (term list -> 'a) -> 'a
        exception UnsafeClause
        type db
        type explanation =
            Axiom
          | Resolution of clause * literal
          | ExtExplanation of string * Univ.t
        val db_create : unit -> db
        val db_copy : db -> db
        val db_mem : db -> clause -> bool
        val db_add : ?expl:explanation -> db -> clause -> unit
        val db_add_fact : ?expl:explanation -> db -> literal -> unit
        val db_goal : db -> literal -> unit
        val db_match : db -> literal -> (literal -> unit) -> unit
        val db_query :
          db -> literal -> int list -> (symbol list -> unit) -> unit
        val db_size : db -> int
        val db_fold : ('a -> clause -> 'a) -> 'a -> db -> 'a
        type fact_handler = literal -> unit
        type goal_handler = literal -> unit
        val db_subscribe_fact : db -> symbol -> fact_handler -> unit
        val db_subscribe_all_facts : db -> fact_handler -> unit
        val db_subscribe_goal : db -> goal_handler -> unit
        type user_fun = soft_lit -> soft_lit
        val db_add_fun : db -> symbol -> user_fun -> unit
        val db_goals : db -> (literal -> unit) -> unit
        val db_explain : db -> literal -> literal list
        val db_premises : db -> literal -> clause * literal list
        val db_explanations : db -> clause -> explanation list
        module Query :
          sig
            type set
            val ask :
              db -> ?neg:literal list -> int array -> literal list -> set
            val iter : set -> (term array -> unit) -> unit
            val to_list : set -> term array list
            val cardinal : set -> int
            val pp_plan : Format.formatter -> set -> unit
          end
      end
end