Z3 |

Properties
DatatypeSort Class Reference

Datatype sorts. More...

Inheritance diagram for DatatypeSort:

## Properties
uint | NumConstructors`[get]`
| The number of constructors of the datatype sort. More...
FuncDecl[] | Constructors`[get]`
| The constructors. More...
FuncDecl[] | Recognizers`[get]`
| The recognizers. More...
FuncDecl[][] | Accessors`[get]`
| The constructor accessors. 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
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...
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

Datatype sorts.

Definition at line 28 of file DatatypeSort.cs.

## Property Documentation

## ◆ Accessors

FuncDecl [][] Accessors
| get

The constructor accessors.

Definition at line 73 of file DatatypeSort.cs.

74 {
75 get
76 {
77
78 uint n = NumConstructors;
79 FuncDecl[][] res = new FuncDecl[n][];
80 for (uint i = 0; i < n; i++)
81 {
82 FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
83 uint ds = fd.DomainSize;
84 FuncDecl[] tmp = new FuncDecl[ds];
85 for (uint j = 0; j < ds; j++)
86 tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
87 res[i] = tmp;
88 }
89 return res;
90 }
91 }
Microsoft.Z3.DatatypeSort.NumConstructors
uint NumConstructors
The number of constructors of the datatype sort.
Definition: DatatypeSort.cs:34

## ◆ Constructors

FuncDecl [] Constructors
| get

The constructors.

Definition at line 41 of file DatatypeSort.cs.

42 {
43 get
44 {
45
46 uint n = NumConstructors;
47 FuncDecl[] res = new FuncDecl[n];
48 for (uint i = 0; i < n; i++)
49 res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
50 return res;
51 }
52 }

## ◆ NumConstructors

uint NumConstructors
| get

The number of constructors of the datatype sort.

Definition at line 33 of file DatatypeSort.cs.

34 {
35 get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
36 }

## ◆ Recognizers

FuncDecl [] Recognizers
| get

The recognizers.

Definition at line 57 of file DatatypeSort.cs.

58 {
59 get
60 {
61
62 uint n = NumConstructors;
63 FuncDecl[] res = new FuncDecl[n];
64 for (uint i = 0; i < n; i++)
65 res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
66 return res;
67 }
68 }