Enumeration sorts.
More...
Enumeration sorts.
Definition at line 29 of file EnumSort.cs.
◆ Const()
Retrieves the inx'th constant in the enumeration.
- Parameters
-
- Returns
Definition at line 78 of file EnumSort.cs.
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
◆ ConstDecl()
Retrieves the inx'th constant declaration in the enumeration.
- Parameters
-
- Returns
Definition at line 52 of file EnumSort.cs.
54 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx));
◆ TesterDecl()
Retrieves the inx'th tester/recognizer declaration in the enumeration.
- Parameters
-
- Returns
Definition at line 104 of file EnumSort.cs.
106 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx));
◆ ConstDecls
The function declarations of the constants in the enumeration.
Definition at line 35 of file EnumSort.cs.
38 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
39 uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
40 FuncDecl[] t =
new FuncDecl[n];
41 for (uint i = 0; i < n; i++)
42 t[i] =
new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
◆ Consts
The constants in the enumeration.
Definition at line 61 of file EnumSort.cs.
64 Contract.Ensures(Contract.Result<Expr[]>() != null);
66 Expr[] t =
new Expr[cds.Length];
67 for (uint i = 0; i < t.Length; i++)
68 t[i] = Context.
MkApp(cds[i]);
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
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 87 of file EnumSort.cs.
90 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
91 uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
92 FuncDecl[] t =
new FuncDecl[n];
93 for (uint i = 0; i < n; i++)
94 t[i] =
new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));