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;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class DatatypeSort : Sort
30  {
34  public uint NumConstructors
35  {
36  get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
37  }
38 
42  public FuncDecl[] Constructors
43  {
44  get
45  {
46  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
47 
48  uint n = NumConstructors;
49  FuncDecl[] res = new FuncDecl[n];
50  for (uint i = 0; i < n; i++)
51  res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
52  return res;
53  }
54  }
55 
59  public FuncDecl[] Recognizers
60  {
61  get
62  {
63  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
64 
65  uint n = NumConstructors;
66  FuncDecl[] res = new FuncDecl[n];
67  for (uint i = 0; i < n; i++)
68  res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
69  return res;
70  }
71  }
72 
76  public FuncDecl[][] Accessors
77  {
78  get
79  {
80  Contract.Ensures(Contract.Result<FuncDecl[][]>() != null);
81 
82  uint n = NumConstructors;
83  FuncDecl[][] res = new FuncDecl[n][];
84  for (uint i = 0; i < n; i++)
85  {
86  FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
87  uint ds = fd.DomainSize;
88  FuncDecl[] tmp = new FuncDecl[ds];
89  for (uint j = 0; j < ds; j++)
90  tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
91  res[i] = tmp;
92  }
93  return res;
94  }
95  }
96 
97  #region Internal
98  internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
99 
100  internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
101  : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
102  {
103  Contract.Requires(ctx != null);
104  Contract.Requires(name != null);
105  Contract.Requires(constructors != null);
106  }
107  #endregion
108  };
109 }
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:100
Constructors are used for datatype sorts.
Definition: Constructor.cs:29
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Function declarations.
Definition: FuncDecl.cs:29