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, 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 [] getFieldDecls()
Definition: TupleSort.java:48
static long getTupleSortFieldDecl(long a0, long a1, int a2)
Definition: Native.java:2411
static long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
Definition: Native.java:948
static int getTupleSortNumFields(long a0, long a1)
Definition: Native.java:2402
static long getTupleSortMkDecl(long a0, long a1)
Definition: Native.java:2393