Z3
Public Member Functions
ListSort< R extends Sort > Class Template Reference
+ Inheritance diagram for ListSort< R extends Sort >:

Public Member Functions

FuncDecl< ListSort< R > > getNilDecl ()
 
Expr< ListSort< R > > getNil ()
 
FuncDecl< BoolSortgetIsNilDecl ()
 
FuncDecl< ListSort< R > > getConsDecl ()
 
FuncDecl< BoolSortgetIsConsDecl ()
 
FuncDecl< R > getHeadDecl ()
 
FuncDecl< ListSort< R > > 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<ListSort<R> > 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<R> 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<BoolSort> 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<BoolSort> 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<ListSort<R> > getNil ( )
inline

The empty list.

Exceptions
Z3Exception

Definition at line 40 of file ListSort.java.

41  {
42  return getContext().mkApp(getNilDecl());
43  }

◆ getNilDecl()

FuncDecl<ListSort<R> > 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< R extends Sort >.getNil().

◆ getTailDecl()

FuncDecl<ListSort<R> > 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.ListSort.getNilDecl
FuncDecl< ListSort< R > > getNilDecl()
Definition: ListSort.java:31