Z3Algebraic
public class Z3Algebraic : AnyZ3Ast
An algebraic number that can be used in the Z3 real algebraic number package.
-
Returns
true
ifself
is positive,false
otherwise.Declaration
Swift
public var isPositive: Bool { get }
-
Returns
true
ifself
is negative,false
otherwise.Declaration
Swift
public var isNegative: Bool { get }
-
Returns
true
ifself
is zero,false
otherwise.Declaration
Swift
public var isZero: Bool { get }
-
Returns
1
ifself
is positive,0
ifself
is zero, and-1
if it is negative.Declaration
Swift
public var sign: Int { get }
-
Return the
self^(1/k)
Declaration
Swift
public func root(_ k: UInt32) -> Z3Algebraic
-
Return the
self^k
Declaration
Swift
public func power(_ k: UInt32) -> Z3Algebraic
-
Given a multivariate polynomial
self(x_0, ..., x_{n-1}, x_n)
, returns the roots of the univariate polynomialself(a[0], ..., a[n-1], x_n)
.Precondition
self
is a Z3 expression that contains only arithmetic terms and free variables.Declaration
Swift
public func roots(_ a: [Z3Algebraic]) -> Z3AstVector
-
Given a multivariate polynomial
self(x_0, ..., x_{n-1})
, return the sign ofself(a[0], ..., a[n-1])
.Precondition
self
is a Z3 expression that contains only arithmetic terms and free variables.Declaration
Swift
public func eval(_ a: [Z3Algebraic]) -> Int
-
Return the coefficients of this polynomial.
Declaration
Swift
public func coefficients() -> Z3AstVector
-
Return which root of a polynomial the algebraic number represents.
Declaration
Swift
public func polynomialRootIndex() -> UInt32
-
Return the value a + b.
Declaration
Swift
static func + (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Z3Algebraic
-
Return the value a - b.
Declaration
Swift
static func - (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Z3Algebraic
-
Return the value a * b.
Declaration
Swift
static func * (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Z3Algebraic
-
Return the value a / b.
Declaration
Swift
static func / (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Z3Algebraic
-
Return
true
iflhs < rhs
,false
otherwise.Declaration
Swift
static func < (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs <= rhs
,false
otherwise.Declaration
Swift
static func <= (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs > rhs
,false
otherwise.Declaration
Swift
static func > (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs >= rhs
,false
otherwise.Declaration
Swift
static func >= (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs == rhs
,false
otherwise.Declaration
Swift
static func == (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs != rhs
,false
otherwise.Declaration
Swift
static func != (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool