Z3
Constructor.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Constructor.cs
7
8Abstract:
9
10 Z3 Managed API: Constructors
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-22
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
28 public class Constructor : Z3Object
29 {
33 public uint NumFields
34 {
35 get
36 {
37 return n;
38 }
39 }
40
45 {
46 get
47 {
48 IntPtr constructor = IntPtr.Zero;
49 IntPtr tester = IntPtr.Zero;
50 IntPtr[] accessors = new IntPtr[n];
51 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
52 return new FuncDecl(Context, constructor);
53 }
54 }
55
60 {
61 get
62 {
63 IntPtr constructor = IntPtr.Zero;
64 IntPtr tester = IntPtr.Zero;
65 IntPtr[] accessors = new IntPtr[n];
66 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
67 return new FuncDecl(Context, tester);
68 }
69 }
70
75 {
76 get
77 {
78 IntPtr constructor = IntPtr.Zero;
79 IntPtr tester = IntPtr.Zero;
80 IntPtr[] accessors = new IntPtr[n];
81 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
82 FuncDecl[] t = new FuncDecl[n];
83 for (uint i = 0; i < n; i++)
84 t[i] = new FuncDecl(Context, accessors[i]);
85 return t;
86 }
87 }
88
93 {
94 Native.Z3_del_constructor(Context.nCtx, NativeObject);
95 }
96
97 #region Internal
98 private uint n = 0;
99
100 internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
101 Sort[] sorts, uint[] sortRefs)
102 : base(ctx)
103 {
104 Debug.Assert(ctx != null);
105 Debug.Assert(name != null);
106 Debug.Assert(recognizer != null);
107
108 n = AST.ArrayLength(fieldNames);
109
110 if (n != AST.ArrayLength(sorts))
111 throw new Z3Exception("Number of field names does not match number of sorts");
112 if (sortRefs != null && sortRefs.Length != n)
113 throw new Z3Exception("Number of field names does not match number of sort refs");
114
115 if (sortRefs == null) sortRefs = new uint[n];
116
117 NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
118 n,
119 Symbol.ArrayToNative(fieldNames),
120 Sort.ArrayToNative(sorts),
121 sortRefs);
122
123 }
124
125 #endregion
126 }
127}
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
FuncDecl[] AccessorDecls
The function declarations of the accessors
Definition: Constructor.cs:75
uint NumFields
The number of fields of the constructor.
Definition: Constructor.cs:34
FuncDecl ConstructorDecl
The function declaration of the constructor.
Definition: Constructor.cs:45
FuncDecl TesterDecl
The function declaration of the tester.
Definition: Constructor.cs:60
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Function declarations.
Definition: FuncDecl.cs:31
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33