mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955)

Browse source 
* Distinguish between Quantifier and Lambda in AST.java

* Distinguish betwee Lambda and Quantifier in Expr.java

* Make things compile
This commit is contained in:
Ruijie Fang 2025-09-30 11:55:14 -05:00 • committed by Nikolaj Bjorner
parent a9a46f4ac9
commit 7bece6e473
3 changed files with 17 additions and 4 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:
return new FuncDecl<>(ctx, obj);
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.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
if (isLambda) {
return new Lambda(ctx, obj);
} else {
return new Quantifier(ctx, obj);
}
case Z3_SORT_AST:
return Sort.create(ctx, obj);
case Z3_APP_AST:

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)
{
Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
return new Quantifier(ctx, obj);
if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) {
// a quantifier AST is a lambda iff it is neither a forall nor an exists.
boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
if (isLambda) {
return new Lambda(ctx, obj);
} else {
return new Quantifier(ctx, obj);
}
}
long s = Native.getSort(ctx.nCtx(), obj);
Z3_sort_kind sk = Z3_sort_kind
.fromInt(Native.getSortKind(ctx.nCtx(), s));

2
src/api/java/Lambda.java
View file

@ -126,7 +126,7 @@ public class Lambda<R extends Sort> extends ArrayExpr<Sort, R>
}
private Lambda(Context ctx, long obj)
Lambda(Context ctx, long obj)
{
super(ctx, obj);
}