Z3
ListSort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.Native.LongPtr;
21
25public class ListSort<R extends Sort> extends Sort
26{
32 {
33 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
34 }
35
41 {
42 return getContext().mkApp(getNilDecl());
43 }
44
50 {
51 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
52 }
53
59 {
60 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
61 }
62
69 {
70 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
71 }
72
78 {
79 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
80 }
81
87 {
88 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
89 }
90
91 ListSort(Context ctx, Symbol name, Sort elemSort)
92 {
93 super(ctx, Native.mkListSort(ctx.nCtx(), name.getNativeObject(),
94 elemSort.getNativeObject(),
95 new LongPtr(), new Native.LongPtr(), new LongPtr(),
96 new LongPtr(), new LongPtr(), new LongPtr()));
97 }
98};
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:692
FuncDecl< BoolSort > getIsNilDecl()
Definition: ListSort.java:49
FuncDecl< ListSort< R > > getTailDecl()
Definition: ListSort.java:86
FuncDecl< BoolSort > getIsConsDecl()
Definition: ListSort.java:68
FuncDecl< ListSort< R > > getConsDecl()
Definition: ListSort.java:58
Expr< ListSort< R > > getNil()
Definition: ListSort.java:40
FuncDecl< R > getHeadDecl()
Definition: ListSort.java:77
FuncDecl< ListSort< R > > getNilDecl()
Definition: ListSort.java:31