Z3::RealExpr

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.

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

Z3 answers an irrational root with an algebraic number rather than giving up, and those are apps rather than numerals, so #const? won't spot them

SMT-LIB's to_int rounds towards negative infinity, so this is Crystal's Float#floor. Deliberately not #to_i, which truncates towards zero instead - (-2.5).to_i is -2 in Crystal, but this is -3.

A Z3 Bool, like #zero? and the other predicates, not a Crystal one

Rationals bracketing the value, as tightly as precision asks for. An exact value is its own bound.

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.

Always available, because a Float is allowed to be approximate

There's no #value here, unlike every other sort which can hand back a Crystal object. Z3's Reals include the algebraic numbers, and √2 has no exact Crystal equivalent at all - so instead there's #to_r, which is exact and refuses when it can't be, and #to_f, which is an approximation and says so by being a Float64.