Z3 |

Public Member Functions | Properties
EnumSort Class Reference

Enumeration sorts. More...

Inheritance diagram for EnumSort:

## Public Member Functions
FuncDecl | ConstDecl (uint inx)
| Retrieves the inx'th constant declaration in the enumeration. More...
Expr | Const (uint inx)
| Retrieves the inx'th constant in the enumeration. More...
FuncDecl | TesterDecl (uint inx)
| Retrieves the inx'th tester/recognizer declaration in the enumeration. More...
Public Member Functions inherited from Sort
override bool | Equals (object o)
| Equality operator for objects of type Sort. More...
override int | GetHashCode ()
| Hash code generation for Sorts More...
override string | ToString ()
| A string representation of the sort. More...
new Sort | Translate (Context ctx)
| Translates (copies) the sort to the Context ctx . More...
Public Member Functions inherited from AST
override bool | Equals (object o)
| Object comparison. More...
virtual int | CompareTo (object other)
| Object Comparison. More...
override int | GetHashCode ()
| The AST's hash code. More...
AST | Translate (Context ctx)
| Translates (copies) the AST to the Context ctx . More...
override string | ToString ()
| A string representation of the AST. More...
string | SExpr ()
| A string representation of the AST in s-expression notation. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
FuncDecl[] | ConstDecls`[get]`
| The function declarations of the constants in the enumeration. More...
Expr[] | Consts`[get]`
| The constants in the enumeration. More...
FuncDecl[] | TesterDecls`[get]`
| The test predicates (recognizers) for the constants in the enumeration. More...
Properties inherited from Sort
new uint | Id`[get]`
| Returns a unique identifier for the sort. More...
Z3_sort_kind | SortKind`[get]`
| The kind of the sort. More...
Symbol | Name`[get]`
| The name of the sort More...
Properties inherited from AST
uint | Id`[get]`
| A unique identifier for the AST (unique among all ASTs). More...
Z3_ast_kind | ASTKind`[get]`
| The kind of the AST. More...
bool | IsExpr`[get]`
| Indicates whether the AST is an Expr More...
bool | IsApp`[get]`
| Indicates whether the AST is an application More...
bool | IsVar`[get]`
| Indicates whether the AST is a BoundVariable More...
bool | IsQuantifier`[get]`
| Indicates whether the AST is a Quantifier More...
bool | IsSort`[get]`
| Indicates whether the AST is a Sort More...
bool | IsFuncDecl`[get]`
| Indicates whether the AST is a FunctionDeclaration More...

## Additional Inherited Members
Static Public Member Functions inherited from Sort
static bool | operator== (Sort a, Sort b)
| Comparison operator. More...
static bool | operator!= (Sort a, Sort b)
| Comparison operator. More...
Static Public Member Functions inherited from AST
static bool | operator== (AST a, AST b)
| Comparison operator. More...
static bool | operator!= (AST a, AST b)
| Comparison operator. More...

## Detailed Description

Enumeration sorts.

Definition at line 28 of file EnumSort.cs.

## Member Function Documentation

## ◆ Const()

Expr Const | ( | uint | inx | ) |
| inline

Retrieves the inx'th constant in the enumeration.

Parameters

  inx |

Returns

Definition at line 75 of file EnumSort.cs.

76 {
77 return Context.MkApp(ConstDecl(inx));
78 }
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
Microsoft.Z3.EnumSort.ConstDecl
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
Definition: EnumSort.cs:50

## ◆ ConstDecl()

FuncDecl ConstDecl | ( | uint | inx | ) |
| inline

Retrieves the inx'th constant declaration in the enumeration.

Parameters

  inx |

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()

FuncDecl TesterDecl | ( | uint | inx | ) |
| inline

Retrieves the inx'th tester/recognizer declaration in the enumeration.

Parameters

  inx |

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 }

## Property Documentation

## ◆ ConstDecls

FuncDecl [] ConstDecls
| get

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

Expr [] Consts
| get

The constants in the enumeration.

Definition at line 58 of file EnumSort.cs.

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 }
Microsoft.Z3.EnumSort.ConstDecls
FuncDecl[] ConstDecls
The function declarations of the constants in the enumeration.
Definition: EnumSort.cs:34

## ◆ TesterDecls

FuncDecl [] TesterDecls
| get

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 }