21 using System.Runtime.InteropServices;
22 using System.Diagnostics.Contracts;
29 [ContractVerification(
true)]
62 return ((IntSymbol)
this).Int.ToString();
63 else if (IsStringSymbol())
64 return ((StringSymbol)
this).String;
66 throw new Z3Exception(
"Unknown symbol kind encountered");
70 internal protected Symbol(
Context ctx, IntPtr obj) : base(ctx, obj)
75 Contract.Requires(ctx != null);
78 internal static Symbol Create(Context ctx, IntPtr obj)
80 Contract.Requires(ctx != null);
81 Contract.Ensures(Contract.Result<Symbol>() != null);
86 case Z3_symbol_kind.Z3_STRING_SYMBOL:
return new StringSymbol(ctx, obj);
88 throw new Z3Exception(
"Unknown symbol kind encountered");
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
override string ToString()
A string representation of the symbol.
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Z3_symbol_kind
Z3_symbol_kind
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Symbols are used to name several term and type constructors.