Z3
Public Member Functions
ListSort Class Reference
+ Inheritance diagram for ListSort:

Public Member Functions

FuncDecl getNilDecl ()
 
Expr getNil ()
 
FuncDecl getIsNilDecl ()
 
FuncDecl getConsDecl ()
 
FuncDecl getIsConsDecl ()
 
FuncDecl getHeadDecl ()
 
FuncDecl getTailDecl ()
 
- Public Member Functions inherited from Sort
boolean equals (Object o)
 
int hashCode ()
 
int getId ()
 
Z3_sort_kind getSortKind ()
 
Symbol getName ()
 
String toString ()
 
- Public Member Functions inherited from AST
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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

List sorts.

Definition at line 23 of file ListSort.java.

Member Function Documentation

FuncDecl getConsDecl ( )
inline

The declaration of the cons function of this list sort.

Exceptions
Z3Exception

Definition at line 56 of file ListSort.java.

57  {
58  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
59  }
FuncDecl getHeadDecl ( )
inline

The declaration of the head function of this list sort.

Exceptions
Z3Exception

Definition at line 75 of file ListSort.java.

76  {
77  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
78  }
FuncDecl getIsConsDecl ( )
inline

The declaration of the isCons function of this list sort.

Exceptions
Z3Exception

Definition at line 66 of file ListSort.java.

67  {
68  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
69  }
FuncDecl getIsNilDecl ( )
inline

The declaration of the isNil function of this list sort.

Exceptions
Z3Exception

Definition at line 47 of file ListSort.java.

48  {
49  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
50  }
Expr getNil ( )
inline

The empty list.

Exceptions
Z3Exception

Definition at line 38 of file ListSort.java.

39  {
40  return getContext().mkApp(getNilDecl());
41  }
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:610
FuncDecl getNilDecl ( )
inline

The declaration of the nil function of this list sort.

Exceptions
Z3Exception

Definition at line 29 of file ListSort.java.

Referenced by ListSort.getNil().

30  {
31  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
32  }
FuncDecl getTailDecl ( )
inline

The declaration of the tail function of this list sort.

Exceptions
Z3Exception

Definition at line 84 of file ListSort.java.

85  {
86  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
87  }