Z3BitVector

Gets the statically-typed Z3Sort associated with T from this Z3BitVector<T>.

Create an integer from this bit-vector.

If isSigned is false, then this bit-vector is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in this bit-vector. If isSigned is true, this bit-vector is treated as a signed bit-vector.

Two’s complement signed less than.

It abbreviates:

(or (and (= (extract[|m-1|:|m-1|] t1) bit1)
        (= (extract[|m-1|:|m-1|] t2) bit0))
    (and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2))
        (bvult t1 t2)))

Two’s complement signed less than or equal to.

Two’s complement signed greater than.

Two’s complement signed greater than or equal to.