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, andnil
otherwiseDeclaration
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 contexttarget
Declaration
Swift
public override func translate(to newContext: Z3Context) -> AnyZ3Ast
-
An unsafe cast from a generic
AnyZ3Ast
to aZ3Algebraic
type.Declaration
Swift
func unsafeCastToAlgebraic() -> Z3Algebraic
-
A runtime type-checked cast from a generic
AnyZ3Ast
to aZ3Algebraic
type.The underlying value is checked against
Z3Context.algebraicIsValue(_:)
, and if it succeeds, the return is aZ3Algebraic
instance.Declaration
Swift
func castToAlgebraic() -> Z3Algebraic?
-
An unsafe cast from a generic
AnyZ3Ast
or a specializedZ3Ast
to another specializedZ3RegularExp
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 specializedZ3RegularExp
to another specializedZ3RegularExp
type.The underlying
SortKind
of this AST type is checked, and if it matches the incoming sort, the result is a non-nilZ3RegularExp
instance annotated with the requested type.Declaration
Swift
func castToRegularExp<Element>(elementSort: Element.Type = Element.self) -> Z3RegularExp<Element>? where Element : SortKind