class
Z3::RealExpr
- Z3::RealExpr
- Reference
- Object
Defined in:
z3/real_expr.crConstructors
Instance Method Summary
-
#!=(other)
Returns
trueif this object is not equal to other. - #*(other)
- #**(other)
- #+(other)
- #-(other)
- #-
- #/(other)
- #<(other)
- #<=(other)
-
#==(other)
Returns
false(other can only be aValuehere). - #>(other)
- #>=(other)
- #abs
-
#algebraic?
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 - #const?
-
#floor
SMT-LIB's
#to_introunds towards negative infinity, so this is Crystal's Float#floor. - #inspect(io)
-
#integer?
A Z3 Bool, like #zero? and the other predicates, not a Crystal one
-
#lower_bound(precision = 20) : BigRational
Rationals bracketing the value, as tightly as
precisionasks for. - #negative?
- #nonzero?
- #positive?
-
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #simplify
- #sort
-
#to_f : Float64
Always available, because a Float is allowed to be approximate
- #to_int
-
#to_r : BigRational
There's no #value here, unlike every other sort which can hand back a Crystal object.
- #to_s(io)
- #to_unsafe : LibZ3::Ast
- #upper_bound(precision = 20) : BigRational
- #zero?
Constructor Detail
Instance Method Detail
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.
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.
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.