Java API: ClassCastException when getting EnumSort of constant

[mmsbrggr]

Consider the following scenario using the Java API: We declare a new enum-sort E and a new constant C whose sort is E.

If we now try to get the sort of C the API doesn't return an EnumSort but a DatatypeSort. If we now call a method such as getName of the returned sort the application throws a ClassCastException.

Here is a minimal example:

import com.microsoft.z3.Context;
import com.microsoft.z3.EnumSort;
import com.microsoft.z3.Expr;

public class Minimal {

    public static void main(String[] args) {
        Context ctx = new Context();
        EnumSort<Minimal> enumSort = ctx.mkEnumSort("my-enum", "e1", "e2");
        Expr<EnumSort<Minimal>> myConst = ctx.mkConst("my-const", enumSort);
        System.out.println(myConst.getSort().getName());
        ctx.close();
    }
}

Behavior: throws ClassCastException Expected: prints "my-enum"

[intrigus-lgtm]

There is no such thing as an "EnumSort" in the core z3 api: https://github.com/Z3Prover/z3/blob/6086a30c071b7a3905c722810f3b53369edb32c0/src/api/z3_api.h#L137-L155

it's all syntactic sugar for a DatatypeSort.

So when you call getSort, it calls the native API and that API can only ever return DatatypeSort.

So if you actually need to check whether the sort of a constant was an EnumSort, it is my understanding that you are out of luck. If you just want to make your code work, it should be enough to cast the result of myConst.getSort() to Sort like so: ((Sort)myConst.getSort()).getName().

Why does Java claim that getSort returns an EnumSort when it doesn't? This cast here is the reason: https://github.com/Z3Prover/z3/blob/6086a30c071b7a3905c722810f3b53369edb32c0/src/api/java/Expr.java#L239-L243