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
internal	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()

internal Symbol ( Context  ctx, IntPtr  obj  )

inlineprotected

Symbol constructor

Definition at line 114 of file Symbol.cs.

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

Referenced by Symbol.Equals().

Member Function Documentation

Equals()

override bool Equals ( object  o )

inline

Object comparison.

Definition at line 93 of file Symbol.cs.

        {
            Symbol casted = o as Symbol;
            if (casted == null) return false;
            return this == casted;
        }

GetHashCode()

override int GetHashCode ( )

inline

The Symbols's hash code.

Returns

A hash code

Definition at line 104 of file Symbol.cs.

        {
            return (int)NativeObject;
        }

IsIntSymbol()

bool IsIntSymbol ( )

inline

Indicates whether the symbol is of Int kind

Definition at line 43 of file Symbol.cs.

        {
            return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
        }

Referenced by Symbol.ToString().

IsStringSymbol()

bool IsStringSymbol ( )

inline

Indicates whether the symbol is of string kind.

Definition at line 51 of file Symbol.cs.

        {
            return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
        }

Referenced by Symbol.ToString().

operator !=()

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

inlinestatic

Equality overloading.

Definition at line 85 of file Symbol.cs.

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

operator==()

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

inlinestatic

Equality overloading.

Definition at line 73 of file Symbol.cs.

        {
            
            return Object.ReferenceEquals(s1, s2) ||
                   (!Object.ReferenceEquals(s1, null) &&
                    !Object.ReferenceEquals(s2, null) &&
                    s1.NativeObject == s2.NativeObject);
        }

ToString()

override string ToString ( )

inline

A string representation of the symbol.

Definition at line 59 of file Symbol.cs.

        {
            if (IsIntSymbol())
                return ((IntSymbol)this).Int.ToString();
            else if (IsStringSymbol())
                return ((StringSymbol)this).String;
            else
                throw new Z3Exception("Unknown symbol kind encountered");
        }

Property Documentation

Kind

Z3_symbol_kind Kind

getprotected

The kind of the symbol (int or string)

Definition at line 36 of file Symbol.cs.

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

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