Z3 |

Public Member Functions | Static Public Member Functions | Protected Member Functions | Properties
Symbol Class Reference

Symbols are used to name several term and type constructors. More...

Inheritance diagram for Symbol:

## Public Member Functions
bool | IsIntSymbol ()
| Indicates whether the symbol is of Int kind More...
bool | IsStringSymbol ()
| Indicates whether the symbol is of string kind. More...
override string | ToString ()
| A string representation of the symbol. More...
override bool | Equals (object o)
| Object comparison. More...
override int | GetHashCode ()
| The Symbols's hash code. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Static Public Member Functions
static bool | operator== (Symbol s1, Symbol s2)
| Equality overloading. More...
static bool | operator!= (Symbol s1, Symbol s2)
| Equality overloading. More...

## Protected Member Functions
| Symbol (Context ctx, IntPtr obj)
| Symbol constructor More...

## Properties
Z3_symbol_kind | Kind`[get]`
| The kind of the symbol (int or string) More...

## Detailed Description

Symbols are used to name several term and type constructors.

Definition at line 29 of file Symbol.cs.

## Constructor & Destructor Documentation

## ◆ Symbol()

Symbol | ( | Context | ctx,
|  | IntPtr | obj
| ) |  |
| inline protected

Symbol constructor

Definition at line 116 of file Symbol.cs.

116 : base(ctx, obj)
117 {
118 Debug.Assert(ctx != null);
119 }

Referenced by Symbol.Equals().

## Member Function Documentation

## ◆ Equals()

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

Object comparison.

Definition at line 92 of file Symbol.cs.

93 {
94 Symbol casted = o as Symbol;
95 if (casted == null) return false;
96 return this == casted;
97 }
Microsoft.Z3.Symbol.Symbol
Symbol(Context ctx, IntPtr obj)
Symbol constructor
Definition: Symbol.cs:116

## ◆ GetHashCode()

override int GetHashCode | ( |  | ) |
| inline

The Symbols's hash code.

Returns
  A hash code

Definition at line 103 of file Symbol.cs.

104 {
105 if (IsIntSymbol())
106 return ((IntSymbol)this).Int;
107 else
108 return ((StringSymbol)this).String.GetHashCode();
109 }
Microsoft.Z3.Symbol.IsIntSymbol
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Definition: Symbol.cs:42

## ◆ IsIntSymbol()

bool IsIntSymbol | ( |  | ) |
| inline

Indicates whether the symbol is of Int kind

Definition at line 42 of file Symbol.cs.

43 {
44 return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
45 }
Microsoft.Z3.Symbol.Kind
Z3_symbol_kind Kind
The kind of the symbol (int or string)
Definition: Symbol.cs:35
Z3_symbol_kind
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h:116

Referenced by Symbol.GetHashCode(), and Symbol.ToString().

## ◆ IsStringSymbol()

bool IsStringSymbol | ( |  | ) |
| inline

Indicates whether the symbol is of string kind.

Definition at line 50 of file Symbol.cs.

51 {
52 return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
53 }

Referenced by Symbol.ToString().

## ◆ operator!=()

static bool operator!= | ( | Symbol | s1,
|  | Symbol | s2
| ) |  |
| inline static

Equality overloading.

Definition at line 84 of file Symbol.cs.

85 {
86 return !(s1 == s2);
87 }

## ◆ operator==()

static bool operator== | ( | Symbol | s1,
|  | Symbol | s2
| ) |  |
| inline static

Equality overloading.

Definition at line 72 of file Symbol.cs.

73 {
74
75 return Object.ReferenceEquals(s1, s2) ||
76 (!Object.ReferenceEquals(s1, null) &&
77 !Object.ReferenceEquals(s2, null) &&
78 s1.NativeObject == s2.NativeObject);
79 }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

A string representation of the symbol.

Definition at line 58 of file Symbol.cs.

59 {
60 if (IsIntSymbol())
61 return ((IntSymbol)this).Int.ToString();
62 else if (IsStringSymbol())
63 return ((StringSymbol)this).String;
64 else
65 throw new Z3Exception("Unknown symbol kind encountered");
66 }
Microsoft.Z3.Symbol.IsStringSymbol
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Definition: Symbol.cs:50

## Property Documentation

## ◆ Kind

Z3_symbol_kind Kind
| get protected

The kind of the symbol (int or string)

Definition at line 34 of file Symbol.cs.

35 {
36 get { return (Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, NativeObject); }
37 }

Referenced by Symbol.IsIntSymbol(), and Symbol.IsStringSymbol().