Z3 |

Public Member Functions | Static Public 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...
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
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
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 28 of file Sort.cs.

## Member Function Documentation

## ◆ Equals()

override bool Equals | ( | object | o | ) |
| inline

Equality operator for objects of type Sort.

Parameters

  o |

Returns

Definition at line 63 of file Sort.cs.

64 {
65 Sort casted = o as Sort;
66 if (casted == null) return false;
67 return this == casted;
68 }

## ◆ GetHashCode()

override int GetHashCode | ( |  | ) |
| inline

Hash code generation for Sorts

Returns
  A hash code

Definition at line 74 of file Sort.cs.

75 {
76 return base.GetHashCode();
77 }

## ◆ operator!=()

static bool operator!= | ( | Sort | a,
|  | Sort | b
| ) |  |
| inline static

Comparison operator.

Parameters

  a | A Sort
  b | A Sort

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

Definition at line 53 of file Sort.cs.

54 {
55 return !(a == b);
56 }

## ◆ operator==()

static bool operator== | ( | Sort | a,
|  | Sort | b
| ) |  |
| inline static

Comparison operator.

Parameters

  a | A Sort
  b | A Sort

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

Definition at line 37 of file Sort.cs.

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

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

A string representation of the sort.

Definition at line 109 of file Sort.cs.

110 {
111 return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
112 }

## ◆ Translate()

new Sort Translate | ( | Context | ctx | ) |
| inline

Translates (copies) the sort to the Context ctx .

Parameters

  ctx | A context

Returns
  A copy of the sort which is associated with ctx

Definition at line 119 of file Sort.cs.

120 {
121 return (Sort)base.Translate(ctx);
122 }

Referenced by Sort.Translate().

## Property Documentation

## ◆ Id

new uint Id
| get

Returns a unique identifier for the sort.

Definition at line 82 of file Sort.cs.

83 {
84 get { return Native.Z3_get_sort_id(Context.nCtx, NativeObject); }
85 }

## ◆ Name

Symbol Name
| get

The name of the sort

Definition at line 98 of file Sort.cs.

99 {
100 get
101 {
102 return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
103 }
104 }

## ◆ SortKind

Z3_sort_kind SortKind
| get

The kind of the sort.

Definition at line 90 of file Sort.cs.

91 {
92 get { return (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, NativeObject); }
93 }
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150