class
Z3::BitvecExpr
- Z3::BitvecExpr
- Reference
- Object
Defined in:
z3/bitvec_expr.crConstructors
Instance Method Summary
-
#!=(other)
Returns
trueif this object is not equal to other. - #%(other)
- #&(other)
- #*(other)
- #+(other)
- #-(other)
- #-
- #/(other)
- #<(other)
- #<<(other)
- #<=(other)
-
#==(other)
Returns
false(other can only be aValuehere). - #>(other)
- #>=(other)
- #>>(other)
- #^(other)
- #|(other)
- #~
-
#abs
Inherently signed
- #add_no_overflow?(other)
- #add_no_underflow?(other)
- #all_bits_set?
- #any_bits_set?
-
#bit(index : Int)
A single bit, as a Bool.
- #concat(other : BitvecExpr)
- #const?
- #div_no_overflow?(other)
- #extract(hi : Int, lo : Int)
- #inspect(io)
- #lshift(other)
- #mul_no_overflow?(other)
- #mul_no_underflow?(other)
- #nand(other)
- #neg_no_overflow?
-
#negative?
Inherently signed
- #nonzero?
- #nor(other)
-
#positive?
Inherently signed
-
#redand
Z3 answers these with a one-bit Bitvec rather than a Bool, which is what #all_bits_set? and #any_bits_set? are for
- #redor
- #repeat(n : Int)
-
#rotate_left(n : Int)
An Int rotates by a fixed amount, a Bitvec of the same size by whatever it turns out to be - Z3 has a separate operation for each, and the fixed one gives the solver much more to work with, so a literal never goes through the other
- #rotate_left(n : BitvecExpr)
- #rotate_right(n : Int)
- #rotate_right(n : BitvecExpr)
- #rshift(other)
-
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #sign_ext(n : Int)
- #signed_add_no_overflow?(other)
- #signed_add_no_underflow?(other)
- #signed_div(other)
- #signed_div_no_overflow?(other)
- #signed_ge(other)
- #signed_gt(other)
- #signed_le(other)
- #signed_lshift(other)
- #signed_lt(other)
- #signed_mod(other)
- #signed_mul_no_overflow?(other)
- #signed_mul_no_underflow?(other)
- #signed_neg_no_overflow?
- #signed_rem(other)
- #signed_rshift(other)
- #signed_sub_no_overflow?(other)
- #signed_sub_no_underflow?(other)
- #signed_to_i
- #signed_value : BigInt
- #simplify
- #size
- #sort : Z3::BitvecSort
-
#sub_no_overflow?(other)
Subtraction is addition's mirror image: only signed can overflow, and both signs can underflow - so which of these takes a sign is the other way round
- #sub_no_underflow?(other)
-
#to_i
#to_i and friends build a Z3 Int expression out of this one.
- #to_s(io)
- #to_unsafe : LibZ3::Ast
- #unsigned_add_no_overflow?(other)
- #unsigned_add_no_underflow?(other)
- #unsigned_div(other)
- #unsigned_div_no_overflow?(other)
- #unsigned_ge(other)
- #unsigned_gt(other)
- #unsigned_le(other)
- #unsigned_lshift(other)
- #unsigned_lt(other)
- #unsigned_mul_no_overflow?(other)
- #unsigned_mul_no_underflow?(other)
- #unsigned_neg_no_overflow?
- #unsigned_rem(other)
- #unsigned_rshift(other)
- #unsigned_sub_no_overflow?(other)
- #unsigned_sub_no_underflow?(other)
- #unsigned_to_i
-
#unsigned_value : BigInt
Z3 prints a Bitvec numeral as its unsigned value, so this is the one it gives us
- #value
- #xnor(other)
- #zero?
- #zero_ext(n : Int)
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).
A single bit, as a Bool. Deliberately not #[] - that would read like #extract with a one-bit range, which gives a Bitvec(1) instead
Z3 answers these with a one-bit Bitvec rather than a Bool, which is what #all_bits_set? and #any_bits_set? are for
An Int rotates by a fixed amount, a Bitvec of the same size by whatever it turns out to be - Z3 has a separate operation for each, and the fixed one gives the solver much more to work with, so a literal never goes through the other
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.
Subtraction is addition's mirror image: only signed can overflow, and both signs can underflow - so which of these takes a sign is the other way round
#to_i and friends build a Z3 Int expression out of this one. #value and friends leave Z3 and give back a Crystal Integer, which only works on a literal. Both come in pairs because a Bitvec carries no sign of its own - the same eight bits are 200 read one way and -56 read the other.
Z3 prints a Bitvec numeral as its unsigned value, so this is the one it gives us