Z3 |

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.Diagnostics;
21 using System;
22
23 namespace Microsoft.Z3
24{
28 public class Constructor : Z3Object
29 {
33 public uint NumFields
34 {
35 get
36 {
37 return n;
38 }
39 }
40
44 public FuncDecl ConstructorDecl
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
59 public FuncDecl TesterDecl
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
74 public FuncDecl[] AccessorDecls
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
92 ~Constructor()
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}
Microsoft.Z3.Constructor
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
Microsoft.Z3.Constructor.AccessorDecls
FuncDecl[] AccessorDecls
The function declarations of the accessors
Definition: Constructor.cs:75
Microsoft.Z3.Constructor.NumFields
uint NumFields
The number of fields of the constructor.
Definition: Constructor.cs:34
Microsoft.Z3.Constructor.ConstructorDecl
FuncDecl ConstructorDecl
The function declaration of the constructor.
Definition: Constructor.cs:45
Microsoft.Z3.Constructor.TesterDecl
FuncDecl TesterDecl
The function declaration of the tester.
Definition: Constructor.cs:60
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.FuncDecl
Function declarations.
Definition: FuncDecl.cs:31
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Microsoft.Z3
Definition: AlgebraicNum.cs:27