Z3 |

DatatypeSort.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 DatatypeSort.cs
7
8 Abstract:
9
10 Z3 Managed API: Datatype Sorts
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16 Notes:
17
18--*/
19
20 using System.Diagnostics;
21 using System;
22
23 namespace Microsoft.Z3
24{
28 public class DatatypeSort : Sort
29 {
33 public uint NumConstructors
34 {
35 get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
36 }
37
41 public FuncDecl[] Constructors
42 {
43 get
44 {
45
46 uint n = NumConstructors;
47 FuncDecl[] res = new FuncDecl[n];
48 for (uint i = 0; i < n; i++)
49 res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
50 return res;
51 }
52 }
53
57 public FuncDecl[] Recognizers
58 {
59 get
60 {
61
62 uint n = NumConstructors;
63 FuncDecl[] res = new FuncDecl[n];
64 for (uint i = 0; i < n; i++)
65 res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
66 return res;
67 }
68 }
69
73 public FuncDecl[][] Accessors
74 {
75 get
76 {
77
78 uint n = NumConstructors;
79 FuncDecl[][] res = new FuncDecl[n][];
80 for (uint i = 0; i < n; i++)
81 {
82 FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
83 uint ds = fd.DomainSize;
84 FuncDecl[] tmp = new FuncDecl[ds];
85 for (uint j = 0; j < ds; j++)
86 tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
87 res[i] = tmp;
88 }
89 return res;
90 }
91 }
92
93 #region Internal
94 internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
95
96 internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
97 : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
98 {
99 Debug.Assert(ctx != null);
100 Debug.Assert(name != null);
101 Debug.Assert(constructors != null);
102 }
103 #endregion
104 };
105}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.DatatypeSort
Datatype sorts.
Definition: DatatypeSort.cs:29
Microsoft.Z3.DatatypeSort.Constructors
FuncDecl[] Constructors
The constructors.
Definition: DatatypeSort.cs:42
Microsoft.Z3.DatatypeSort.NumConstructors
uint NumConstructors
The number of constructors of the datatype sort.
Definition: DatatypeSort.cs:34
Microsoft.Z3.DatatypeSort.Accessors
FuncDecl[][] Accessors
The constructor accessors.
Definition: DatatypeSort.cs:74
Microsoft.Z3.DatatypeSort.Recognizers
FuncDecl[] Recognizers
The recognizers.
Definition: DatatypeSort.cs:58
Microsoft.Z3.FuncDecl
Function declarations.
Definition: FuncDecl.cs:31
Microsoft.Z3.FuncDecl.DomainSize
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:101
Microsoft.Z3.Sort
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Microsoft.Z3
Definition: AlgebraicNum.cs:27
z3py.Length
def Length(s)
Definition: z3py.py:10852
Z3_mk_datatype
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records....