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