AST.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_ast_kind;
 
import java.lang.ref.ReferenceQueue;
 
public class AST extends Z3Object implements Comparable<AST>
{
    @Override
    public boolean equals(Object o)
    {
        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()));
    }
 
    @Override
    public int compareTo(AST other)
    {
        if (other == null) {
            return 1;
        }
        return Integer.compare(getId(), other.getId());
    }
 
    @Override
    public int hashCode()
    {
        return Native.getAstHash(getContext().nCtx(), getNativeObject());
    }
 
    public int getId()
    {
        return Native.getAstId(getContext().nCtx(), getNativeObject());
    }
 
    public int getDepth()
    {
        return Native.getDepth(getContext().nCtx(), getNativeObject());
    }
 
    public AST translate(Context ctx)
    {
        if (getContext() == ctx) {
            return this;
        } else {
            return create(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;
    }
 
    @Override
    public String toString() {
        return Native.astToString(getContext().nCtx(), getNativeObject());
    }
 
    public String getSExpr()
    {
        return Native.astToString(getContext().nCtx(), getNativeObject());
    }
 
    AST(Context ctx, long obj) {
        super(ctx, obj);
    }
 
    @Override
    void incRef() {
        Native.incRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, ASTRef::new);
    }
 
    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:
            // a quantifier AST is a lambda iff it is neither a forall nor an exists. 
            boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
            if (isLambda) {
               return new Lambda(ctx, obj);
            } else {
               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");
        }
    }
 
    private static class ASTRef extends Z3ReferenceQueue.Reference<AST> {
 
        private ASTRef(AST referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.decRef(ctx.nCtx(), z3Obj);
        }
    }
}