Z3
src
api
java
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
extends
Sort
26
{
31
public
FuncDecl
getNilDecl
()
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
49
public
FuncDecl
getIsNilDecl
()
50
{
51
return
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortRecognizer
(getContext().nCtx(), getNativeObject(), 0));
52
}
53
58
public
FuncDecl
getConsDecl
()
59
{
60
return
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortConstructor
(getContext().nCtx(), getNativeObject(), 1));
61
}
62
68
public
FuncDecl
getIsConsDecl
()
69
{
70
return
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortRecognizer
(getContext().nCtx(), getNativeObject(), 1));
71
}
72
77
public
FuncDecl
getHeadDecl
()
78
{
79
return
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortConstructorAccessor
(getContext().nCtx(), getNativeObject(), 1, 0));
80
}
81
86
public
FuncDecl
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.ListSort.getIsConsDecl
FuncDecl getIsConsDecl()
Definition:
ListSort.java:68
com.microsoft.z3.ListSort.getConsDecl
FuncDecl getConsDecl()
Definition:
ListSort.java:58
com.microsoft.z3.FuncDecl
Definition:
FuncDecl.java:27
com.microsoft.z3.Sort
Definition:
Sort.java:26
com.microsoft.z3.Context.mkApp
Expr mkApp(FuncDecl f, Expr... args)
Definition:
Context.java:667
com.microsoft.z3.ListSort.getNilDecl
FuncDecl getNilDecl()
Definition:
ListSort.java:31
com.microsoft
com.microsoft.z3.Native.getDatatypeSortRecognizer
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition:
Native.java:2785
com.microsoft.z3.Native.LongPtr
Definition:
Native.java:6
com.microsoft.z3.Symbol
Definition:
Symbol.java:25
com.microsoft.z3.ListSort.getNil
Expr getNil()
Definition:
ListSort.java:40
com.microsoft.z3.Native.getDatatypeSortConstructorAccessor
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition:
Native.java:2794
com.microsoft.z3.Context.nCtx
long nCtx()
Definition:
Context.java:3966
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3
Definition:
AlgebraicNum.java:18
com.microsoft.z3.Native.mkListSort
static long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
Definition:
Native.java:1035
com.microsoft.z3.Expr
Definition:
Expr.java:30
com.microsoft.z3.ListSort
Definition:
ListSort.java:25
com.microsoft.z3.ListSort.getIsNilDecl
FuncDecl getIsNilDecl()
Definition:
ListSort.java:49
com.microsoft.z3.ListSort.getTailDecl
FuncDecl getTailDecl()
Definition:
ListSort.java:86
com
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.Native.getDatatypeSortConstructor
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition:
Native.java:2776
com.microsoft.z3.ListSort.getHeadDecl
FuncDecl getHeadDecl()
Definition:
ListSort.java:77
Generated on Sat May 9 2020 00:00:00 for Z3 by
1.8.17