Z3
Constructor.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class Constructor extends Z3Object
24 {
29  public int getNumFields() throws Z3Exception
30  {
31  return n;
32  }
33 
39  {
40  Native.LongPtr constructor = new Native.LongPtr();
41  Native.LongPtr tester = new Native.LongPtr();
42  long[] accessors = new long[n];
43  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
44  return new FuncDecl(getContext(), constructor.value);
45  }
46 
52  {
53  Native.LongPtr constructor = new Native.LongPtr();
54  Native.LongPtr tester = new Native.LongPtr();
55  long[] accessors = new long[n];
56  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
57  return new FuncDecl(getContext(), tester.value);
58  }
59 
65  {
66  Native.LongPtr constructor = new Native.LongPtr();
67  Native.LongPtr tester = new Native.LongPtr();
68  long[] accessors = new long[n];
69  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
70  FuncDecl[] t = new FuncDecl[n];
71  for (int i = 0; i < n; i++)
72  t[i] = new FuncDecl(getContext(), accessors[i]);
73  return t;
74  }
75 
79  protected void finalize() throws Z3Exception
80  {
81  Native.delConstructor(getContext().nCtx(), getNativeObject());
82  }
83 
84  private int n = 0;
85 
86  Constructor(Context ctx, Symbol name, Symbol recognizer,
87  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
88  throws Z3Exception
89  {
90  super(ctx);
91 
92  n = AST.arrayLength(fieldNames);
93 
94  if (n != AST.arrayLength(sorts))
95  throw new Z3Exception(
96  "Number of field names does not match number of sorts");
97  if (sortRefs != null && sortRefs.length != n)
98  throw new Z3Exception(
99  "Number of field names does not match number of sort refs");
100 
101  if (sortRefs == null)
102  sortRefs = new int[n];
103 
104  setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
105  recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
106  Sort.arrayToNative(sorts), sortRefs));
107 
108  }
109 }
static void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
Definition: Native.java:924
static void delConstructor(long a0, long a1)
Definition: Native.java:882
static long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
Definition: Native.java:873