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 };
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.FuncDecl.getDomainSize
int getDomainSize()
Definition: FuncDecl.java:86
com.microsoft.z3.Native.getDatatypeSortRecognizer
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2785
com.microsoft.z3.DatatypeSort.getNumConstructors
int getNumConstructors()
Definition: DatatypeSort.java:30
com.microsoft.z3.DatatypeSort.getAccessors
FuncDecl[][] getAccessors()
Definition: DatatypeSort.java:74
com.microsoft.z3.DatatypeSort.getConstructors
FuncDecl[] getConstructors()
Definition: DatatypeSort.java:42
com.microsoft.z3.Native.getDatatypeSortConstructorAccessor
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2794
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.getDatatypeSortNumConstructors
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2767
com.microsoft.z3.DatatypeSort
Definition: DatatypeSort.java:24
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.DatatypeSort.getRecognizers
FuncDecl[] getRecognizers()
Definition: DatatypeSort.java:58
com.microsoft.z3.Native.getDatatypeSortConstructor
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2776