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