class Z3::RoundingModeSort

• Z3::RoundingModeSort
• Reference
• Object

Overview

The way an operation rounds, as a Z3 value - IEEE says every arithmetic operation names one, so every FloatExpr method which rounds takes one.

The sort has exactly five elements, and they're the class methods below. It's also an ordinary sort, so RoundingModeSort.var("m") hands the choice to the solver, and a model answers with one of the five.

Defined in:

z3/rounding_mode_sort.cr

Class Method Summary

• .[](expr : RoundingModeExpr)
• .cast(value) : RoundingModeExpr

  A rounding mode has no Crystal counterpart to be cast from - the five above are the only values there are

• .from_ast(ast : LibZ3::Ast) : RoundingModeExpr
• .nearest_ties_away
• .nearest_ties_even

  Ties are the values exactly between two floats, which is the only case the first two disagree on - 2.5 rounds to 2.0 one way and 3.0 the other

• .to_s(io)
• .to_unsafe
• .towards_negative
• .towards_positive
• .towards_zero
• .var(name : String)

Class Method Detail