sig
  type category = Lang.lfun Qed.Logic.category
  type kind = Z | R | I of Ctypes.c_int | F of Ctypes.c_float | A
  val add_builtin : string -> LogicBuiltins.kind list -> Lang.lfun -> unit
  type driver
  val driver : LogicBuiltins.driver Context.value
  val create :
    id:string ->
    ?descr:string -> ?includes:string list -> unit -> LogicBuiltins.driver
  val init :
    id:string -> ?descr:string -> ?includes:string list -> unit -> unit
  val id : LogicBuiltins.driver -> string
  val descr : LogicBuiltins.driver -> string
  val is_default : LogicBuiltins.driver -> bool
  val compare : LogicBuiltins.driver -> LogicBuiltins.driver -> int
  val find_lib : string -> string
  val dependencies : string -> string list
  val add_library : string -> string list -> unit
  val add_alias :
    string -> LogicBuiltins.kind list -> alias:string -> unit -> unit
  val add_type :
    string -> library:string -> ?link:string Lang.infoprover -> unit -> unit
  val add_ctor :
    string ->
    LogicBuiltins.kind list ->
    library:string -> link:Qed.Engine.link Lang.infoprover -> unit -> unit
  val add_logic :
    LogicBuiltins.kind ->
    string ->
    LogicBuiltins.kind list ->
    library:string ->
    ?category:LogicBuiltins.category ->
    link:Qed.Engine.link Lang.infoprover -> unit -> unit
  val add_predicate :
    string ->
    LogicBuiltins.kind list ->
    library:string -> link:string Lang.infoprover -> unit -> unit
  val add_option :
    driver_dir:string -> string -> string -> library:string -> string -> unit
  val set_option :
    driver_dir:string -> string -> string -> library:string -> string -> unit
  type doption
  val create_option :
    (driver_dir:string -> string -> string) ->
    string -> string -> LogicBuiltins.doption
  val get_option : LogicBuiltins.doption -> library:string -> string list
  type builtin = ACSLDEF | LFUN of Lang.lfun
  val logic : Cil_types.logic_info -> LogicBuiltins.builtin
  val ctor : Cil_types.logic_ctor_info -> LogicBuiltins.builtin
  val constant : string -> LogicBuiltins.builtin
  val dump : unit -> unit
end