sig
  type t
  type interpreter = TopDown.S.T.t -> TopDown.S.C.t list
  val create : ?parent:TopDown.S.DB.t -> unit -> TopDown.S.DB.t
  val copy : TopDown.S.DB.t -> TopDown.S.DB.t
  val clear : TopDown.S.DB.t -> unit
  val add_fact : TopDown.S.DB.t -> TopDown.S.T.t -> unit
  val add_facts : TopDown.S.DB.t -> TopDown.S.T.t list -> unit
  val add_clause : TopDown.S.DB.t -> TopDown.S.C.t -> unit
  val add_clauses : TopDown.S.DB.t -> TopDown.S.C.t list -> unit
  val interpret :
    ?help:string ->
    TopDown.S.DB.t -> TopDown.S.const -> TopDown.S.DB.interpreter -> unit
  val interpret_list :
    TopDown.S.DB.t ->
    (TopDown.S.const * string * TopDown.S.DB.interpreter) list -> unit
  val is_interpreted : TopDown.S.DB.t -> TopDown.S.const -> bool
  val add_builtin :
    TopDown.S.DB.t -> Const.t -> TopDown.S.BuiltinFun.t -> unit
  val builtin_funs : TopDown.S.DB.t -> TopDown.S.BuiltinFun.map
  val eval : TopDown.S.DB.t -> TopDown.S.T.t -> TopDown.S.T.t
  val help : TopDown.S.DB.t -> string list
  val num_facts : TopDown.S.DB.t -> int
  val num_clauses : TopDown.S.DB.t -> int
  val size : TopDown.S.DB.t -> int
  val find_facts :
    ?oc:bool ->
    TopDown.S.DB.t ->
    TopDown.S.scope ->
    TopDown.S.T.t ->
    TopDown.S.scope -> (TopDown.S.T.t -> TopDown.S.Subst.t -> unit) -> unit
  val find_clauses_head :
    ?oc:bool ->
    TopDown.S.DB.t ->
    TopDown.S.scope ->
    TopDown.S.T.t ->
    TopDown.S.scope -> (TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
  val find_interpretation :
    ?oc:bool ->
    TopDown.S.DB.t ->
    TopDown.S.scope ->
    TopDown.S.T.t ->
    TopDown.S.scope -> (TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
end