Public Member Functions | |
int | getNumConstructors () |
FuncDecl[] | getConstructors () |
FuncDecl[] | getRecognizers () |
FuncDecl[][] | getAccessors () |
![]() | |
boolean | equals (Object o) |
int | hashCode () |
int | getId () |
Z3_sort_kind | getSortKind () |
Symbol | getName () |
String | toString () |
![]() | |
boolean | equals (Object o) |
int | compareTo (Object 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 () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
Datatype sorts.
Definition at line 23 of file DatatypeSort.java.
|
inline |
The constructor accessors.
Z3Exception | |
Z3Exception | on error |
Definition at line 74 of file DatatypeSort.java.
|
inline |
The constructors.
Z3Exception | |
Z3Exception | on error |
Definition at line 42 of file DatatypeSort.java.
|
inline |
The number of constructors of the datatype sort.
Z3Exception | on error |
Definition at line 30 of file DatatypeSort.java.
Referenced by DatatypeSort.getAccessors(), DatatypeSort.getConstructors(), and DatatypeSort.getRecognizers().
|
inline |
The recognizers.
Z3Exception | |
Z3Exception | on error |
Definition at line 58 of file DatatypeSort.java.