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 extends Sort
26{
32 {
33 return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
34 }
35
40 public Expr getNil()
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};
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2792
static long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
Definition: Native.java:1033
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2774
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2783