Z3
Constructor.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class Constructor extends Z3Object
24 {
31  public int getNumFields()
32  {
33  return n;
34  }
35 
42  {
43  Native.LongPtr constructor = new Native.LongPtr();
44  Native.LongPtr tester = new Native.LongPtr();
45  long[] accessors = new long[n];
46  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
47  return new FuncDecl(getContext(), constructor.value);
48  }
49 
56  {
57  Native.LongPtr constructor = new Native.LongPtr();
58  Native.LongPtr tester = new Native.LongPtr();
59  long[] accessors = new long[n];
60  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
61  return new FuncDecl(getContext(), tester.value);
62  }
63 
70  {
71  Native.LongPtr constructor = new Native.LongPtr();
72  Native.LongPtr tester = new Native.LongPtr();
73  long[] accessors = new long[n];
74  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
75  FuncDecl[] t = new FuncDecl[n];
76  for (int i = 0; i < n; i++)
77  t[i] = new FuncDecl(getContext(), accessors[i]);
78  return t;
79  }
80 
85  protected void finalize()
86  {
87  Native.delConstructor(getContext().nCtx(), getNativeObject());
88  }
89 
90  private int n = 0;
91 
92  Constructor(Context ctx, Symbol name, Symbol recognizer,
93  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
94 
95  {
96  super(ctx);
97 
98  n = AST.arrayLength(fieldNames);
99 
100  if (n != AST.arrayLength(sorts))
101  throw new Z3Exception(
102  "Number of field names does not match number of sorts");
103  if (sortRefs != null && sortRefs.length != n)
104  throw new Z3Exception(
105  "Number of field names does not match number of sort refs");
106 
107  if (sortRefs == null)
108  sortRefs = new int[n];
109 
110  setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
111  recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
112  Sort.arrayToNative(sorts), sortRefs));
113 
114  }
115 }
static void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
Definition: Native.java:1020
static void delConstructor(long a0, long a1)
Definition: Native.java:978
static long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
Definition: Native.java:969