|
Z3
|
|
|
Z3
|
|
A real sort More...
Inheritance diagram for RealSort: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... | |
| 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... | |
A real sort
Definition at line 28 of file RealSort.cs.
1.9.1
