AnyZ3Ast

public class AnyZ3Ast : Z3AstBase

The abstract syntax tree (AST) class for Expression syntaxes.

  • Return the sort of this AST node.

    The AST node must be a constant, application, numeral, bound variable, or quantifier.

    Declaration

    Swift

    public var sort: Z3Sort? { get }

  • Return true if this expression is well sorted.

    Declaration

    Swift

    public var isWellSorted: Bool { get }

  • Returns true if this AST is true, false if this AST is false, and nil otherwise

    Declaration

    Swift

    public var boolValue: Bool? { get }

  • Return numeral value, as a string of a numeric constant term

    Precondition

    self.astKind == Z3AstKind.numeralAst

    Declaration

    Swift

    public var numeralString: String { get }

  • Return numeral as a double.

    Precondition

    self.astKind == Z3AstKind.numeralAst

    Declaration

    Swift

    public var numeralDouble: Double { get }

  • Return numeral as an integer.

    Return 0 if numeral does not fit in an Int32.

    Precondition

    self.astKind == Z3AstKind.numeralAst

    Declaration

    Swift

    public var numeralInt: Int32 { get }

  • Return the numerator (as a numeral AST) of a numeral AST of sort Real.

    Precondition

    self.astKind == Z3AstKind.numeralAst

    Declaration

    Swift

    public var numerator: AnyZ3Ast? { get }

  • Return the denominator (as a numeral AST) of a numeral AST of sort Real.

    Precondition

    self.astKind == Z3AstKind.numeralAst

    Declaration

    Swift

    public var denominator: AnyZ3Ast? { get }

  • Compares this term to another term.

    Declaration

    Swift

    public func isEqual(to other: AnyZ3Ast) -> Bool

  • Return numeral as a string in decimal notation.

    The result has at most precision decimal places.

    Precondition

    self.astKind == Z3AstKind.numeralAst || self.isAlgebraicNumber

    Declaration

    Swift

    public func getNumeralDecimalString(precision: UInt32) -> String

  • Return numeral value, as a pair of 64 bit numbers if the representation fits.

    Return nil if the numeral value does not fit in 64-bit numerals.

    Precondition

    self.astKind == Z3AstKind.numeralAst

    Declaration

    Swift

    public func getNumeralSmall() -> (num: Int64, den: Int64)?

  • Translate/Copy the AST self from its current context to context target

    Declaration

    Swift

    public override func translate(to newContext: Z3Context) -> AnyZ3Ast

  • An unsafe cast from a generic AnyZ3Ast or a specialized Z3Ast to another specialized Z3Ast type

    Declaration

    Swift

    func unsafeCastTo<T>(sort: T.Type = T.self) -> Z3Ast<T> where T : SortKind

  • A runtime type-checked cast from a generic AnyZ3Ast or a specialized Z3Ast to another specialized Z3Ast type.

    The underlying SortKind of this AST type is checked, and if it matches the incoming sort, the result is a non-nil Z3Ast instance annotated with the requested type.

    Declaration

    Swift

    func castTo<T>(sort: T.Type = T.self) -> Z3Ast<T>? where T : SortKind

  • An unsafe cast from a generic AnyZ3Ast to a Z3Algebraic type.

    Declaration

    Swift

    func unsafeCastToAlgebraic() -> Z3Algebraic

  • A runtime type-checked cast from a generic AnyZ3Ast to a Z3Algebraic type.

    The underlying value is checked against Z3Context.algebraicIsValue(_:), and if it succeeds, the return is a Z3Algebraic instance.

    Declaration

    Swift

    func castToAlgebraic() -> Z3Algebraic?

  • An unsafe cast from a generic AnyZ3Ast or a specialized Z3Ast to another specialized Z3RegularExp type.

    Declaration

    Swift

    func unsafeCastToRegularExp<Element>(elementSort: Element.Type = Element.self) -> Z3RegularExp<Element> where Element : SortKind

  • A runtime type-checked cast from a generic AnyZ3Ast or a specialized Z3RegularExp to another specialized Z3RegularExp type.

    The underlying SortKind of this AST type is checked, and if it matches the incoming sort, the result is a non-nil Z3RegularExp instance annotated with the requested type.

    Declaration

    Swift

    func castToRegularExp<Element>(elementSort: Element.Type = Element.self) -> Z3RegularExp<Element>? where Element : SortKind

  • An unsafe cast from a generic AnyZ3Ast or a specialized Z3Ast to another specialized Z3Seq type.

    Declaration

    Swift

    func unsafeCastToSequence<Element>(elementSort: Element.Type = Element.self) -> Z3Seq<Element> where Element : SortKind

  • A runtime type-checked cast from a generic AnyZ3Ast or a specialized Z3Seq to another specialized Z3Seq type.

    The underlying SortKind of this AST type is checked, and if it matches the incoming sort, the result is a non-nil Z3Seq instance annotated with the requested type.

    Declaration

    Swift

    func castToSequence<Element>(elementSort: Element.Type = Element.self) -> Z3Seq<Element>? where Element : SortKind