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 
)
inlineprotected

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  }

◆ 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  }

◆ 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  }

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 
)
inlinestatic

Equality overloading.

Definition at line 84 of file Symbol.cs.

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

◆ operator==()

static bool operator== ( Symbol  s1,
Symbol  s2 
)
inlinestatic

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  }

Property Documentation

◆ Kind

Z3_symbol_kind Kind
getprotected

The kind of the symbol (int or string)

Definition at line 35 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().

Microsoft.Z3.Symbol.IsIntSymbol
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Definition: Symbol.cs:42
Microsoft.Z3.Symbol.Symbol
Symbol(Context ctx, IntPtr obj)
Symbol constructor
Definition: Symbol.cs:116
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:115
Microsoft.Z3.Symbol.IsStringSymbol
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Definition: Symbol.cs:50
Microsoft.Z3.Symbol.Kind
Z3_symbol_kind Kind
The kind of the symbol (int or string)
Definition: Symbol.cs:35