18 package com.microsoft.z3;
35 if (o ==
this)
return true;
36 if (!(o instanceof
AST))
return false;
40 (getContext().nCtx() == casted.getContext().nCtx()) &&
41 (
Native.
isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
58 return Integer.compare(
getId(), other.
getId());
90 if (getContext() == ctx) {
93 return create(ctx,
Native.
translate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
194 Native.incRef(getContext().nCtx(), getNativeObject());
198 void addToReferenceQueue() {
202 static AST create(Context ctx,
long obj)
204 switch (
Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
207 return new FuncDecl(ctx, obj);
209 return new Quantifier(ctx, obj);
211 return Sort.create(ctx, obj);
215 return Expr.create(ctx, obj);
217 throw new Z3Exception(
"Unknown AST kind");