MCPcopy Create free account
hub / github.com/Z3Prover/z3 / getConstDecls

Method getConstDecls

src/api/java/EnumSort.java:30–37  ·  view source on GitHub ↗

The function declarations of the constants in the enumeration. @throws Z3Exception on error

()

Source from the content-addressed store, hash-verified

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.

Callers 1

getConstsMethod · 0.95

Calls 3

nCtxMethod · 0.80
getContextMethod · 0.80
getNativeObjectMethod · 0.80

Tested by

no test coverage detected