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...
 
- Properties inherited from Z3Object
Context Context [get]
 Access Context object 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  using 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  }
uint NumConstructors
The number of constructors of the datatype sort.
Definition: DatatypeSort.cs:34
Context Context
Access Context object
Definition: Z3Object.cs:111

◆ 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  }