sig
  module StringSymbol :
    sig
      type t = string
      val equal : t -> t -> bool
      val hash : t -> int
      val to_string : t -> string
    end
  type symbol = string
  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 * BottomUp.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 : ('-> clause -> '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
  type vartbl = {
    mutable vartbl_count : int;
    vartbl_tbl : (string, int) Hashtbl.t;
  }
  val mk_vartbl : unit -> Default.vartbl
  val literal_of_ast : ?tbl:Default.vartbl -> BottomUpAst.literal -> literal
  val clause_of_ast : BottomUpAst.clause -> clause
  val query_of_ast :
    BottomUpAst.query -> int array * literal list * literal list
end