Module Dolmen_model.Fp

Value definition

************************************************************************

val ops : Farith.F.t Value.ops

ops for bitvector values.

val mk : Farith.F.t -> Value.t

mk f floating point value creation.

Corner cases & builtins

************************************************************************

val builtins : Env.t -> Dolmen.Std.Expr.Term.Const.t -> Value.t option

builtins for floating-points