Z3AstBase

public class Z3AstBase : Z3RefCountedObject

Abstract syntax tree node. That is, the data-structure used in Z3 to represent terms, formulas and types. Base class for Z3Sort, Z3FuncDecl, Z3Pattern, and AnyZ3Ast.

  • The context this Z3AstBase belongs

    Declaration

    Swift

    public let context: Z3Context
  • id

    Return a unique identifier for this AST.

    The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.

    Declaration

    Swift

    public var id: UInt32 { get }

  • Return a hash code for this AST.

    The hash code is structural. You can use AnyZ3Ast.id interchangeably with this function.

    Declaration

    Swift

    public var hash: UInt32 { get }

  • Return true if this AST is an application

    Declaration

    Swift

    public var isApp: Bool { get }

  • Declaration

    Swift

    public var isNumeralAst: Bool { get }

  • Return true if this AST is a real algebraic number.

    Declaration

    Swift

    public var isAlgebraicNumber: Bool { get }

  • Return true if this AST is a BoundVariable

    Declaration

    Swift

    public var isVar: Bool { get }

  • Return true if this AST is a Quantifier

    Declaration

    Swift

    public var isQuantifier: Bool { get }

  • Return true if this AST is a Sort

    Declaration

    Swift

    public var isSort: Bool { get }

  • Return true if this AST is a FunctionDeclaration

    Declaration

    Swift

    public var isFuncDecl: Bool { get }

  • Determine if an ast is a universal quantifier.

    Declaration

    Swift

    public var isQuantifierForAll: Bool { get }

  • Determine if ast is an existential quantifier.

    Declaration

    Swift

    public var isQuantifierExists: Bool { get }

  • Determine if ast is a lambda expression.

    Precondition

    astKind == Z3AstKind.quantifierAst

    Declaration

    Swift

    public var isLambda: Bool { get }

  • Determine if this ast is a string.

    Declaration

    Swift

    public var isString: Bool { get }

  • Return the kind of the given AST.

    Declaration

    Swift

    public var astKind: Z3AstKind { get }

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

    Declaration

    Swift

    public func translate(to newContext: Z3Context) -> Z3AstBase

  • Convert the current AST node into a string.

    Declaration

    Swift

    public func toString() -> String