The function declarations of the constants in the enumeration. @throws Z3Exception on error
()
| 28 | * @throws Z3Exception on error |
| 29 | **/ |
| 30 | public FuncDecl<EnumSort<R>>[] getConstDecls() |
| 31 | { |
| 32 | int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); |
| 33 | FuncDecl<?>[] t = new FuncDecl[n]; |
| 34 | for (int i = 0; i < n; i++) |
| 35 | t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); |
| 36 | return (FuncDecl<EnumSort<R>>[]) t; |
| 37 | } |
| 38 | |
| 39 | /** |
| 40 | * Retrieves the inx'th constant declaration in the enumeration. |
no test coverage detected