Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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  return n;
39  }
40  }
41 
45  public FuncDecl ConstructorDecl
46  {
47  get
48  {
49  Contract.Ensures(Contract.Result<FuncDecl>() != null);
50  IntPtr constructor = IntPtr.Zero;
51  IntPtr tester = IntPtr.Zero;
52  IntPtr[] accessors = new IntPtr[n];
53  Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
54  return new FuncDecl(Context, constructor);
55  }
56  }
57 
61  public FuncDecl TesterDecl
62  {
63  get
64  {
65  Contract.Ensures(Contract.Result<FuncDecl>() != null);
66  IntPtr constructor = IntPtr.Zero;
67  IntPtr tester = IntPtr.Zero;
68  IntPtr[] accessors = new IntPtr[n];
69  Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
70  return new FuncDecl(Context, tester);
71  }
72  }
73 
77  public FuncDecl[] AccessorDecls
78  {
79  get
80  {
81  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
82  IntPtr constructor = IntPtr.Zero;
83  IntPtr tester = IntPtr.Zero;
84  IntPtr[] accessors = new IntPtr[n];
85  Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
86  FuncDecl[] t = new FuncDecl[n];
87  for (uint i = 0; i < n; i++)
88  t[i] = new FuncDecl(Context, accessors[i]);
89  return t;
90  }
91  }
92 
96  ~Constructor()
97  {
98  Native.Z3_del_constructor(Context.nCtx, NativeObject);
99  }
100 
101  #region Internal
102  private uint n = 0;
103 
104  internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
105  Sort[] sorts, uint[] sortRefs)
106  : base(ctx)
107  {
108  Contract.Requires(ctx != null);
109  Contract.Requires(name != null);
110  Contract.Requires(recognizer != null);
111 
112  n = AST.ArrayLength(fieldNames);
113 
114  if (n != AST.ArrayLength(sorts))
115  throw new Z3Exception("Number of field names does not match number of sorts");
116  if (sortRefs != null && sortRefs.Length != n)
117  throw new Z3Exception("Number of field names does not match number of sort refs");
118 
119  if (sortRefs == null) sortRefs = new uint[n];
120 
121  NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
122  n,
123  Symbol.ArrayToNative(fieldNames),
124  Sort.ArrayToNative(sorts),
125  sortRefs);
126 
127  }
128 
129  #endregion
130  }
131 }
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
static void Z3_query_constructor(Z3_context a0, Z3_constructor a1, uint a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [Out] Z3_func_decl[] a5)
Definition: Native.cs:1999
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static void Z3_del_constructor(Z3_context a0, Z3_constructor a1)
Definition: Native.cs:1962
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
Function declarations.
Definition: FuncDecl.cs:29