mirror of
https://github.com/Z3Prover/z3
synced 2026-07-14 19:15:41 +00:00
Java API: return EnumSort instead of DatatypeSort from Sort.create() (#10104)
`Expr.getSort()` on a constant with an `EnumSort` sort returns a
`DatatypeSort`, causing `ClassCastException` when enum-specific methods
are called.
```java
Context ctx = new Context();
EnumSort<Foo> enumSort = ctx.mkEnumSort("my-enum", "e1", "e2");
Expr<EnumSort<Foo>> c = ctx.mkConst("my-const", enumSort);
c.getSort().getName(); // ClassCastException — getSort() returns DatatypeSort, not EnumSort
```
### Changes
- **`Sort.java`**: In `Sort.create()`, detect enum sorts at the
`Z3_DATATYPE_SORT` case by checking whether all constructors have arity
0 — matching Z3's own `util::is_enum_sort` logic in
`datatype_decl_plugin.cpp`. Return `EnumSort<>` when true,
`DatatypeSort<>` otherwise.
- **`EnumSort.java`**: Add package-private `EnumSort(Context ctx, long
obj)` constructor so an `EnumSort` can be instantiated from an existing
native sort handle (analogous to `DatatypeSort(Context ctx, long obj)`).
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
parent
7b26fe135a
commit
965942be79
2 changed files with 16 additions and 0 deletions
|
|
@ -92,6 +92,11 @@ public class EnumSort<R> extends Sort
|
|||
return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
|
||||
}
|
||||
|
||||
EnumSort(Context ctx, long obj)
|
||||
{
|
||||
super(ctx, obj);
|
||||
}
|
||||
|
||||
EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
|
||||
{
|
||||
super(ctx, Native.mkEnumerationSort(ctx.nCtx(),
|
||||
|
|
|
|||
|
|
@ -125,6 +125,17 @@ public class Sort extends AST
|
|||
case Z3_BV_SORT:
|
||||
return new BitVecSort(ctx, obj);
|
||||
case Z3_DATATYPE_SORT:
|
||||
int n = Native.getDatatypeSortNumConstructors(ctx.nCtx(), obj);
|
||||
boolean isEnum = true;
|
||||
for (int i = 0; i < n && isEnum; i++) {
|
||||
long ctor = Native.getDatatypeSortConstructor(ctx.nCtx(), obj, i);
|
||||
if (Native.getDomainSize(ctx.nCtx(), ctor) != 0) {
|
||||
isEnum = false;
|
||||
}
|
||||
}
|
||||
if (isEnum) {
|
||||
return new EnumSort<>(ctx, obj);
|
||||
}
|
||||
return new DatatypeSort<>(ctx, obj);
|
||||
case Z3_INT_SORT:
|
||||
return new IntSort(ctx, obj);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue