Z3
Constructor.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class Constructor extends Z3Object {
24  private final int n;
25 
26  Constructor(Context ctx, int n, long nativeObj) {
27  super(ctx, nativeObj);
28  this.n = n;
29  }
30 
37  public int getNumFields()
38  {
39  return n;
40  }
41 
48  {
49  Native.LongPtr constructor = new Native.LongPtr();
50  Native.LongPtr tester = new Native.LongPtr();
51  long[] accessors = new long[n];
52  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
53  return new FuncDecl(getContext(), constructor.value);
54  }
55 
62  {
63  Native.LongPtr constructor = new Native.LongPtr();
64  Native.LongPtr tester = new Native.LongPtr();
65  long[] accessors = new long[n];
66  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
67  return new FuncDecl(getContext(), tester.value);
68  }
69 
76  {
77  Native.LongPtr constructor = new Native.LongPtr();
78  Native.LongPtr tester = new Native.LongPtr();
79  long[] accessors = new long[n];
80  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
81  FuncDecl[] t = new FuncDecl[n];
82  for (int i = 0; i < n; i++)
83  t[i] = new FuncDecl(getContext(), accessors[i]);
84  return t;
85  }
86 
87  @Override
88  void incRef() {
89  // Datatype constructors are not reference counted.
90  }
91 
92  @Override
93  void addToReferenceQueue() {
94  getContext().getConstructorDRQ().storeReference(getContext(), this);
95  }
96 
97  static Constructor of(Context ctx, Symbol name, Symbol recognizer,
98  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) {
99  int n = AST.arrayLength(fieldNames);
100 
101  if (n != AST.arrayLength(sorts))
102  throw new Z3Exception(
103  "Number of field names does not match number of sorts");
104  if (sortRefs != null && sortRefs.length != n)
105  throw new Z3Exception(
106  "Number of field names does not match number of sort refs");
107 
108  if (sortRefs == null)
109  sortRefs = new int[n];
110 
111  long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
112  recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
113  Sort.arrayToNative(sorts), sortRefs);
114  return new Constructor(ctx, n, nativeObj);
115 
116  }
117 }
void storeReference(Context ctx, T obj)
static void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
Definition: Native.java:1026
IDecRefQueue< Constructor > getConstructorDRQ()
Definition: Context.java:3926
static long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
Definition: Native.java:975