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 30 of file Symbol.cs.

Constructor & Destructor Documentation

§ Symbol()

Symbol ( Context  ctx,
IntPtr  obj 
)
inlineprotected

Symbol constructor

Definition at line 114 of file Symbol.cs.

114  : base(ctx, obj)
115  {
116  Contract.Requires(ctx != null);
117  }

Member Function Documentation

§ Equals()

override bool Equals ( object  o)
inline

Object comparison.

Definition at line 93 of file Symbol.cs.

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

§ GetHashCode()

override int GetHashCode ( )
inline

The Symbols's hash code.

Returns
A hash code

Definition at line 104 of file Symbol.cs.

105  {
106  return (int)NativeObject;
107  }

§ IsIntSymbol()

bool IsIntSymbol ( )
inline

Indicates whether the symbol is of Int kind

Definition at line 43 of file Symbol.cs.

44  {
45  return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
46  }
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:119
Z3_symbol_kind Kind
The kind of the symbol (int or string)
Definition: Symbol.cs:36

§ IsStringSymbol()

bool IsStringSymbol ( )
inline

Indicates whether the symbol is of string kind.

Definition at line 51 of file Symbol.cs.

52  {
53  return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
54  }
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:119
Z3_symbol_kind Kind
The kind of the symbol (int or string)
Definition: Symbol.cs:36

§ operator!=()

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

Equality overloading.

Definition at line 85 of file Symbol.cs.

86  {
87  return !(s1.NativeObject == s2.NativeObject);
88  }

§ operator==()

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

Equality overloading.

Definition at line 73 of file Symbol.cs.

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

§ ToString()

override string ToString ( )
inline

A string representation of the symbol.

Definition at line 59 of file Symbol.cs.

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

Property Documentation

§ Kind

Z3_symbol_kind Kind
getprotected

The kind of the symbol (int or string)

Definition at line 36 of file Symbol.cs.