AST Class Reference

Inheritance diagram for AST:

Public Member Functions
boolean	equals (Object o)
int	compareTo (AST other)
int	hashCode ()
int	getId ()
int	getDepth ()
AST	translate (Context ctx)
Z3_ast_kind	getASTKind ()
boolean	isExpr ()
boolean	isApp ()
boolean	isVar ()
boolean	isQuantifier ()
boolean	isSort ()
boolean	isFuncDecl ()
String	toString ()
String	getSExpr ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

The abstract syntax tree (AST) class.

Definition at line 27 of file AST.java.

Member Function Documentation

compareTo()

int compareTo ( AST  other )

inline

Object Comparison.

Parameters

other

Another AST

Returns

Negative if the object should be sorted before other, positive if after else zero.

Exceptions

Z3Exception

on error

Definition at line 55 of file AST.java.

    {
        if (other == null) {
            return 1;
        }
        return Integer.compare(getId(), other.getId());
    }

equals()

boolean equals ( Object  o )

inline

Object comparison.

Parameters

o	another AST

Reimplemented in FuncDecl< R extends Sort >, and Sort.

Definition at line 35 of file AST.java.

    {
        if (o == this) return true;
        if (!(o instanceof AST)) return false;
        AST casted = (AST) o;
 
        return
            (getContext().nCtx() == casted.getContext().nCtx()) &&
                (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
    }

getASTKind()

Z3_ast_kind getASTKind ( )

inline

The kind of the AST.

Exceptions

Z3Exception

on error

Definition at line 113 of file AST.java.

    {
        return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
                getNativeObject()));
    }

Referenced by AST.isApp(), AST.isExpr(), AST.isFuncDecl(), AST.isQuantifier(), AST.isSort(), and AST.isVar().

getDepth()

int getDepth ( )

inline

The depth of the AST (max nodes on any root-to-leaf path).

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 88 of file AST.java.

    {
        return Native.getDepth(getContext().nCtx(), getNativeObject());
    }

getId()

int getId ( )

inline

A unique identifier for the AST (unique among all ASTs).

Exceptions

Z3Exception

on error

Reimplemented in FuncDecl< R extends Sort >, and Sort.

Definition at line 78 of file AST.java.

    {
        return Native.getAstId(getContext().nCtx(), getNativeObject());
    }

Referenced by AST.compareTo().

getSExpr()

String getSExpr ( )

inline

A string representation of the AST in s-expression notation.

Definition at line 195 of file AST.java.

    {
        return Native.astToString(getContext().nCtx(), getNativeObject());
    }

hashCode()

int hashCode ( )

inline

The AST's hash code.

Returns

A hash code

Reimplemented in Sort.

Definition at line 69 of file AST.java.

    {
        return Native.getAstHash(getContext().nCtx(), getNativeObject());
    }

isApp()

boolean isApp ( )

inline

Indicates whether the AST is an application

Returns

a boolean

Exceptions

Z3Exception

on error

Definition at line 143 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
    }

isExpr()

boolean isExpr ( )

inline

Indicates whether the AST is an Expr

Exceptions

Z3Exception	on error
Z3Exception	on error

Definition at line 124 of file AST.java.

    {
        switch (getASTKind())
        {
        case Z3_APP_AST:
        case Z3_NUMERAL_AST:
        case Z3_QUANTIFIER_AST:
        case Z3_VAR_AST:
            return true;
        default:
            return false;
        }
    }

isFuncDecl()

boolean isFuncDecl ( )

inline

Indicates whether the AST is a FunctionDeclaration

Definition at line 179 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
    }

isQuantifier()

boolean isQuantifier ( )

inline

Indicates whether the AST is a Quantifier

Returns

a boolean

Exceptions

Z3Exception

on error

Definition at line 163 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
    }

isSort()

boolean isSort ( )

inline

Indicates whether the AST is a Sort

Definition at line 171 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
    }

isVar()

boolean isVar ( )

inline

Indicates whether the AST is a BoundVariable.

Returns

a boolean

Exceptions

Z3Exception

on error

Definition at line 153 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
    }

toString()

String toString ( )

inline

A string representation of the AST.

Reimplemented in Expr< R extends Sort >, FuncDecl< R extends Sort >, Pattern, and Sort.

Definition at line 188 of file AST.java.

                             {
        return Native.astToString(getContext().nCtx(), getNativeObject());
    }

translate()

AST translate ( Context  ctx )

inline

Translates (copies) the AST to the Context ctx.

Parameters

ctx

A context

Returns

A copy of the AST which is associated with ctx

Exceptions

Z3Exception

on error

Reimplemented in Expr< R extends Sort >, FuncDecl< R extends Sort >, and Sort.

Definition at line 100 of file AST.java.

    {
        if (getContext() == ctx) {
            return this;
        } else {
            return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
        }
    }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), and ModelRef.__deepcopy__().