Method create

src/api/java/Sort.java:116–152

(Context ctx, long obj)

    }

    static Sort create(Context ctx, long obj)
    {
        Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
        switch (sk)
        {
        case Z3_ARRAY_SORT:
            return new ArraySort<>(ctx, obj);
        case Z3_BOOL_SORT:
            return new BoolSort(ctx, obj);
        case Z3_BV_SORT:
            return new BitVecSort(ctx, obj);
        case Z3_DATATYPE_SORT:
            return new DatatypeSort<>(ctx, obj);
        case Z3_INT_SORT:
            return new IntSort(ctx, obj);
        case Z3_REAL_SORT:
            return new RealSort(ctx, obj);
        case Z3_UNINTERPRETED_SORT:
            return new UninterpretedSort(ctx, obj);
        case Z3_FINITE_DOMAIN_SORT:
            return new FiniteDomainSort(ctx, obj);
        case Z3_RELATION_SORT:
            return new RelationSort(ctx, obj);
        case Z3_FLOATING_POINT_SORT:
            return new FPSort(ctx, obj);
        case Z3_ROUNDING_MODE_SORT:
            return new FPRMSort(ctx, obj);
        case Z3_SEQ_SORT:
            return new SeqSort<>(ctx, obj);
        case Z3_RE_SORT:
            return new ReSort<>(ctx, obj);
        case Z3_CHAR_SORT:
            return new CharSort(ctx, obj);
        default:
            throw new Z3Exception("Unknown sort kind");
        }
    }
}