Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions | Static Package Functions
AST Class Reference
+ Inheritance diagram for AST:

Public Member Functions

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

Package Functions

 AST (Context ctx)
 AST (Context ctx, long obj) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) throws Z3Exception

Static Package Functions

static AST create (Context ctx, long obj) throws Z3Exception

Detailed Description

The abstract syntax tree (AST) class.

Definition at line 25 of file AST.java.


Constructor & Destructor Documentation

AST ( Context  ctx) [inline, package]

Definition at line 203 of file AST.java.

Referenced by FuncDecl.getParameters(), and AST.translate().

    {
        super(ctx);
    }
AST ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 208 of file AST.java.

    {
        super(ctx, obj);
    }

Member Function Documentation

int compareTo ( Object  other) throws Z3Exception [inline]

Object Comparison.

Parameters:
otherAnother AST
Returns:
Negative if the object should be sorted before other , positive if after else zero.

Definition at line 54 of file AST.java.

    {
        if (other == null)
            return 1;

        AST oAST = null;
        try
        {
            oAST = AST.class.cast(other);
        } catch (ClassCastException e)
        {
            return 1;
        }

        if (getId() < oAST.getId())
            return -1;
        else if (getId() > oAST.getId())
            return +1;
        else
            return 0;
    }
static AST create ( Context  ctx,
long  obj 
) throws Z3Exception [inline, static, package]

Reimplemented in Expr, and Sort.

Definition at line 235 of file AST.java.

Referenced by Context.wrapAST().

    {
        switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
        {
        case Z3_FUNC_DECL_AST:
            return new FuncDecl(ctx, obj);
        case Z3_QUANTIFIER_AST:
            return new Quantifier(ctx, obj);
        case Z3_SORT_AST:
            return Sort.create(ctx, obj);
        case Z3_APP_AST:
        case Z3_NUMERAL_AST:
        case Z3_VAR_AST:
            return Expr.create(ctx, obj);
        default:
            throw new Z3Exception("Unknown AST kind");
        }
    }
void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 224 of file AST.java.

    {
        // Console.WriteLine("AST DecRef()");
        if (getContext() == null)
            throw new Z3Exception("dec() called on null context");
        if (o == 0)
            throw new Z3Exception("dec() called on null AST");
        getContext().ast_DRQ().add(o);
        super.decRef(o);
    }
boolean equals ( Object  o) [inline]

Object comparison.

Parameters:
oanother AST

Reimplemented in FuncDecl, and Sort.

Definition at line 33 of file AST.java.

    {
        AST casted = null;

        try
        {
            casted = AST.class.cast(o);
        } catch (ClassCastException e)
        {
            return false;
        }

        return this.getNativeObject() == casted.getNativeObject();
    }
Z3_ast_kind getASTKind ( ) throws Z3Exception [inline]

The kind of the AST.

Definition at line 118 of file AST.java.

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

    {
        return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
                getNativeObject()));
    }
int getId ( ) throws Z3Exception [inline]

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

Reimplemented in FuncDecl, and Sort.

Definition at line 94 of file AST.java.

Referenced by AST.compareTo().

    {
        return Native.getAstId(getContext().nCtx(), getNativeObject());
    }
String getSExpr ( ) throws Z3Exception [inline]

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

Definition at line 198 of file AST.java.

    {
        return Native.astToString(getContext().nCtx(), getNativeObject());
    }
int hashCode ( ) [inline]

The AST's hash code.

Returns:
A hash code

Reimplemented in FuncDecl, and Sort.

Definition at line 81 of file AST.java.

    {
        int r = 0;
        try {
            Native.getAstHash(getContext().nCtx(), getNativeObject());
        }
        catch (Z3Exception ex) {}
        return r;
    }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 213 of file AST.java.

    {
        // Console.WriteLine("AST IncRef()");
        if (getContext() == null)
            throw new Z3Exception("inc() called on null context");
        if (o == 0)
            throw new Z3Exception("inc() called on null AST");
        getContext().ast_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }
boolean isApp ( ) throws Z3Exception [inline]

Indicates whether the AST is an application

Definition at line 144 of file AST.java.

