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 (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 ()
 

Detailed Description

List sorts.

Definition at line 25 of file ListSort.java.

Member Function Documentation

§ getConsDecl()

FuncDecl getConsDecl ( )
inline

The declaration of the cons function of this list sort.

Exceptions
Z3Exception

Definition at line 58 of file ListSort.java.

59  {
60  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
61  }

§ getHeadDecl()

FuncDecl getHeadDecl ( )
inline

The declaration of the head function of this list sort.

Exceptions
Z3Exception

Definition at line 77 of file ListSort.java.

78  {
79  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
80  }

§ getIsConsDecl()

FuncDecl getIsConsDecl ( )
inline

The declaration of the isCons function of this list sort.

Exceptions
Z3Exception

Definition at line 68 of file ListSort.java.

69  {
70  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
71  }

§ getIsNilDecl()

FuncDecl getIsNilDecl ( )
inline

The declaration of the isNil function of this list sort.

Exceptions
Z3Exception

Definition at line 49 of file ListSort.java.

50  {
51  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
52  }

§ getNil()

Expr getNil ( )
inline

The empty list.

Exceptions
Z3Exception

Definition at line 40 of file ListSort.java.

41  {
42  return getContext().mkApp(getNilDecl());
43  }
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:644

§ getNilDecl()

FuncDecl getNilDecl ( )
inline

The declaration of the nil function of this list sort.

Exceptions
Z3Exception

Definition at line 31 of file ListSort.java.

Referenced by ListSort.getNil().

32  {
33  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
34  }

§ getTailDecl()

FuncDecl getTailDecl ( )
inline

The declaration of the tail function of this list sort.

Exceptions
Z3Exception

Definition at line 86 of file ListSort.java.

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