Z3FloatingPoint
public extension Z3FloatingPoint
public extension Z3FloatingPoint where T: FloatingSort, T: BinaryFloatingPoint, T: LosslessStringConvertible
-
Gets the statically-typed Z3Sort associated with
T
from thisZ3FloatingPoint<T>
. -
Floating-point square root.
Declaration
Swift
var squareRoot: Z3Ast { get }
-
Predicate indicating whether
t
is a normal floating-point number.Declaration
Swift
var isNormal: Z3Bool { get }
-
Predicate indicating whether
t
is a subnormal floating-point number.Declaration
Swift
var isSubnormal: Z3Bool { get }
-
Predicate indicating whether
t
is a NaN.Declaration
Swift
var isNan: Z3Bool { get }
-
Predicate indicating whether
t
is a floating-point number with zero value, i.e., +zero or -zero.Declaration
Swift
var isZero: Z3Bool { get }
-
Predicate indicating whether
t
is a floating-point number representing +oo or -oo.Declaration
Swift
var isInfinite: Z3Bool { get }
-
Predicate indicating whether
t
is a positive floating-point number.Declaration
Swift
var isPositive: Z3Bool { get }
-
Predicate indicating whether
t
is a negative floating-point number.Declaration
Swift
var isNegative: Z3Bool { get }
-
Checks whether this floating-point numeral is a NaN.
Declaration
Swift
var isNumeralNormal: Bool { get }
-
Checks whether this floating-point numeral is a +oo or -oo.
Declaration
Swift
var isNumeralSubnormal: Bool { get }
-
Checks whether this floating-point numeral is +zero or -zero.
Declaration
Swift
var isNumeralNan: Bool { get }
-
Checks whether this floating-point numeral is normal.
Declaration
Swift
var isNumeralZero: Bool { get }
-
Checks whether this floating-point numeral is subnormal.
Declaration
Swift
var isNumeralInfinite: Bool { get }
-
Checks whether this floating-point numeral is positive.
Declaration
Swift
var isNumeralPositive: Bool { get }
-
Checks whether this floating-point numeral is negative.
Declaration
Swift
var isNumeralNegative: Bool { get }
-
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 moderoundingMode
.Declaration
Swift
func convertTo<U>(roundingMode: Z3Ast<RoundingModeSort>, sort: U.Type) -> Z3FloatingPoint<U> where U : FloatingSort
-
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 moderoundingMode
.Type-erased version.
Declaration
Swift
func convertToAny(roundingMode: Z3Ast<RoundingModeSort>, sort: Z3Sort) -> AnyZ3Ast
-
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
-
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 moderoundingMode
.Declaration
Swift
func convertToBitVector<BV>(roundingMode: Z3Ast<RoundingModeSort>, sort: BV.Type = BV.self, signed: Bool) -> Z3BitVector<BV> where BV : BitVectorSort
-
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 sizesz
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
-
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: Z3FloatingPoint, rhs: T) -> Z3FloatingPoint
-
Declaration
Swift
static func % (lhs: T, rhs: Z3FloatingPoint) -> Z3FloatingPoint