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