Z3
src/api/dotnet/Symbol.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Symbol.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Symbols
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-16
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines