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 | |
int | compareTo (AST other) |
Z3_ast_kind | getASTKind () |
boolean | isExpr () |
boolean | isApp () |
boolean | isVar () |
boolean | isQuantifier () |
boolean | isSort () |
boolean | isFuncDecl () |
String | getSExpr () |
Additional Inherited Members | |
Static Public Member Functions inherited from Z3Object | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Enumeration sorts.
Definition at line 24 of file EnumSort.java.
Retrieves the inx'th constant in the enumeration.
Z3Exception | on error |
Definition at line 67 of file EnumSort.java.
Retrieves the inx'th constant declaration in the enumeration.
Z3Exception | on error |
Definition at line 43 of file EnumSort.java.
The function declarations of the constants in the enumeration.
Z3Exception | on error |
Definition at line 30 of file EnumSort.java.
The constants in the enumeration.
Z3Exception | on error |
Definition at line 53 of file EnumSort.java.
Retrieves the inx'th tester/recognizer declaration in the enumeration.
Z3Exception | on error |
Definition at line 90 of file EnumSort.java.
The test predicates for the constants in the enumeration.
Z3Exception | on error |
Definition at line 77 of file EnumSort.java.