Enumeration sorts.
More...
Enumeration sorts.
Definition at line 28 of file EnumSort.cs.
◆ Const()
Retrieves the inx'th constant in the enumeration.
- Parameters
-
- Returns
Definition at line 75 of file EnumSort.cs.
76 {
78 }
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
◆ ConstDecl()
Retrieves the inx'th constant declaration in the enumeration.
- Parameters
-
- Returns
Definition at line 50 of file EnumSort.cs.
51 {
52 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx));
53 }
Referenced by EnumSort.Const().
◆ TesterDecl()
Retrieves the inx'th tester/recognizer declaration in the enumeration.
- Parameters
-
- Returns
Definition at line 100 of file EnumSort.cs.
101 {
102 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx));
103 }
◆ ConstDecls
The function declarations of the constants in the enumeration.
Definition at line 33 of file EnumSort.cs.
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 }
◆ Consts
The constants in the enumeration.
Definition at line 58 of file EnumSort.cs.
59 {
60 get
61 {
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 }
FuncDecl[] ConstDecls
The function declarations of the constants in the enumeration.
◆ TesterDecls
The test predicates (recognizers) for the constants in the enumeration.
Definition at line 83 of file EnumSort.cs.
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 }