Module Cfloat

module Cfloat: sig .. end
Floatting Arithmetic Model

val library : string
val result : ('a, 'b) Qed.Logic.datatype
val params : Qed.Logic.sort list
val link : string -> Qed.Engine.link Lang.infoprover
val make_fun_float : string -> Ctypes.c_float -> Lang.lfun
val make_pred_float : string -> Ctypes.c_float -> Lang.lfun
val f_of_int : Lang.lfun
val f_sqrt : Lang.lfun
val f_iabs : Lang.lfun
val f_rabs : Lang.lfun
val f_model : Lang.lfun
val f_delta : Lang.lfun
val f_epsilon : Lang.lfun
type model = 
| Real
| Float
val model : model Context.value
val configure : model -> unit
val code_lit : float -> Lang.F.term
val suffixed : string -> bool
val acsl_lit : Cil_types.logic_real -> Lang.F.term
val round_lit : Ctypes.c_float -> string -> Lang.F.term
val is_lt0 : Lang.F.term -> Lang.F.term -> bool
val is_le0 : Lang.F.term -> Lang.F.term -> bool
val is_eq0 : Lang.F.term -> Lang.F.term -> bool
val builtin_positive_eq : Lang.F.Fun.t -> Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term
val builtin_positive_leq : Lang.F.Fun.t -> Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.term
val is_model : Lang.F.term -> Lang.F.term -> bool
val is_delta : Lang.F.term -> Lang.F.term -> bool
val builtin_abs : Lang.F.Fun.t -> Lang.F.term -> Lang.F.term list -> Lang.F.term
val builtin_sqrt : Lang.F.term list -> Lang.F.term
val flt_rnd : Ctypes.c_float -> Lang.lfun
val flt_add : Ctypes.c_float -> Lang.lfun
val flt_mul : Ctypes.c_float -> Lang.lfun
val flt_div : Ctypes.c_float -> Lang.lfun
val flt_sqrt : Ctypes.c_float -> Lang.lfun
module OP: FCMap.Make(Lang.Fun)
val models : (Lang.F.term list -> Lang.F.term) OP.t Pervasives.ref
val add_model : OP.key -> (Lang.F.term list -> Lang.F.term) -> unit
val add_fmodel : (Ctypes.c_float -> OP.key) ->
(Lang.F.term list -> Lang.F.term) -> unit
val builtin_model : Lang.F.term list -> Lang.F.term
val builtin_round : Ctypes.c_float -> Lang.F.term list -> Lang.F.term
val builtin_error : Lang.F.term list -> Lang.F.term
val fconvert : Ctypes.c_float -> Lang.F.term -> Lang.F.term
val real_of_int : Lang.F.term -> Lang.F.term
val float_of_int : Ctypes.c_float -> Lang.F.term -> Lang.F.term
val frange : Ctypes.c_float -> Lang.F.term -> Lang.F.pred
val runop : (Lang.F.term -> Lang.F.term) -> Lang.F.Fun.t -> Lang.F.term -> Lang.F.term
val rbinop : (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
Lang.F.Fun.t -> Lang.F.term -> Lang.F.term -> Lang.F.term
val funop : ('a -> Lang.F.term) -> Ctypes.c_float -> 'a -> Lang.F.term
val fbinop : (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
('a -> Lang.F.Fun.t) -> 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term
val fadd : Ctypes.c_float -> Lang.F.term -> Lang.F.term -> Lang.F.term
val fmul : Ctypes.c_float -> Lang.F.term -> Lang.F.term -> Lang.F.term
val fdiv : Ctypes.c_float -> Lang.F.term -> Lang.F.term -> Lang.F.term
val fopp : 'a -> Lang.F.term -> Lang.F.term
val fsub : Ctypes.c_float -> Lang.F.term -> Lang.F.term -> Lang.F.term
val compute_f_of_int : Lang.F.term list -> Lang.F.term