Z3FloatingPoint

public extension Z3FloatingPoint

public extension Z3FloatingPoint where T: FloatingSort, T: BinaryFloatingPoint, T: LosslessStringConvertible

getSort(_:)
Gets the statically-typed Z3Sort associated with T from this Z3FloatingPoint<T>.
Declaration
Swift

static func getSort(_ context: Z3Context) -> Z3Sort
squareRoot
Floating-point square root.
Declaration
Swift

var squareRoot: Z3Ast { get }
isNormal
Predicate indicating whether t is a normal floating-point number.
Declaration
Swift

var isNormal: Z3Bool { get }
isSubnormal
Predicate indicating whether t is a subnormal floating-point number.
Declaration
Swift

var isSubnormal: Z3Bool { get }
isNan
Predicate indicating whether t is a NaN.
Declaration
Swift

var isNan: Z3Bool { get }
isZero
Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
Declaration
Swift

var isZero: Z3Bool { get }
isInfinite
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Declaration
Swift

var isInfinite: Z3Bool { get }
isPositive
Predicate indicating whether t is a positive floating-point number.
Declaration
Swift

var isPositive: Z3Bool { get }
isNegative
Predicate indicating whether t is a negative floating-point number.
Declaration
Swift

var isNegative: Z3Bool { get }
isNumeralNormal
Checks whether this floating-point numeral is a NaN.
Declaration
Swift

var isNumeralNormal: Bool { get }
isNumeralSubnormal
Checks whether this floating-point numeral is a +oo or -oo.
Declaration
Swift

var isNumeralSubnormal: Bool { get }
isNumeralNan
Checks whether this floating-point numeral is +zero or -zero.
Declaration
Swift

var isNumeralNan: Bool { get }
isNumeralZero
Checks whether this floating-point numeral is normal.
Declaration
Swift

var isNumeralZero: Bool { get }
isNumeralInfinite
Checks whether this floating-point numeral is subnormal.
Declaration
Swift

var isNumeralInfinite: Bool { get }
isNumeralPositive
Checks whether this floating-point numeral is positive.
Declaration
Swift

var isNumeralPositive: Bool { get }
isNumeralNegative
Checks whether this floating-point numeral is negative.
Declaration
Swift

var isNumeralNegative: Bool { get }
convertTo(roundingMode:sort:)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Produces a term that represents the conversion of this floating-point term to a floating-point term of sort sort. If necessary, the result will be rounded according to rounding mode roundingMode.
Declaration
Swift

func convertTo<U>(roundingMode: Z3Ast<RoundingModeSort>, sort: U.Type) -> Z3FloatingPoint<U> where U : FloatingSort
convertToAny(roundingMode:sort:)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Produces a term that represents the conversion of this floating-point term to a floating-point term of sort sort. If necessary, the result will be rounded according to rounding mode roundingMode.

Type-erased version.
Declaration
Swift

func convertToAny(roundingMode: Z3Ast<RoundingModeSort>, sort: Z3Sort) -> AnyZ3Ast
convertToReal()
Conversion of a floating-point term into a real-numbered term.

Produces a term that represents the conversion of this floating-point term into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.
Declaration
Swift

func convertToReal() -> Z3Real
convertToBitVector(roundingMode:sort:signed:)
Produces a term that represents the conversion of this floating-point term into a bit-vector term of bitWidth T.bitWidth in 2’s complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode roundingMode.
Declaration
Swift

func convertToBitVector<BV>(roundingMode: Z3Ast<RoundingModeSort>, sort: BV.Type = BV.self, signed: Bool) -> Z3BitVector<BV> where BV : BitVectorSort
convertToBitVectorAny(roundingMode:_:signed:)
Produces a term that represents the conversion of this floating-point term into a bit-vector term of bitWidth T.bitWidth into a bit-vector term of size sz in 2’s complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm.
Declaration
Swift

func convertToBitVectorAny(roundingMode: Z3Ast<RoundingModeSort>, _ sz: UInt32, signed: Bool) -> AnyZ3Ast


                    
                    
                    -(_:)

Declaration

Swift

prefix static func - (rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    >=(_:_:)

Declaration

Swift

static func >= (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    >(_:_:)

Declaration

Swift

static func > (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    <=(_:_:)

Declaration

Swift

static func <= (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    <(_:_:)

Declaration

Swift

static func < (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    +(_:_:)

Declaration

Swift

static func + (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    -(_:_:)

Declaration

Swift

static func - (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    *(_:_:)

Declaration

Swift

static func * (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    /(_:_:)

Declaration

Swift

static func / (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    %(_:_:)

Declaration

Swift

static func % (lhs: Z3FloatingPoint, rhs: Z3FloatingPoint) -> Z3FloatingPoint

Constants Casting


                    
                    
                    ==(_:_:)

Declaration

Swift

static func == (lhs: T, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    ==(_:_:)

Declaration

Swift

static func == (lhs: Z3FloatingPoint, rhs: T) -> Z3Bool


                    
                    
                    !=(_:_:)

Declaration

Swift

static func != (lhs: T, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    !=(_:_:)

Declaration

Swift

static func != (lhs: Z3FloatingPoint, rhs: T) -> Z3Bool


                    
                    
                    >=(_:_:)

Declaration

Swift

static func >= (lhs: T, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    >=(_:_:)

Declaration

Swift

static func >= (lhs: Z3FloatingPoint, rhs: T) -> Z3Bool


                    
                    
                    >(_:_:)

Declaration

Swift

static func > (lhs: T, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    >(_:_:)

Declaration

Swift

static func > (lhs: Z3FloatingPoint, rhs: T) -> Z3Bool


                    
                    
                    <=(_:_:)

Declaration

Swift

static func <= (lhs: T, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    <=(_:_:)

Declaration

Swift

static func <= (lhs: Z3FloatingPoint, rhs: T) -> Z3Bool


                    
                    
                    <(_:_:)

Declaration

Swift

static func < (lhs: T, rhs: Z3FloatingPoint) -> Z3Bool


                    
                    
                    <(_:_:)

Declaration

Swift

static func < (lhs: Z3FloatingPoint, rhs: T) -> Z3Bool


                    
                    
                    +(_:_:)

Declaration

Swift

static func + (lhs: T, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    +(_:_:)

Declaration

Swift

static func + (lhs: Z3FloatingPoint, rhs: T) -> Z3FloatingPoint


                    
                    
                    -(_:_:)

Declaration

Swift

static func - (lhs: T, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    -(_:_:)

Declaration

Swift

static func - (lhs: Z3FloatingPoint, rhs: T) -> Z3FloatingPoint


                    
                    
                    *(_:_:)

Declaration

Swift

static func * (lhs: T, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    *(_:_:)

Declaration

Swift

static func * (lhs: Z3FloatingPoint, rhs: T) -> Z3FloatingPoint


                    
                    
                    /(_:_:)

Declaration

Swift

static func / (lhs: T, rhs: Z3FloatingPoint) -> Z3FloatingPoint


                    
                    
                    /(_:_:)

Declaration

Swift

static func / (lhs: Z3Ast, rhs: T) -> Z3Ast


                    
                    
                    %(_:_:)

Declaration

Swift

static func % (lhs: Z3FloatingPoint, rhs: T) -> Z3FloatingPoint


                    
                    
                    %(_:_:)

Declaration

Swift

static func % (lhs: T, rhs: Z3FloatingPoint) -> Z3FloatingPoint