Z3
src/api/java/AST.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import com.microsoft.z3.enumerations.Z3_ast_kind;
00021 
00025 public class AST extends Z3Object
00026 {
00027     /* Overloaded operators are not translated. */
00028 
00033     public boolean equals(Object o)
00034     {
00035         AST casted = null;
00036 
00037         try
00038         {
00039             casted = AST.class.cast(o);
00040         } catch (ClassCastException e)
00041         {
00042             return false;
00043         }
00044 
00045         return this.getNativeObject() == casted.getNativeObject();
00046     }
00047 
00054     public int compareTo(Object other) throws Z3Exception
00055     {
00056         if (other == null)
00057             return 1;
00058 
00059         AST oAST = null;
00060         try
00061         {
00062             oAST = AST.class.cast(other);
00063         } catch (ClassCastException e)
00064         {
00065             return 1;
00066         }
00067 
00068         if (getId() < oAST.getId())
00069             return -1;
00070         else if (getId() > oAST.getId())
00071             return +1;
00072         else
00073             return 0;
00074     }
00075 
00081     public int hashCode()
00082     {
00083         int r = 0;
00084         try {
00085             Native.getAstHash(getContext().nCtx(), getNativeObject());
00086         }
00087         catch (Z3Exception ex) {}
00088         return r;
00089     }
00090 
00094     public int getId() throws Z3Exception
00095     {
00096         return Native.getAstId(getContext().nCtx(), getNativeObject());
00097     }
00098 
00105     public AST translate(Context ctx) throws Z3Exception
00106     {
00107 
00108         if (getContext() == ctx)
00109             return this;
00110         else
00111             return new AST(ctx, Native.translate(getContext().nCtx(),
00112                     getNativeObject(), ctx.nCtx()));
00113     }
00114 
00118     public Z3_ast_kind getASTKind() throws Z3Exception
00119     {
00120         return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
00121                 getNativeObject()));
00122     }
00123 
00127     public boolean isExpr() throws Z3Exception
00128     {
00129         switch (getASTKind())
00130         {
00131         case Z3_APP_AST:
00132         case Z3_NUMERAL_AST:
00133         case Z3_QUANTIFIER_AST:
00134         case Z3_VAR_AST:
00135             return true;
00136         default:
00137             return false;
00138         }
00139     }
00140 
00144     public boolean isApp() throws Z3Exception
00145     {
00146         return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
00147     }
00148 
00152     public boolean isVar() throws Z3Exception
00153     {
00154         return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
00155     }
00156 
00160     public boolean isQuantifier() throws Z3Exception
00161     {
00162         return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
00163     }
00164 
00168     public boolean isSort() throws Z3Exception
00169     {
00170         return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
00171     }
00172 
00176     public boolean isFuncDecl() throws Z3Exception
00177     {
00178         return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
00179     }
00180 
00184     public String toString()
00185     {
00186         try
00187         {
00188             return Native.astToString(getContext().nCtx(), getNativeObject());
00189         } catch (Z3Exception e)
00190         {
00191             return "Z3Exception: " + e.getMessage();
00192         }
00193     }
00194 
00198     public String getSExpr() throws Z3Exception
00199     {
00200         return Native.astToString(getContext().nCtx(), getNativeObject());
00201     }
00202 
00203     AST(Context ctx)
00204     {
00205         super(ctx);
00206     }
00207 
00208     AST(Context ctx, long obj) throws Z3Exception
00209     {
00210         super(ctx, obj);
00211     }
00212 
00213     void incRef(long o) throws Z3Exception
00214     {
00215         // Console.WriteLine("AST IncRef()");
00216         if (getContext() == null)
00217             throw new Z3Exception("inc() called on null context");
00218         if (o == 0)
00219             throw new Z3Exception("inc() called on null AST");
00220         getContext().ast_DRQ().incAndClear(getContext(), o);
00221         super.incRef(o);
00222     }
00223 
00224     void decRef(long o) throws Z3Exception
00225     {
00226         // Console.WriteLine("AST DecRef()");
00227         if (getContext() == null)
00228             throw new Z3Exception("dec() called on null context");
00229         if (o == 0)
00230             throw new Z3Exception("dec() called on null AST");
00231         getContext().ast_DRQ().add(o);
00232         super.decRef(o);
00233     }
00234 
00235     static AST create(Context ctx, long obj) throws Z3Exception
00236     {
00237         switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
00238         {
00239         case Z3_FUNC_DECL_AST:
00240             return new FuncDecl(ctx, obj);
00241         case Z3_QUANTIFIER_AST:
00242             return new Quantifier(ctx, obj);
00243         case Z3_SORT_AST:
00244             return Sort.create(ctx, obj);
00245         case Z3_APP_AST:
00246         case Z3_NUMERAL_AST:
00247         case Z3_VAR_AST:
00248             return Expr.create(ctx, obj);
00249         default:
00250             throw new Z3Exception("Unknown AST kind");
00251         }
00252     }
00253 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines