sig
  module Univ :
    sig
      type t
      type 'a embedding
      val embed : unit -> 'Datalog.Univ.embedding
      val pack : 'Datalog.Univ.embedding -> '-> Datalog.Univ.t
      val unpack : 'Datalog.Univ.embedding -> Datalog.Univ.t -> 'a option
      val compatible : 'Datalog.Univ.embedding -> Datalog.Univ.t -> bool
    end
  module type S =
    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
  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
        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 : ('-> 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
      end
  module Ast :
    sig
      type file = Datalog.Ast.clause list
      and clause = Clause of Datalog.Ast.literal * Datalog.Ast.literal list
      and literal = Atom of string * Datalog.Ast.term list
      and term = Var of string | Const of string | Quoted of string
      and query =
          Query of Datalog.Ast.term list * Datalog.Ast.literal list *
            Datalog.Ast.literal list
    end
  module Parser :
    sig
      type token
      val parse_literal :
        (Lexing.lexbuf -> Datalog.Parser.token) ->
        Lexing.lexbuf -> Datalog.Ast.literal
      val parse_literals :
        (Lexing.lexbuf -> Datalog.Parser.token) ->
        Lexing.lexbuf -> Datalog.Ast.literal list
      val parse_clause :
        (Lexing.lexbuf -> Datalog.Parser.token) ->
        Lexing.lexbuf -> Datalog.Ast.clause
      val parse_file :
        (Lexing.lexbuf -> Datalog.Parser.token) ->
        Lexing.lexbuf -> Datalog.Ast.file
      val parse_query :
        (Lexing.lexbuf -> Datalog.Parser.token) ->
        Lexing.lexbuf -> Datalog.Ast.query
    end
  module Lexer :
    sig
      val token : Lexing.lexbuf -> Datalog.Parser.token
      val print_location : Lexing.lexbuf -> string
    end
  module StringSymbol :
    sig
      type t = string
      val equal : t -> t -> bool
      val hash : t -> int
      val to_string : t -> string
    end
  module Default :
    sig
      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
      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 : ('-> 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 -> Datalog.Default.vartbl
      val literal_of_ast :
        ?tbl:Datalog.Default.vartbl -> Datalog.Ast.literal -> literal
      val clause_of_ast : Datalog.Ast.clause -> clause
      val query_of_ast :
        Datalog.Ast.query -> int array * literal list * literal list
    end
  val version : string
end