Z3
DatatypeSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class DatatypeSort extends Sort
24 {
30  public int getNumConstructors()
31  {
32  return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
33  getNativeObject());
34  }
35 
43  {
44  int n = getNumConstructors();
45  FuncDecl[] res = new FuncDecl[n];
46  for (int i = 0; i < n; i++)
47  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
48  getContext().nCtx(), getNativeObject(), i));
49  return res;
50  }
51 
59  {
60  int n = getNumConstructors();
61  FuncDecl[] res = new FuncDecl[n];
62  for (int i = 0; i < n; i++)
63  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
64  getContext().nCtx(), getNativeObject(), i));
65  return res;
66  }
67 
74  public FuncDecl[][] getAccessors()
75  {
76 
77  int n = getNumConstructors();
78  FuncDecl[][] res = new FuncDecl[n][];
79  for (int i = 0; i < n; i++)
80  {
81  FuncDecl fd = new FuncDecl(getContext(),
82  Native.getDatatypeSortConstructor(getContext().nCtx(),
83  getNativeObject(), i));
84  int ds = fd.getDomainSize();
85  FuncDecl[] tmp = new FuncDecl[ds];
86  for (int j = 0; j < ds; j++)
87  tmp[j] = new FuncDecl(getContext(),
89  .nCtx(), getNativeObject(), i, j));
90  res[i] = tmp;
91  }
92  return res;
93  }
94 
95  DatatypeSort(Context ctx, long obj)
96  {
97  super(ctx, obj);
98  }
99 
100  DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
101 
102  {
103  super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
104  constructors.length, arrayToNative(constructors)));
105 
106  }
107 };
static long mkDatatype(long a0, long a1, int a2, long[] a3)
Definition: Native.java:992
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2438
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2429
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2420
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2447