Z3 |

ListSort.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
20 import com.microsoft.z3.Native.LongPtr;
21
25 public class ListSort<R extends Sort> extends Sort
26{
31 public FuncDecl<ListSort<R>> getNilDecl()
32 {
33 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
34 }
35
40 public Expr<ListSort<R>> getNil()
41 {
42 return getContext().mkApp(getNilDecl());
43 }
44
49 public FuncDecl<BoolSort> getIsNilDecl()
50 {
51 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
52 }
53
58 public FuncDecl<ListSort<R>> getConsDecl()
59 {
60 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
61 }
62
68 public FuncDecl<BoolSort> getIsConsDecl()
69 {
70 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
71 }
72
77 public FuncDecl<R> getHeadDecl()
78 {
79 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
80 }
81
86 public FuncDecl<ListSort<R>> getTailDecl()
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};
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.Context.mkApp
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:692
com.microsoft.z3.Expr
Definition: Expr.java:35
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.ListSort
Definition: ListSort.java:26
com.microsoft.z3.ListSort.getIsNilDecl
FuncDecl< BoolSort > getIsNilDecl()
Definition: ListSort.java:49
com.microsoft.z3.ListSort.getTailDecl
FuncDecl< ListSort< R > > getTailDecl()
Definition: ListSort.java:86
com.microsoft.z3.ListSort.getIsConsDecl
FuncDecl< BoolSort > getIsConsDecl()
Definition: ListSort.java:68
com.microsoft.z3.ListSort.getConsDecl
FuncDecl< ListSort< R > > getConsDecl()
Definition: ListSort.java:58
com.microsoft.z3.ListSort.getNil
Expr< ListSort< R > > getNil()
Definition: ListSort.java:40
com.microsoft.z3.ListSort.getHeadDecl
FuncDecl< R > getHeadDecl()
Definition: ListSort.java:77
com.microsoft.z3.ListSort.getNilDecl
FuncDecl< ListSort< R > > getNilDecl()
Definition: ListSort.java:31
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Symbol
Definition: Symbol.java:25