class
Z3::IntExpr
- Z3::IntExpr
- Reference
- Object
Defined in:
z3/int_expr.crConstructors
Instance Method Summary
-
#!=(other)
Returns
trueif this object is not equal to other. -
#%(other)
It doesn't match Crystal on a negative right side, but nobody does modulo a negative anyway, and the Python Z3 API does the same thing
- #*(other)
- #**(other)
- #+(other)
- #-(other)
- #-
- #/(other)
- #<(other)
- #<=(other)
-
#==(other)
Returns
false(other can only be aValuehere). - #>(other)
- #>=(other)
- #abs
- #const?
-
#divisible_by?(other)
Z3 spells this the other way round, as "other divides self"
- #inspect(io)
- #mod(other)
- #negative?
- #nonzero?
- #positive?
- #rem(other)
-
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #simplify
- #sort
- #to_big_i : BigInt
- #to_bitvec(n : Int)
-
#to_bv(n : Int)
Takes the low
nbits, so it wraps rather than failing on values which don't fit -Z3.int("a").to_bv(8)of 256 is 0. - #to_i : Int32
- #to_i64 : Int64
- #to_real
- #to_s(io)
- #to_unsafe : LibZ3::Ast
-
#value : BigInt
Every sort which can hand back a Crystal object spells it #value.
- #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.
It doesn't match Crystal on a negative right side, but nobody does modulo a negative anyway, and the Python Z3 API does the same thing
Returns false (other can only be a Value here).
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.
Takes the low n bits, so it wraps rather than failing on values which don't
fit - Z3.int("a").to_bv(8) of 256 is 0. Which Integer comes back out depends
on how you read it again: BitvecExpr#signed_value or #unsigned_value.
Every sort which can hand back a Crystal object spells it #value. Z3 Ints are unbounded, so this is a BigInt - #to_i is the Int32 one, as everywhere else in Crystal.