Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00023 public class Constructor extends Z3Object
00024 {
00029 public int getNumFields() throws Z3Exception
00030 {
00031 return n;
00032 }
00033
00038 public FuncDecl ConstructorDecl() throws Z3Exception
00039 {
00040 Native.LongPtr constructor = new Native.LongPtr();
00041 Native.LongPtr tester = new Native.LongPtr();
00042 long[] accessors = new long[n];
00043 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
00044 return new FuncDecl(getContext(), constructor.value);
00045 }
00046
00051 public FuncDecl getTesterDecl() throws Z3Exception
00052 {
00053 Native.LongPtr constructor = new Native.LongPtr();
00054 Native.LongPtr tester = new Native.LongPtr();
00055 long[] accessors = new long[n];
00056 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
00057 return new FuncDecl(getContext(), tester.value);
00058 }
00059
00064 public FuncDecl[] getAccessorDecls() throws Z3Exception
00065 {
00066 Native.LongPtr constructor = new Native.LongPtr();
00067 Native.LongPtr tester = new Native.LongPtr();
00068 long[] accessors = new long[n];
00069 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
00070 FuncDecl[] t = new FuncDecl[n];
00071 for (int i = 0; i < n; i++)
00072 t[i] = new FuncDecl(getContext(), accessors[i]);
00073 return t;
00074 }
00075
00079 protected void finalize() throws Z3Exception
00080 {
00081 Native.delConstructor(getContext().nCtx(), getNativeObject());
00082 }
00083
00084 private int n = 0;
00085
00086 Constructor(Context ctx, Symbol name, Symbol recognizer,
00087 Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
00088 throws Z3Exception
00089 {
00090 super(ctx);
00091
00092 n = AST.arrayLength(fieldNames);
00093
00094 if (n != AST.arrayLength(sorts))
00095 throw new Z3Exception(
00096 "Number of field names does not match number of sorts");
00097 if (sortRefs != null && sortRefs.length != n)
00098 throw new Z3Exception(
00099 "Number of field names does not match number of sort refs");
00100
00101 if (sortRefs == null)
00102 sortRefs = new int[n];
00103
00104 setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
00105 recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
00106 Sort.arrayToNative(sorts), sortRefs));
00107
00108 }
00109 }