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< BoolSort > | getIsNilDecl ()
FuncDecl< ListSort< R > > | getConsDecl ()
FuncDecl< BoolSort > | getIsConsDecl ()
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
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 ()

## 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 }
com.microsoft.z3.Context.mkApp
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:692
com.microsoft.z3.ListSort.getNilDecl
FuncDecl< ListSort< R > > getNilDecl()
Definition: ListSort.java:31

## ◆ 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 }