class

Z3::RoundingModeSort

Inherits Reference < Object

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.

Class methods

[](expr : RoundingModeExpr)
Source
cast(value) : RoundingModeExpr

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

Source
from_ast(ast : LibZ3::Ast) : RoundingModeExpr
Source
nearest_ties_away
Source
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

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