Module Z3.FloatingPoint

module RoundingMode : sig ... end
val mk_sort : context -> int -> int -> Sort.sort
val mk_sort_half : context -> Sort.sort
val mk_sort_16 : context -> Sort.sort
val mk_sort_single : context -> Sort.sort
val mk_sort_32 : context -> Sort.sort
val mk_sort_double : context -> Sort.sort
val mk_sort_64 : context -> Sort.sort
val mk_sort_quadruple : context -> Sort.sort
val mk_sort_128 : context -> Sort.sort
val mk_nan : context -> Sort.sort -> Expr.expr
val mk_inf : context -> Sort.sort -> bool -> Expr.expr
val mk_zero : context -> Sort.sort -> bool -> Expr.expr
val mk_numeral_f : context -> float -> Sort.sort -> Expr.expr
val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr
val mk_numeral_i_u : context -> bool -> int64 -> int64 -> Sort.sort -> Expr.expr
val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr
val is_fp : Expr.expr -> bool
val is_abs : Expr.expr -> bool
val is_neg : Expr.expr -> bool
val is_add : Expr.expr -> bool
val is_sub : Expr.expr -> bool
val is_mul : Expr.expr -> bool
val is_div : Expr.expr -> bool
val is_fma : Expr.expr -> bool
val is_sqrt : Expr.expr -> bool
val is_rem : Expr.expr -> bool
val is_round_to_integral : Expr.expr -> bool
val is_min : Expr.expr -> bool
val is_max : Expr.expr -> bool
val is_leq : Expr.expr -> bool
val is_lt : Expr.expr -> bool
val is_geq : Expr.expr -> bool
val is_gt : Expr.expr -> bool
val is_eq : Expr.expr -> bool
val is_is_normal : Expr.expr -> bool
val is_is_subnormal : Expr.expr -> bool
val is_is_zero : Expr.expr -> bool
val is_is_infinite : Expr.expr -> bool
val is_is_nan : Expr.expr -> bool
val is_is_negative : Expr.expr -> bool
val is_is_positive : Expr.expr -> bool
val is_to_fp : Expr.expr -> bool
val is_to_fp_unsigned : Expr.expr -> bool
val is_to_ubv : Expr.expr -> bool
val is_to_sbv : Expr.expr -> bool
val is_to_real : Expr.expr -> bool
val is_to_ieee_bv : Expr.expr -> bool
val mk_const : context -> Symbol.symbol -> Sort.sort -> Expr.expr
val mk_const_s : context -> string -> Sort.sort -> Expr.expr
val mk_abs : context -> Expr.expr -> Expr.expr
val mk_neg : context -> Expr.expr -> Expr.expr
val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_min : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_is_normal : context -> Expr.expr -> Expr.expr
val mk_is_subnormal : context -> Expr.expr -> Expr.expr
val mk_is_zero : context -> Expr.expr -> Expr.expr
val mk_is_infinite : context -> Expr.expr -> Expr.expr
val mk_is_nan : context -> Expr.expr -> Expr.expr
val mk_is_negative : context -> Expr.expr -> Expr.expr
val mk_is_positive : context -> Expr.expr -> Expr.expr
val mk_to_fp_bv : context -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_float : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_real : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_signed : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
val mk_to_real : context -> Expr.expr -> Expr.expr
val get_ebits : context -> Sort.sort -> int
val get_sbits : context -> Sort.sort -> int
val get_numeral_sign : context -> Expr.expr -> bool * int
val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr
val get_numeral_exponent_string : context -> Expr.expr -> bool -> string
val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int64
val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr
val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr
val get_numeral_significand_string : context -> Expr.expr -> string
val get_numeral_significand_uint : context -> Expr.expr -> bool * int64
val is_numeral_nan : context -> Expr.expr -> bool
val is_numeral_inf : context -> Expr.expr -> bool
val is_numeral_zero : context -> Expr.expr -> bool
val is_numeral_normal : context -> Expr.expr -> bool
val is_numeral_subnormal : context -> Expr.expr -> bool
val is_numeral_positive : context -> Expr.expr -> bool
val is_numeral_negative : context -> Expr.expr -> bool
val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr
val mk_to_fp_int_real : context -> Expr.expr -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
val numeral_to_string : Expr.expr -> string