Z3::BitvecExpr
Inherits Reference < Object
Constructors
Instance methods
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.
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