18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_ast_kind;
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");
AST translate(Context ctx)
IDecRefQueue< AST > getASTDRQ()
void storeReference(Context ctx, T obj)
static int getAstHash(long a0, long a1)
static int getAstId(long a0, long a1)
static int getAstKind(long a0, long a1)
static long translate(long a0, long a1, long a2)
static boolean isEqAst(long a0, long a1, long a2)
static String astToString(long a0, long a1)
static final Z3_ast_kind fromInt(int v)
def String(name, ctx=None)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.