Enumeration sorts.
Definition at line 23 of file EnumSort.java.
◆ getConst()
Retrieves the inx'th constant in the enumeration.
- Exceptions
-
- Returns
- an Expr
Definition at line 66 of file EnumSort.java.
◆ getConstDecl()
Retrieves the inx'th constant declaration in the enumeration.
- Exceptions
-
Definition at line 42 of file EnumSort.java.
44 return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
Referenced by EnumSort.getConst().
◆ getConstDecls()
The function declarations of the constants in the enumeration.
- Exceptions
-
Definition at line 29 of file EnumSort.java.
31 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
32 FuncDecl[] t =
new FuncDecl[n];
33 for (
int i = 0; i < n; i++)
34 t[i] =
new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
Referenced by EnumSort.getConsts().
◆ getConsts()
The constants in the enumeration.
- Exceptions
-
- Returns
- an Expr[]
Definition at line 52 of file EnumSort.java.
55 Expr[] t =
new Expr[cds.length];
56 for (
int i = 0; i < t.length; i++)
57 t[i] = getContext().
mkApp(cds[i]);
◆ getTesterDecl()
Retrieves the inx'th tester/recognizer declaration in the enumeration.
- Exceptions
-
Definition at line 88 of file EnumSort.java.
90 return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
◆ getTesterDecls()
The test predicates for the constants in the enumeration.
- Exceptions
-
Definition at line 75 of file EnumSort.java.
77 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
78 FuncDecl[] t =
new FuncDecl[n];
79 for (
int i = 0; i < n; i++)
80 t[i] =
new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
Expr mkApp(FuncDecl f, Expr... args)