Z3 |

Public Member Functions
EnumSort< R > Class Template Reference
Inheritance diagram for EnumSort< R >:

## Public Member Functions
FuncDecl< EnumSort< R > >[] | getConstDecls ()
FuncDecl< EnumSort< R > > | getConstDecl (int inx)
Expr< EnumSort< R > >[] | getConsts ()
Expr< EnumSort< R > > | getConst (int inx)
FuncDecl< BoolSort >[] | getTesterDecls ()
FuncDecl< BoolSort > | getTesterDecl (int inx)
Public Member Functions inherited from Sort
boolean | equals (Object o)
int | hashCode ()
int | getId ()
Z3_sort_kind | getSortKind ()
Symbol | getName ()
String | toString ()
Sort | translate (Context ctx)
Public Member Functions inherited from AST
boolean | equals (Object o)
int | compareTo (AST other)
int | hashCode ()
int | getId ()
AST | translate (Context ctx)
Z3_ast_kind | getASTKind ()
boolean | isExpr ()
boolean | isApp ()
boolean | isVar ()
boolean | isQuantifier ()
boolean | isSort ()
boolean | isFuncDecl ()
String | toString ()
String | getSExpr ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Enumeration sorts.

Definition at line 24 of file EnumSort.java.

## Member Function Documentation

## ◆ getConst()

Expr< EnumSort< R > > getConst | ( | int | inx | ) |
| inline

Retrieves the inx'th constant in the enumeration.

Exceptions

  Z3Exception | on error

Returns
  an Expr

Definition at line 67 of file EnumSort.java.

68 {
69 return getContext().mkApp(getConstDecl(inx));
70 }
com.microsoft.z3.Context.mkApp
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:692
com.microsoft.z3.EnumSort.getConstDecl
FuncDecl< EnumSort< R > > getConstDecl(int inx)
Definition: EnumSort.java:43

## ◆ getConstDecl()

FuncDecl< EnumSort< R > > getConstDecl | ( | int | inx | ) |
| inline

Retrieves the inx'th constant declaration in the enumeration.

Exceptions

  Z3Exception | on error

Definition at line 43 of file EnumSort.java.

44 {
45 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
46 }

## ◆ getConstDecls()

FuncDecl< EnumSort< R > >[] getConstDecls | ( |  | ) |
| inline

The function declarations of the constants in the enumeration.

Exceptions

  Z3Exception | on error

Definition at line 30 of file EnumSort.java.

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 }
com.microsoft.z3.FuncDecl<?>

## ◆ getConsts()

Expr< EnumSort< R > >[] getConsts | ( |  | ) |
| inline

The constants in the enumeration.

Exceptions

  Z3Exception | on error

Returns
  an Expr[]

Definition at line 53 of file EnumSort.java.

54 {
55 FuncDecl<?>[] cds = getConstDecls();
56 Expr<?>[] t = new Expr[cds.length];
57 for (int i = 0; i < t.length; i++)
58 t[i] = getContext().mkApp(cds[i]);
59 return (Expr<EnumSort<R>>[]) t;
60 }
com.microsoft.z3.EnumSort.getConstDecls
FuncDecl< EnumSort< R > >[] getConstDecls()
Definition: EnumSort.java:30

## ◆ getTesterDecl()

FuncDecl< BoolSort > getTesterDecl | ( | int | inx | ) |
| inline

Retrieves the inx'th tester/recognizer declaration in the enumeration.

Exceptions

  Z3Exception | on error

Definition at line 90 of file EnumSort.java.

91 {
92 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
93 }

## ◆ getTesterDecls()

FuncDecl< BoolSort >[] getTesterDecls | ( |  | ) |
| inline

The test predicates for the constants in the enumeration.

Exceptions

  Z3Exception | on error

Definition at line 77 of file EnumSort.java.

78 {
79 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
80 FuncDecl<BoolSort>[] t = new FuncDecl[n];
81 for (int i = 0; i < n; i++)
82 t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
83 return t;
84 }