Z3
src
api
java
TupleSort.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
23
public
class
TupleSort
extends
Sort
24
{
29
public
FuncDecl
mkDecl
()
30
{
31
32
return
new
FuncDecl
(getContext(),
Native
.
getTupleSortMkDecl
(getContext()
33
.nCtx(), getNativeObject()));
34
}
35
39
public
int
getNumFields
()
40
{
41
return
Native
.
getTupleSortNumFields
(getContext().nCtx(), getNativeObject());
42
}
43
48
public
FuncDecl
[]
getFieldDecls
()
49
{
50
51
int
n =
getNumFields
();
52
FuncDecl
[] res =
new
FuncDecl
[n];
53
for
(
int
i = 0; i < n; i++)
54
res[i] =
new
FuncDecl
(getContext(),
Native
.
getTupleSortFieldDecl
(
55
getContext().nCtx(), getNativeObject(), i));
56
return
res;
57
}
58
59
TupleSort
(
Context
ctx,
Symbol
name,
int
numFields,
Symbol
[] fieldNames,
60
Sort
[] fieldSorts)
61
{
62
super(ctx,
Native
.
mkTupleSort
(ctx.
nCtx
(), name.getNativeObject(),
63
numFields,
Symbol
.
arrayToNative
(fieldNames),
64
AST
.
arrayToNative
(fieldSorts),
new
Native
.
LongPtr
(),
65
new
long
[numFields]));
66
}
67
};
com.microsoft.z3.TupleSort.mkDecl
FuncDecl mkDecl()
Definition:
TupleSort.java:29
com.microsoft.z3.FuncDecl
Definition:
FuncDecl.java:27
com.microsoft.z3.Sort
Definition:
Sort.java:26
com.microsoft.z3.TupleSort.getNumFields
int getNumFields()
Definition:
TupleSort.java:39
com.microsoft.z3.Native.getTupleSortFieldDecl
static long getTupleSortFieldDecl(long a0, long a1, int a2)
Definition:
Native.java:2758
com.microsoft.z3.Native.LongPtr
Definition:
Native.java:6
com.microsoft.z3.Symbol
Definition:
Symbol.java:25
com.microsoft.z3.TupleSort
Definition:
TupleSort.java:23
com.microsoft.z3.Native.getTupleSortMkDecl
static long getTupleSortMkDecl(long a0, long a1)
Definition:
Native.java:2740
com.microsoft.z3.Context.nCtx
long nCtx()
Definition:
Context.java:3966
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.AST
Definition:
AST.java:25
com.microsoft.z3.Native.mkTupleSort
static long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
Definition:
Native.java:1017
com.microsoft.z3.Native.getTupleSortNumFields
static int getTupleSortNumFields(long a0, long a1)
Definition:
Native.java:2749
com.microsoft.z3.TupleSort.getFieldDecls
FuncDecl[] getFieldDecls()
Definition:
TupleSort.java:48
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition:
Z3Object.java:73
Generated on Sat May 9 2020 00:00:00 for Z3 by
1.8.17