Z3
src/api/java/Constructor.java
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines