Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Runtime.InteropServices;
00022 using System.Diagnostics.Contracts;
00023
00024 namespace Microsoft.Z3
00025 {
00029 [ContractVerification(true)]
00030 public class Symbol : Z3Object
00031 {
00035 protected Z3_symbol_kind Kind
00036 {
00037 get { return (Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, NativeObject); }
00038 }
00039
00043 public bool IsIntSymbol()
00044 {
00045 return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
00046 }
00047
00051 public bool IsStringSymbol()
00052 {
00053 return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
00054 }
00055
00059 public override string ToString()
00060 {
00061 if (IsIntSymbol())
00062 return ((IntSymbol)this).Int.ToString();
00063 else if (IsStringSymbol())
00064 return ((StringSymbol)this).String;
00065 else
00066 throw new Z3Exception("Unknown symbol kind encountered");
00067 }
00068
00069 #region Internal
00070
00071
00072
00073 internal protected Symbol(Context ctx, IntPtr obj) : base(ctx, obj)
00074 {
00075 Contract.Requires(ctx != null);
00076 }
00077
00078 internal static Symbol Create(Context ctx, IntPtr obj)
00079 {
00080 Contract.Requires(ctx != null);
00081 Contract.Ensures(Contract.Result<Symbol>() != null);
00082
00083 switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
00084 {
00085 case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
00086 case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
00087 default:
00088 throw new Z3Exception("Unknown symbol kind encountered");
00089 }
00090 }
00091 #endregion
00092 }
00093 }