mirror of
https://github.com/Z3Prover/z3
synced 2025-10-04 06:53:58 +00:00
Correctly distinguish between Lambda
and Quantifier
in Z3 Java API (#7955)
* Distinguish between Quantifier and Lambda in AST.java * Distinguish betwee Lambda and Quantifier in Expr.java * Make things compile
This commit is contained in:
parent
253a7245d0
commit
339f0cd5f9
3 changed files with 17 additions and 4 deletions
|
@ -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:
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue