Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Constructor.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Constructor.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Constructors
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-22
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Constructor : Z3Object
30  {
34  public uint NumFields
35  {
36  get
37  {
38  init();
39  return n;
40  }
41  }
42 
46  public FuncDecl ConstructorDecl
47  {
48  get
49  {
50  Contract.Ensures(Contract.Result<FuncDecl>() != null);
51  init();
52  return m_constructorDecl;
53  }
54  }
55 
59  public FuncDecl TesterDecl
60  {
61  get
62  {
63  Contract.Ensures(Contract.Result<FuncDecl>() != null);
64  init();
65  return m_testerDecl;
66  }
67  }
68 
72  public FuncDecl[] AccessorDecls
73  {
74  get
75  {
76  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
77  init();
78  return m_accessorDecls;
79  }
80  }
81 
85  ~Constructor()
86  {
87  Native.Z3_del_constructor(Context.nCtx, NativeObject);
88  }
89 
90  #region Object invariant
91 
92  [ContractInvariantMethod]
93  private void ObjectInvariant()
94  {
95  Contract.Invariant(m_testerDecl == null || m_constructorDecl != null);
96  Contract.Invariant(m_testerDecl == null || m_accessorDecls != null);
97  }
98 
99  #endregion
100 
101  #region Internal
102  readonly private uint n = 0;
103  private FuncDecl m_testerDecl = null;
104  private FuncDecl m_constructorDecl = null;
105  private FuncDecl[] m_accessorDecls = null;
106 
107  internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
108  Sort[] sorts, uint[] sortRefs)
109  : base(ctx)
110  {
111  Contract.Requires(ctx != null);
112  Contract.Requires(name != null);
113  Contract.Requires(recognizer != null);
114 
115  n = AST.ArrayLength(fieldNames);
116 
117  if (n != AST.ArrayLength(sorts))
118  throw new Z3Exception("Number of field names does not match number of sorts");
119  if (sortRefs != null && sortRefs.Length != n)
120  throw new Z3Exception("Number of field names does not match number of sort refs");
121 
122  if (sortRefs == null) sortRefs = new uint[n];
123 
124  NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
125  n,
126  Symbol.ArrayToNative(fieldNames),
127  Sort.ArrayToNative(sorts),
128  sortRefs);
129 
130  }
131 
132  private void init()
133  {
134  Contract.Ensures(m_constructorDecl != null);
135  Contract.Ensures(m_testerDecl != null);
136  Contract.Ensures(m_accessorDecls != null);
137 
138  if (m_testerDecl != null) return;
139  IntPtr constructor = IntPtr.Zero;
140  IntPtr tester = IntPtr.Zero;
141  IntPtr[] accessors = new IntPtr[n];
142  Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
143  m_constructorDecl = new FuncDecl(Context, constructor);
144  m_testerDecl = new FuncDecl(Context, tester);
145  m_accessorDecls = new FuncDecl[n];
146  for (uint i = 0; i < n; i++)
147  m_accessorDecls[i] = new FuncDecl(Context, accessors[i]);
148  }
149 
150  #endregion
151  }
152 
156  public class ConstructorList : Z3Object
157  {
161  ~ConstructorList()
162  {
163  Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
164  }
165 
166  #region Internal
167  internal ConstructorList(Context ctx, IntPtr obj)
168  : base(ctx, obj)
169  {
170  Contract.Requires(ctx != null);
171  }
172 
173  internal ConstructorList(Context ctx, Constructor[] constructors)
174  : base(ctx)
175  {
176  Contract.Requires(ctx != null);
177  Contract.Requires(constructors != null);
178 
179  NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
180  }
181  #endregion
182  }
183 }