Z3Ast

public class Z3Ast<T> : AnyZ3Ast where T : SortKind

An expression abstract syntax tree (AST) class that is typed with a sort to allow for compile-time static type checking of expressions.

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

    Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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

Available where T: ArithmeticSort

  • Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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

  • Declaration

    Swift

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