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