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};
static long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
Definition: Native.java:1015
static int getTupleSortNumFields(long a0, long a1)
Definition: Native.java:2747
static long getTupleSortMkDecl(long a0, long a1)
Definition: Native.java:2738
static long getTupleSortFieldDecl(long a0, long a1, int a2)
Definition: Native.java:2756
FuncDecl[] getFieldDecls()
Definition: TupleSort.java:48