A Sequence sort. More...
Inheritance diagram for SeqSort:Additional Inherited Members | |
Public Member Functions inherited from Sort | |
| override bool | Equals (object o) |
| Equality operator for objects of type Sort. | |
| override int | GetHashCode () |
| Hash code generation for Sorts. | |
| override string | ToString () |
| A string representation of the sort. | |
| new Sort | Translate (Context ctx) |
| Translates (copies) the sort to the Context ctx . | |
Public Member Functions inherited from AST | |
| override bool | Equals (object o) |
| Object comparison. | |
| virtual int | CompareTo (object other) |
| Object Comparison. | |
| override int | GetHashCode () |
| The AST's hash code. | |
| AST | Translate (Context ctx) |
| Translates (copies) the AST to the Context ctx . | |
| override string | ToString () |
| A string representation of the AST. | |
| string | SExpr () |
| A string representation of the AST in s-expression notation. | |
Public Member Functions inherited from Z3Object | |
| void | Dispose () |
| Disposes of the underlying native Z3 object. | |
Static Public Member Functions inherited from Sort | |
| static bool | operator== (Sort a, Sort b) |
| Comparison operator. | |
| static bool | operator!= (Sort a, Sort b) |
| Comparison operator. | |
Static Public Member Functions inherited from AST | |
| static bool | operator== (AST a, AST b) |
| Comparison operator. | |
| static bool | operator!= (AST a, AST b) |
| Comparison operator. | |
Properties inherited from Sort | |
| new uint | Id [get] |
| Returns a unique identifier for the sort. | |
| Z3_sort_kind | SortKind [get] |
| The kind of the sort. | |
| Symbol | Name [get] |
| The name of the sort. | |
Properties inherited from AST | |
| uint | Id [get] |
| A unique identifier for the AST (unique among all ASTs). | |
| Z3_ast_kind | ASTKind [get] |
| The kind of the AST. | |
| bool | IsExpr [get] |
| Indicates whether the AST is an Expr. | |
| bool | IsApp [get] |
| Indicates whether the AST is an application. | |
| bool | IsVar [get] |
| Indicates whether the AST is a BoundVariable. | |
| bool | IsQuantifier [get] |
| Indicates whether the AST is a Quantifier. | |
| bool | IsSort [get] |
| Indicates whether the AST is a Sort. | |
| bool | IsFuncDecl [get] |
| Indicates whether the AST is a FunctionDeclaration. | |
Properties inherited from Z3Object | |
| Context | Context [get] |
| Access Context object. | |
A Sequence sort.
Definition at line 28 of file SeqSort.cs.