Module Z3.FloatingPoint.RoundingMode

module RoundingMode: sig .. end

Rounding Modes

val mk_sort : context -> Sort.sort

Create the RoundingMode sort.

val is_fprm : Expr.expr -> bool

Indicates whether the terms is of floating-point rounding mode sort.

val mk_round_nearest_ties_to_even : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

val mk_rne : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

val mk_round_nearest_ties_to_away : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

val mk_rna : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

val mk_round_toward_positive : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

val mk_rtp : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

val mk_round_toward_negative : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

val mk_rtn : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

val mk_round_toward_zero : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

val mk_rtz : context -> Expr.expr

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.