Z3
DatatypeSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class DatatypeSort extends Sort
24 {
28  public int getNumConstructors() throws Z3Exception
29  {
30  return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
31  getNativeObject());
32  }
33 
40  {
41  int n = getNumConstructors();
42  FuncDecl[] res = new FuncDecl[n];
43  for (int i = 0; i < n; i++)
44  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
45  getContext().nCtx(), getNativeObject(), i));
46  return res;
47  }
48 
55  {
56  int n = getNumConstructors();
57  FuncDecl[] res = new FuncDecl[n];
58  for (int i = 0; i < n; i++)
59  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
60  getContext().nCtx(), getNativeObject(), i));
61  return res;
62  }
63 
69  public FuncDecl[][] getAccessors() throws Z3Exception
70  {
71 
72  int n = getNumConstructors();
73  FuncDecl[][] res = new FuncDecl[n][];
74  for (int i = 0; i < n; i++)
75  {
76  FuncDecl fd = new FuncDecl(getContext(),
77  Native.getDatatypeSortConstructor(getContext().nCtx(),
78  getNativeObject(), i));
79  int ds = fd.getDomainSize();
80  FuncDecl[] tmp = new FuncDecl[ds];
81  for (int j = 0; j < ds; j++)
82  tmp[j] = new FuncDecl(getContext(),
84  .nCtx(), getNativeObject(), i, j));
85  res[i] = tmp;
86  }
87  return res;
88  }
89 
90  DatatypeSort(Context ctx, long obj) throws Z3Exception
91  {
92  super(ctx, obj);
93  }
94 
95  DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
96  throws Z3Exception
97  {
98  super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
99  (int) constructors.length, arrayToNative(constructors)));
100 
101  }
102 };
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2084
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2075
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2066
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2093