Z3
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 
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, 0);
63 
64  Native.LongPtr t = new Native.LongPtr();
65  setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),
66  numFields, Symbol.arrayToNative(fieldNames),
67  AST.arrayToNative(fieldSorts), t, new long[numFields]));
68  }
69 };
FuncDecl[] getFieldDecls()
Definition: TupleSort.java:48
static long getTupleSortFieldDecl(long a0, long a1, int a2)
Definition: Native.java:2153
static long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
Definition: Native.java:942
static int getTupleSortNumFields(long a0, long a1)
Definition: Native.java:2144
static long getTupleSortMkDecl(long a0, long a1)
Definition: Native.java:2135