18 package com.microsoft.z3;
39 casted =
AST.class.cast(o);
40 }
catch (ClassCastException e)
45 return this.getNativeObject() == casted.getNativeObject();
62 oAST =
AST.class.cast(other);
63 }
catch (ClassCastException e)
108 if (getContext() == ctx)
112 getNativeObject(), ctx.nCtx()));
191 return "Z3Exception: " + e.getMessage();
208 AST(Context ctx,
long obj)
throws Z3Exception
213 void incRef(
long o)
throws Z3Exception
216 if (getContext() == null)
217 throw new Z3Exception(
"inc() called on null context");
219 throw new Z3Exception(
"inc() called on null AST");
220 getContext().ast_DRQ().incAndClear(getContext(), o);
224 void decRef(
long o)
throws Z3Exception
227 if (getContext() == null)
228 throw new Z3Exception(
"dec() called on null context");
230 throw new Z3Exception(
"dec() called on null AST");
231 getContext().ast_DRQ().add(o);
235 static AST create(Context ctx,
long obj)
throws Z3Exception
237 switch (
Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
240 return new FuncDecl(ctx, obj);
242 return new Quantifier(ctx, obj);
244 return Sort.create(ctx, obj);
248 return Expr.create(ctx, obj);
250 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...
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)