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());
91 if (getContext() == ctx) {
95 getNativeObject(), ctx.nCtx()));
200 void addToReferenceQueue() {
213 return Sort.create(ctx, obj);
217 return Expr.create(ctx, obj);
static void incRef(long a0, long a1)
IDecRefQueue< AST > getASTDRQ()
static final Z3_ast_kind fromInt(int v)
static int getAstId(long a0, long a1)
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)