mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Distinguish betwee Lambda and Quantifier in Expr.java

Browse source
This commit is contained in:
Ruijie Fang 2025-09-29 21:48:33 -05:00 • committed by GitHub
parent 121f66c19c
commit c791694af8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/java/Expr.java
View file

@ -2148,8 +2148,15 @@ public class Expr<R extends Sort> extends AST
static Expr<?> create(Context ctx, long obj) static Expr<?> create(Context ctx, long obj)
{ {
Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) {
return new Quantifier(ctx, obj); // a quantifier AST is a lambda iff it is neither a forall nor an exists.
boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj);
if (isLambda) {
return new Lambda(ctx, obj);
} else {
return new Quantifier(ctx, obj);
}
}
long s = Native.getSort(ctx.nCtx(), obj); long s = Native.getSort(ctx.nCtx(), obj);
Z3_sort_kind sk = Z3_sort_kind Z3_sort_kind sk = Z3_sort_kind
.fromInt(Native.getSortKind(ctx.nCtx(), s)); .fromInt(Native.getSortKind(ctx.nCtx(), s));