Z3
src
api
java
EnumSort.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
23
public
class
EnumSort
extends
Sort
24
{
29
public
FuncDecl
[]
getConstDecls
()
30
{
31
int
n =
Native
.
getDatatypeSortNumConstructors
(getContext().nCtx(), getNativeObject());
32
FuncDecl
[] t =
new
FuncDecl
[n];
33
for
(
int
i = 0; i < n; i++)
34
t[i] =
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortConstructor
(getContext().nCtx(), getNativeObject(), i));
35
return
t;
36
}
37
42
public
FuncDecl
getConstDecl
(
int
inx)
43
{
44
return
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortConstructor
(getContext().nCtx(), getNativeObject(), inx));
45
}
46
52
public
Expr
[]
getConsts
()
53
{
54
FuncDecl
[] cds =
getConstDecls
();
55
Expr
[] t =
new
Expr
[cds.length];
56
for
(
int
i = 0; i < t.length; i++)
57
t[i] = getContext().
mkApp
(cds[i]);
58
return
t;
59
}
60
66
public
Expr
getConst
(
int
inx)
67
{
68
return
getContext().
mkApp
(
getConstDecl
(inx));
69
}
70
75
public
FuncDecl
[]
getTesterDecls
()
76
{
77
int
n =
Native
.
getDatatypeSortNumConstructors
(getContext().nCtx(), getNativeObject());
78
FuncDecl
[] t =
new
FuncDecl
[n];
79
for
(
int
i = 0; i < n; i++)
80
t[i] =
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortRecognizer
(getContext().nCtx(), getNativeObject(), i));
81
return
t;
82
}
83
88
public
FuncDecl
getTesterDecl
(
int
inx)
89
{
90
return
new
FuncDecl
(getContext(),
Native
.
getDatatypeSortRecognizer
(getContext().nCtx(), getNativeObject(), inx));
91
}
92
93
EnumSort
(
Context
ctx,
Symbol
name,
Symbol
[] enumNames)
94
{
95
super(ctx,
Native
.
mkEnumerationSort
(ctx.nCtx(),
96
name.getNativeObject(), enumNames.length,
97
Symbol
.arrayToNative(enumNames),
98
new
long
[enumNames.length],
new
long
[enumNames.length]));
99
}
100
};
com.microsoft.z3.Native.mkEnumerationSort
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
Definition:
Native.java:1024
com.microsoft.z3.EnumSort.getTesterDecls
FuncDecl[] getTesterDecls()
Definition:
EnumSort.java:75
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.Native.getDatatypeSortRecognizer
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition:
Native.java:2783
com.microsoft.z3.Symbol
Definition:
Symbol.java:25
com.microsoft.z3.EnumSort.getConstDecls
FuncDecl[] getConstDecls()
Definition:
EnumSort.java:29
com.microsoft.z3.EnumSort.getConst
Expr getConst(int inx)
Definition:
EnumSort.java:66
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.Native.getDatatypeSortNumConstructors
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition:
Native.java:2765
com.microsoft.z3.Expr
Definition:
Expr.java:30
com.microsoft.z3.EnumSort
Definition:
EnumSort.java:23
com.microsoft.z3.EnumSort.getTesterDecl
FuncDecl getTesterDecl(int inx)
Definition:
EnumSort.java:88
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.EnumSort.getConstDecl
FuncDecl getConstDecl(int inx)
Definition:
EnumSort.java:42
com.microsoft.z3.Native.getDatatypeSortConstructor
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition:
Native.java:2774
com.microsoft.z3.EnumSort.getConsts
Expr[] getConsts()
Definition:
EnumSort.java:52
Generated on Thu Feb 27 2020 00:00:00 for Z3 by
1.8.17