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());
69 return Native.getAstHash(getContext().nCtx(), getNativeObject());
78 return Native.getAstId(getContext().nCtx(), getNativeObject());
90 if (getContext() == ctx) {
93 return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.
nCtx()));
103 return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
177 return Native.astToString(getContext().nCtx(), getNativeObject());
185 return Native.astToString(getContext().nCtx(), getNativeObject());
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)
def String(name, ctx=None)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.