Referenced by Expr.isAdd(), Expr.isAnd(), Expr.isArithmeticNumeral(), Expr.isArrayMap(), Expr.isAsArray(), Expr.isBVAdd(), Expr.isBVAND(), Expr.isBVBitOne(), Expr.isBVBitZero(), Expr.isBVCarry(), Expr.isBVComp(), Expr.isBVConcat(), Expr.isBVExtract(), Expr.isBVMul(), Expr.isBVNAND(), Expr.isBVNOR(), Expr.isBVNOT(), Expr.isBVNumeral(), Expr.isBVOR(), Expr.isBVReduceAND(), Expr.isBVReduceOR(), Expr.isBVRepeat(), Expr.isBVRotateLeft(), Expr.isBVRotateLeftExtended(), Expr.isBVRotateRight(), Expr.isBVRotateRightExtended(), Expr.isBVSDiv(), Expr.IsBVSDiv0(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.IsBVSMod0(), Expr.isBVSRem(), Expr.IsBVSRem0(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.IsBVUDiv0(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.IsBVURem0(), Expr.isBVXNOR(), Expr.isBVXOR(), Expr.isBVXOR3(), Expr.isBVZeroExtension(), Expr.isConst(), Expr.isConstantArray(), Expr.isDefaultArray(), Expr.isDistinct(), Expr.isDiv(), Expr.isEmptyRelation(), Expr.isEq(), Expr.isFalse(), Expr.isFiniteDomainLT(), Expr.isGE(), Expr.isGT(), Expr.isIDiv(), Expr.isIff(), Expr.isImplies(), Expr.isIntToBV(), Expr.isIntToReal(), Expr.isIsEmptyRelation(), Expr.isITE(), Expr.isLabel(), Expr.isLabelLit(), Expr.isLE(), Expr.isLT(), Expr.isModulus(), Expr.isMul(), Expr.isNot(), Expr.isOEQ(), Expr.isOr(), Expr.isProofAndElimination(), Expr.isProofApplyDef(), Expr.isProofAsserted(), Expr.isProofCNFStar(), Expr.isProofCommutativity(), Expr.isProofDefAxiom(), Expr.isProofDefIntro(), Expr.isProofDER(), Expr.isProofDistributivity(), Expr.isProofElimUnusedVars(), Expr.isProofGoal(), Expr.isProofHypothesis(), Expr.isProofIFFFalse(), Expr.isProofIFFOEQ(), Expr.isProofIFFTrue(), Expr.isProofLemma(), Expr.isProofModusPonens(), Expr.isProofModusPonensOEQ(), Expr.isProofMonotonicity(), Expr.isProofNNFNeg(), Expr.isProofNNFPos(), Expr.isProofNNFStar(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPullQuantStar(), Expr.isProofPushQuant(), Expr.isProofQuantInst(), Expr.isProofQuantIntro(), Expr.isProofReflexivity(), Expr.isProofRewrite(), Expr.isProofRewriteStar(), Expr.isProofSkolemize(), Expr.isProofSymmetry(), Expr.isProofTheoryLemma(), Expr.isProofTransitivity(), Expr.isProofTransitivityStar(), Expr.isProofTrue(), Expr.isProofUnitResolution(), Expr.isRealIsInt(), Expr.isRealToInt(), Expr.isRelationalJoin(), Expr.isRelationClone(), Expr.isRelationComplement(), Expr.isRelationFilter(), Expr.isRelationNegationFilter(), Expr.isRelationProject(), Expr.isRelationRename(), Expr.isRelationSelect(), Expr.isRelationStore(), Expr.isRelationUnion(), Expr.isRelationWiden(), Expr.isRemainder(), Expr.isSelect(), Expr.isSetComplement(), Expr.isSetDifference(), Expr.isSetIntersect(), Expr.isSetSubset(), Expr.isSetUnion(), Expr.isStore(), Expr.isSub(), Expr.isTrue(), Expr.isUMinus(), Expr.isXor(), and Expr.update().

    {
        return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
    }
boolean isExpr ( ) throws Z3Exception [inline]

Indicates whether the AST is an Expr

Definition at line 127 of file AST.java.

Referenced by Expr.isBool().

    {
        switch (getASTKind())
        {
        case Z3_APP_AST:
        case Z3_NUMERAL_AST:
        case Z3_QUANTIFIER_AST:
        case Z3_VAR_AST:
            return true;
        default:
            return false;
        }
    }
boolean isFuncDecl ( ) throws Z3Exception [inline]

Indicates whether the AST is a FunctionDeclaration

Definition at line 176 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
    }
boolean isQuantifier ( ) throws Z3Exception [inline]

Indicates whether the AST is a Quantifier

Definition at line 160 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
    }
boolean isSort ( ) throws Z3Exception [inline]

Indicates whether the AST is a Sort

Definition at line 168 of file AST.java.

    {
        return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
    }
boolean isVar ( ) throws Z3Exception [inline]

Indicates whether the AST is a BoundVariable

Definition at line 152 of file AST.java.

Referenced by Expr.getIndex().

    {
        return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
    }
String toString ( ) [inline]

A string representation of the AST.

Reimplemented in Expr, Sort, RatNum, FuncDecl, IntNum, BitVecNum, and Pattern.

Definition at line 184 of file AST.java.

    {
        try
        {
            return Native.astToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }
AST translate ( Context  ctx) throws Z3Exception [inline]

Translates (copies) the AST to the Context ctx .

Parameters:
ctxA context
Returns:
A copy of the AST which is associated with ctx

Reimplemented in Expr.

Definition at line 105 of file AST.java.

    {

        if (getContext() == ctx)
            return this;
        else
            return new AST(ctx, Native.translate(getContext().nCtx(),
                    getNativeObject(), ctx.nCtx()));
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines