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
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
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
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 }