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 ()
 
Sort translate (Context ctx)
 
- Public Member Functions inherited from AST
int compareTo (AST other)
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
String getSExpr ()
 

Additional Inherited Members

- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

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  }

◆ getNilDecl()

FuncDecl getNilDecl ( )
inline

The declaration of the nil function of this list sort.

Exceptions
Z3Exception

Definition at line 31 of file ListSort.java.

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

Referenced by ListSort.getNil().

◆ 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  }
com.microsoft.z3.Context.mkApp
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667
com.microsoft.z3.ListSort.getNilDecl
FuncDecl getNilDecl()
Definition: ListSort.java:31