Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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
 
bool IsStringSymbol ()
 Indicates whether the symbol is of string kind.
 
override string ToString ()
 A string representation of the symbol.
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object.
 

Protected Member Functions

 Symbol (Context ctx, IntPtr obj)
 Symbol constructor
 

Properties

Z3_symbol_kind Kind [get]
 The kind of the symbol (int or string)
 

Detailed Description

Symbols are used to name several term and type constructors.

Definition at line 30 of file Symbol.cs.

Constructor & Destructor Documentation

Symbol ( Context  ctx,
IntPtr  obj 
)
inlineprotected

Symbol constructor

Definition at line 73 of file Symbol.cs.

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

Member Function Documentation

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

Z3_symbol_kind Kind
getprotected

The kind of the symbol (int or string)

Definition at line 36 of file Symbol.cs.