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
belongsDeclaration
Swift
public let context: Z3Context
-
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 applicationDeclaration
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 BoundVariableDeclaration
Swift
public var isVar: Bool { get }
-
Return
true
if this AST is a QuantifierDeclaration
Swift
public var isQuantifier: Bool { get }
-
Return
true
if this AST is a SortDeclaration
Swift
public var isSort: Bool { get }
-
Return
true
if this AST is a FunctionDeclarationDeclaration
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 contexttarget
Declaration
Swift
public func translate(to newContext: Z3Context) -> Z3AstBase
-
Convert the current AST node into a string.
Declaration
Swift
public func toString() -> String