Z3Algebraic

public class Z3Algebraic : AnyZ3Ast

An algebraic number that can be used in the Z3 real algebraic number package.

  • Returns true if self is positive, false otherwise.

    Declaration

    Swift

    public var isPositive: Bool { get }

  • Returns true if self is negative, false otherwise.

    Declaration

    Swift

    public var isNegative: Bool { get }

  • Returns true if self is zero, false otherwise.

    Declaration

    Swift

    public var isZero: Bool { get }

  • Returns 1 if self is positive, 0 if self 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 polynomial self(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 of self(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 if lhs < rhs, false otherwise.

    Declaration

    Swift

    static func < (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool

  • Return true if lhs <= rhs, false otherwise.

    Declaration

    Swift

    static func <= (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool

  • Return true if lhs > rhs, false otherwise.

    Declaration

    Swift

    static func > (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool

  • Return true if lhs >= rhs, false otherwise.

    Declaration

    Swift

    static func >= (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool

  • Return true if lhs == rhs, false otherwise.

    Declaration

    Swift

    static func == (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool

  • Return true if lhs != rhs, false otherwise.

    Declaration

    Swift

    static func != (lhs: Z3Algebraic, rhs: Z3Algebraic) -> Bool