Public Member Functions | |
FuncDecl | getNilDecl () |
Expr | getNil () |
FuncDecl | getIsNilDecl () |
FuncDecl | getConsDecl () |
FuncDecl | getIsConsDecl () |
FuncDecl | getHeadDecl () |
FuncDecl | getTailDecl () |
![]() | |
boolean | equals (Object o) |
int | hashCode () |
int | getId () |
Z3_sort_kind | getSortKind () |
Symbol | getName () |
String | toString () |
![]() | |
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 () |
List sorts.
Definition at line 25 of file ListSort.java.
|
inline |
The declaration of the cons function of this list sort.
Z3Exception |
Definition at line 58 of file ListSort.java.
|
inline |
The declaration of the head function of this list sort.
Z3Exception |
Definition at line 77 of file ListSort.java.
|
inline |
The declaration of the isCons function of this list sort.
Z3Exception |
Definition at line 68 of file ListSort.java.
|
inline |
The declaration of the isNil function of this list sort.
Z3Exception |
Definition at line 49 of file ListSort.java.
|
inline |
|
inline |
The declaration of the nil function of this list sort.
Z3Exception |
Definition at line 31 of file ListSort.java.
Referenced by ListSort.getNil().
|
inline |
The declaration of the tail function of this list sort.
Z3Exception |
Definition at line 86 of file ListSort.java.