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