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

Public Member Functions

FuncDecl getNilDecl () throws Z3Exception
 
Expr getNil () throws Z3Exception
 
FuncDecl getIsNilDecl () throws Z3Exception
 
FuncDecl getConsDecl () throws Z3Exception
 
FuncDecl getIsConsDecl () throws Z3Exception
 
FuncDecl getHeadDecl () throws Z3Exception
 
FuncDecl getTailDecl () throws Z3Exception
 
- Public Member Functions inherited from Sort
boolean equals (Object o)
 
int hashCode ()
 
int getId () throws Z3Exception
 
Z3_sort_kind getSortKind () throws Z3Exception
 
Symbol getName () throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object other) throws Z3Exception
 
int hashCode ()
 
int getId () throws Z3Exception
 
AST translate (Context ctx) throws Z3Exception
 
Z3_ast_kind getASTKind () throws Z3Exception
 
boolean isExpr () throws Z3Exception
 
boolean isApp () throws Z3Exception
 
boolean isVar () throws Z3Exception
 
boolean isQuantifier () throws Z3Exception
 
boolean isSort () throws Z3Exception
 
boolean isFuncDecl () throws Z3Exception
 
String toString ()
 
String getSExpr () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Sort
 Sort (Context ctx) throws Z3Exception
 
- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

List sorts.

Definition at line 23 of file ListSort.java.

Member Function Documentation

FuncDecl getConsDecl ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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:624
FuncDecl getNilDecl ( ) throws Z3Exception
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 ( ) throws Z3Exception
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  }