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");
IDecRefQueue< AST > getASTDRQ()
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 storeReference(Context ctx, T obj)
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 boolean isEqAst(long a0, long a1, long a2)
static long translate(long a0, long a1, long a2)
def String(name, ctx=None)