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 Symbol'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...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object 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.

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

Referenced by Symbol.Equals().

Member Function Documentation

Equals()

override bool Equals ( object  o )

inline

Object comparison.

Definition at line 92 of file Symbol.cs.

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

GetHashCode()

override int GetHashCode ( )

inline

The Symbol's hash code.

Returns

A hash code

Definition at line 103 of file Symbol.cs.

        {
            if (IsIntSymbol())
                return ((IntSymbol)this).Int;
            else 
                return ((StringSymbol)this).String.GetHashCode();
        }

IsIntSymbol()

bool IsIntSymbol ( )

inline

Indicates whether the symbol is of Int kind

Definition at line 42 of file Symbol.cs.

        {
            return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
        }

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.

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

        {
            return !(s1 == s2);
        }

operator==()

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

inlinestatic

Equality overloading.

Definition at line 72 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 58 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 34 of file Symbol.cs.

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

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