Z3
TupleSort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public class TupleSort extends Sort
24{
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
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};
FuncDecl< TupleSort > mkDecl()
Definition: TupleSort.java:29
FuncDecl<?>[] getFieldDecls()
Definition: TupleSort.java:48
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73