(Context ctx, Symbol name, Symbol recognizer,
Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
| 97 | } |
| 98 | |
| 99 | static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer, |
| 100 | Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { |
| 101 | int n = AST.arrayLength(fieldNames); |
| 102 | |
| 103 | if (n != AST.arrayLength(sorts)) |
| 104 | throw new Z3Exception( |
| 105 | "Number of field names does not match number of sorts"); |
| 106 | if (sortRefs != null && sortRefs.length != n) |
| 107 | throw new Z3Exception( |
| 108 | "Number of field names does not match number of sort refs"); |
| 109 | |
| 110 | if (sortRefs == null) |
| 111 | sortRefs = new int[n]; |
| 112 | |
| 113 | long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), |
| 114 | recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames), |
| 115 | Sort.arrayToNative(sorts), sortRefs); |
| 116 | return new Constructor<>(ctx, n, nativeObj); |
| 117 | |
| 118 | } |
| 119 | |
| 120 | private static class ConstructorRef extends Z3ReferenceQueue.Reference<Constructor<?>> { |
| 121 |
nothing calls this directly
no test coverage detected