Z3
EnumSort.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 EnumSort.cs
7
8Abstract:
9
10 Z3 Managed API: Enum Sorts
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
28 public class EnumSort : Sort
29 {
34 {
35 get
36 {
37 uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
38 FuncDecl[] t = new FuncDecl[n];
39 for (uint i = 0; i < n; i++)
40 t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
41 return t;
42 }
43 }
44
50 public FuncDecl ConstDecl(uint inx)
51 {
52 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx));
53 }
54
58 public Expr[] Consts
59 {
60 get
61 {
62 FuncDecl[] cds = ConstDecls;
63 Expr[] t = new Expr[cds.Length];
64 for (uint i = 0; i < t.Length; i++)
65 t[i] = Context.MkApp(cds[i]);
66 return t;
67 }
68 }
69
75 public Expr Const(uint inx)
76 {
77 return Context.MkApp(ConstDecl(inx));
78 }
79
84 {
85 get
86 {
87 uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
88 FuncDecl[] t = new FuncDecl[n];
89 for (uint i = 0; i < n; i++)
90 t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
91 return t;
92 }
93 }
94
100 public FuncDecl TesterDecl(uint inx)
101 {
102 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx));
103 }
104
105 #region Internal
106 internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
107 : base(ctx, IntPtr.Zero)
108 {
109 Debug.Assert(ctx != null);
110 Debug.Assert(name != null);
111 Debug.Assert(enumNames != null);
112
113 int n = enumNames.Length;
114 IntPtr[] n_constdecls = new IntPtr[n];
115 IntPtr[] n_testers = new IntPtr[n];
116 NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
117 Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
118 }
119 #endregion
120 };
121}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
Enumeration sorts.
Definition: EnumSort.cs:29
FuncDecl TesterDecl(uint inx)
Retrieves the inx'th tester/recognizer declaration in the enumeration.
Definition: EnumSort.cs:100
Expr[] Consts
The constants in the enumeration.
Definition: EnumSort.cs:59
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
Definition: EnumSort.cs:50
FuncDecl[] ConstDecls
The function declarations of the constants in the enumeration.
Definition: EnumSort.cs:34
FuncDecl[] TesterDecls
The test predicates (recognizers) for the constants in the enumeration.
Definition: EnumSort.cs:84
Expr Const(uint inx)
Retrieves the inx'th constant in the enumeration.
Definition: EnumSort.cs:75
Expressions are terms.
Definition: Expr.cs:31
Function declarations.
Definition: FuncDecl.cs:31
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