| 202 | } |
| 203 | |
| 204 | static AST create(Context ctx, long obj) |
| 205 | { |
| 206 | switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj))) |
| 207 | { |
| 208 | case Z3_FUNC_DECL_AST: |
| 209 | return new FuncDecl<>(ctx, obj); |
| 210 | case Z3_QUANTIFIER_AST: |
| 211 | // a quantifier AST is a lambda iff it is neither a forall nor an exists. |
| 212 | boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); |
| 213 | if (isLambda) { |
| 214 | return new Lambda(ctx, obj); |
| 215 | } else { |
| 216 | return new Quantifier(ctx, obj); |
| 217 | } |
| 218 | case Z3_SORT_AST: |
| 219 | return Sort.create(ctx, obj); |
| 220 | case Z3_APP_AST: |
| 221 | case Z3_NUMERAL_AST: |
| 222 | case Z3_VAR_AST: |
| 223 | return Expr.create(ctx, obj); |
| 224 | default: |
| 225 | throw new Z3Exception("Unknown AST kind"); |
| 226 | } |
| 227 | } |
| 228 | |
| 229 | private static class ASTRef extends Z3ReferenceQueue.Reference<AST> { |
| 230 | |