Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Static Public Member Functions | Protected Member Functions | Properties
Sort Class Reference

The Sort class implements type information for ASTs. More...

+ Inheritance diagram for Sort:

Public Member Functions

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...
 
- 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

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...
 

Protected Member Functions

 Sort (Context ctx)
 Sort constructor More...
 

Properties

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...
 

Detailed Description

The Sort class implements type information for ASTs.

Definition at line 29 of file Sort.cs.

Constructor & Destructor Documentation

Sort ( Context  ctx)
inlineprotected

Sort constructor

Definition at line 120 of file Sort.cs.

120 : base(ctx) { Contract.Requires(ctx != null); }

Member Function Documentation

override bool Equals ( object  o)
inline

Equality operator for objects of type Sort.

Parameters
o
Returns

Definition at line 64 of file Sort.cs.

65  {
66  Sort casted = o as Sort;
67  if (casted == null) return false;
68  return this == casted;
69  }
Sort(Context ctx)
Sort constructor
Definition: Sort.cs:120
override int GetHashCode ( )
inline

Hash code generation for Sorts

Returns
A hash code

Definition at line 75 of file Sort.cs.

76  {
77  return base.GetHashCode();
78  }
static bool operator!= ( Sort  a,
Sort  b 
)
inlinestatic

Comparison operator.

Parameters
aA Sort
bA Sort
Returns
True if a and b are not from the same context or represent different sorts; false otherwise.

Definition at line 54 of file Sort.cs.

55  {
56  return !(a == b);
57  }
static bool operator== ( Sort  a,
Sort  b 
)
inlinestatic

Comparison operator.

Parameters
aA Sort
bA Sort
Returns
True if a and b are from the same context and represent the same sort; false otherwise.

Definition at line 38 of file Sort.cs.

39  {
40  return Object.ReferenceEquals(a, b) ||
41  (!Object.ReferenceEquals(a, null) &&
42  !Object.ReferenceEquals(b, null) &&
43  a.Context == b.Context &&
44  Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
45  }
override string ToString ( )
inline

A string representation of the sort.

Definition at line 111 of file Sort.cs.

112  {
113  return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
114  }

Property Documentation

new uint Id
get

Returns a unique identifier for the sort.

Definition at line 84 of file Sort.cs.

Symbol Name
get

The name of the sort

Definition at line 100 of file Sort.cs.

Z3_sort_kind SortKind
get

The kind of the sort.

Definition at line 92 of file Sort.cs.