mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 11:16:54 +00:00
Code Activity

Distinguish between Quantifier and Lambda in AST.java

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

8
src/api/java/AST.java
View file

@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable<AST>
case Z3_FUNC_DECL_AST: case Z3_FUNC_DECL_AST:
return new FuncDecl<>(ctx, obj); return new FuncDecl<>(ctx, obj);
case Z3_QUANTIFIER_AST: case 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);
}
case Z3_SORT_AST: case Z3_SORT_AST:
return Sort.create(ctx, obj); return Sort.create(ctx, obj);
case Z3_APP_AST: case Z3_APP_AST: