class

Z3::RoundingModeExpr

Inherits Reference < Object

One of the five rounding modes, or a variable which the solver resolves to one of them. RoundingModeSort is where the five come from.

Constructors

new(expr : LibZ3::Ast)

Source

Instance methods

!=(other)

Returns true if this object is not equal to other.

By default this method is implemented as !(self == other) so there's no need to override this unless there's a more efficient way to do it.

Source

==(other)

Returns false (other can only be a Value here).

Source

inspect(io)

Source

same_term?(other : AnyExpr)

Whether this is the same term as other. Z3 hash-conses its expressions, so this is structural equality - Z3.int("a") + 1 built twice is one term. It is a named method rather than == because == builds a Z3 expression instead of answering a Crystal Bool - see the Limitations section of the README.

simplify

sort

to_s(io)

to_unsafe