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