Enumeration sorts. More...
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... | |
![]() | |
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... | |
![]() | |
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... | |
![]() | |
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... | |
![]() | |
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... | |
![]() | |
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 bool | operator== (Sort a, Sort b) |
Comparison operator. More... | |
static bool | operator!= (Sort a, Sort b) |
Comparison operator. More... | |
![]() | |
static bool | operator== (AST a, AST b) |
Comparison operator. More... | |
static bool | operator!= (AST a, AST b) |
Comparison operator. More... | |
Enumeration sorts.
Definition at line 29 of file EnumSort.cs.
|
inline |
Retrieves the inx'th constant in the enumeration.
inx |
Definition at line 78 of file EnumSort.cs.
|
inline |
Retrieves the inx'th constant declaration in the enumeration.
inx |
Definition at line 52 of file EnumSort.cs.
|
inline |
Retrieves the inx'th tester/recognizer declaration in the enumeration.
inx |
Definition at line 104 of file EnumSort.cs.
|
get |
The function declarations of the constants in the enumeration.
Definition at line 35 of file EnumSort.cs.
|
get |
The constants in the enumeration.
Definition at line 61 of file EnumSort.cs.
|
get |
The test predicates (recognizers) for the constants in the enumeration.
Definition at line 87 of file EnumSort.cs.