Z3BitVector
public extension Z3BitVector
-
Gets the statically-typed Z3Sort associated with
T
from thisZ3BitVector<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. IfisSigned
is true, this bit-vector is treated as a signed bit-vector.Declaration
Swift
func toInt(isSigned: Bool) -> Z3Int
-
Declaration
Swift
static func & (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
static func | (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
static func ^ (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
static func + (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
static func - (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
static func * (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
static func / (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3BitVector
-
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)))
Declaration
Swift
static func < (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3Bool
-
Two’s complement signed less than or equal to.
Declaration
Swift
static func <= (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3Bool
-
Two’s complement signed greater than.
Declaration
Swift
static func > (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3Bool
-
Two’s complement signed greater than or equal to.
Declaration
Swift
static func >= (lhs: Z3BitVector, rhs: Z3BitVector) -> Z3Bool
-
Declaration
Swift
prefix static func - (rhs: Z3BitVector) -> Z3BitVector
-
Declaration
Swift
prefix static func ! (rhs: Z3BitVector) -> Z3BitVector