Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 [ContractVerification(true)]
00029 public class Constructor : Z3Object
00030 {
00034 public uint NumFields
00035 {
00036 get
00037 {
00038 return n;
00039 }
00040 }
00041
00045 public FuncDecl ConstructorDecl
00046 {
00047 get
00048 {
00049 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00050 IntPtr constructor = IntPtr.Zero;
00051 IntPtr tester = IntPtr.Zero;
00052 IntPtr[] accessors = new IntPtr[n];
00053 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
00054 return new FuncDecl(Context, constructor);
00055 }
00056 }
00057
00061 public FuncDecl TesterDecl
00062 {
00063 get
00064 {
00065 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00066 IntPtr constructor = IntPtr.Zero;
00067 IntPtr tester = IntPtr.Zero;
00068 IntPtr[] accessors = new IntPtr[n];
00069 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
00070 return new FuncDecl(Context, tester);
00071 }
00072 }
00073
00077 public FuncDecl[] AccessorDecls
00078 {
00079 get
00080 {
00081 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
00082 IntPtr constructor = IntPtr.Zero;
00083 IntPtr tester = IntPtr.Zero;
00084 IntPtr[] accessors = new IntPtr[n];
00085 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
00086 FuncDecl[] t = new FuncDecl[n];
00087 for (uint i = 0; i < n; i++)
00088 t[i] = new FuncDecl(Context, accessors[i]);
00089 return t;
00090 }
00091 }
00092
00096 ~Constructor()
00097 {
00098 Native.Z3_del_constructor(Context.nCtx, NativeObject);
00099 }
00100
00101 #region Internal
00102 private uint n = 0;
00103
00104 internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
00105 Sort[] sorts, uint[] sortRefs)
00106 : base(ctx)
00107 {
00108 Contract.Requires(ctx != null);
00109 Contract.Requires(name != null);
00110 Contract.Requires(recognizer != null);
00111
00112 n = AST.ArrayLength(fieldNames);
00113
00114 if (n != AST.ArrayLength(sorts))
00115 throw new Z3Exception("Number of field names does not match number of sorts");
00116 if (sortRefs != null && sortRefs.Length != n)
00117 throw new Z3Exception("Number of field names does not match number of sort refs");
00118
00119 if (sortRefs == null) sortRefs = new uint[n];
00120
00121 NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
00122 n,
00123 Symbol.ArrayToNative(fieldNames),
00124 Sort.ArrayToNative(sorts),
00125 sortRefs);
00126
00127 }
00128
00129 #endregion
00130 }
00131 }