AST.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_ast_kind;

public class AST extends Z3Object implements Comparable
{
    public boolean equals(Object o)
    {
        AST casted = null;

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

        return  
            (this == casted) || 
            (this != null) &&
            (casted != null) &&
            (getContext().nCtx() == casted.getContext().nCtx()) &&
            (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
}

    public int compareTo(Object other)
    {
        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;
    }

    public int hashCode()
    {
        int r = 0;
        try {
            Native.getAstHash(getContext().nCtx(), getNativeObject());
        }
        catch (Z3Exception ex) {}
        return r;
    }

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

    public AST translate(Context ctx)
    {

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

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

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

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

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

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

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

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

    public String toString()
    {
        try
        {
            return Native.astToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

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

    AST(Context ctx)
    {
        super(ctx);
    }

    AST(Context ctx, long obj)
    {
        super(ctx, obj);
    }

    void incRef(long o)
    {
        // Console.WriteLine("AST IncRef()");
        if (getContext() == null || o == 0)
            return;
        getContext().getASTDRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

    void decRef(long o)
    {
        // Console.WriteLine("AST DecRef()");
        if (getContext() == null || o == 0)
            return;
        getContext().getASTDRQ().add(o);
        super.decRef(o);
    }

    static AST create(Context ctx, long obj)
    {
        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");
        }
    }
}