18 package com.microsoft.z3;
40 casted =
AST.class.cast(o);
41 }
catch (ClassCastException e)
46 return this.getNativeObject() == casted.getNativeObject();
65 oAST =
AST.class.cast(other);
66 }
catch (ClassCastException e)
113 if (getContext() == ctx)
117 getNativeObject(), ctx.nCtx()));
205 return "Z3Exception: " + e.getMessage();
222 AST(Context ctx,
long obj)
230 if (getContext() == null || o == 0)
239 if (getContext() == null || o == 0)
245 static AST create(Context ctx,
long obj)
247 switch (
Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
250 return new FuncDecl(ctx, obj);
252 return new Quantifier(ctx, obj);
254 return Sort.create(ctx, obj);
258 return Expr.create(ctx, obj);
260 throw new Z3Exception(
"Unknown AST kind");
static final Z3_ast_kind fromInt(int v)
static int getAstId(long a0, long a1)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
void incAndClear(Context ctx, long o)
AST translate(Context ctx)
static int getAstHash(long a0, long a1)
static int getAstKind(long a0, long a1)
static String astToString(long a0, long a1)
static long translate(long a0, long a1, long a2)
int compareTo(Object other)