Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Symbol.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Symbol.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Symbols
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-16
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Runtime.InteropServices;
22 using System.Diagnostics.Contracts;
23 
24 namespace Microsoft.Z3
25 {
29  [ContractVerification(true)]
30  public class Symbol : Z3Object
31  {
35  protected Z3_symbol_kind Kind
36  {
37  get { return (Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, NativeObject); }
38  }
39 
43  public bool IsIntSymbol()
44  {
45  return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
46  }
47 
51  public bool IsStringSymbol()
52  {
53  return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
54  }
55 
59  public override string ToString()
60  {
61  if (IsIntSymbol())
62  return ((IntSymbol)this).Int.ToString();
63  else if (IsStringSymbol())
64  return ((StringSymbol)this).String;
65  else
66  throw new Z3Exception("Unknown symbol kind encountered");
67  }
68 
69  #region Internal
70 
71 
72 
73  internal protected Symbol(Context ctx, IntPtr obj) : base(ctx, obj)
74  {
75  Contract.Requires(ctx != null);
76  }
77 
78  internal static Symbol Create(Context ctx, IntPtr obj)
79  {
80  Contract.Requires(ctx != null);
81  Contract.Ensures(Contract.Result<Symbol>() != null);
82 
83  switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
84  {
85  case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
86  case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
87  default:
88  throw new Z3Exception("Unknown symbol kind encountered");
89  }
90  }
91  #endregion
92  }
93 
97  [ContractVerification(true)]
98  public class IntSymbol : Symbol
99  {
104  public int Int
105  {
106  get
107  {
108  if (!IsIntSymbol())
109  throw new Z3Exception("Int requested from non-Int symbol");
110  return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
111  }
112  }
113 
114  #region Internal
115  internal IntSymbol(Context ctx, IntPtr obj)
116  : base(ctx, obj)
117  {
118  Contract.Requires(ctx != null);
119  }
120  internal IntSymbol(Context ctx, int i)
121  : base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
122  {
123  Contract.Requires(ctx != null);
124  }
125 
126  #if DEBUG
127  internal override void CheckNativeObject(IntPtr obj)
128  {
129  if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
130  throw new Z3Exception("Symbol is not of integer kind");
131  base.CheckNativeObject(obj);
132  }
133  #endif
134  #endregion
135  }
136 
140  [ContractVerification(true)]
141  public class StringSymbol : Symbol
142  {
147  public string String
148  {
149  get
150  {
151  Contract.Ensures(Contract.Result<string>() != null);
152 
153  if (!IsStringSymbol())
154  throw new Z3Exception("String requested from non-String symbol");
155  return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);
156  }
157  }
158 
159  #region Internal
160  internal StringSymbol(Context ctx, IntPtr obj) : base(ctx, obj)
161  {
162  Contract.Requires(ctx != null);
163  }
164 
165  internal StringSymbol(Context ctx, string s) : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s))
166  {
167  Contract.Requires(ctx != null);
168  }
169 
170  #if DEBUG
171  internal override void CheckNativeObject(IntPtr obj)
172  {
173  if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
174  throw new Z3Exception("Symbol is not of string kind");
175 
176  base.CheckNativeObject(obj);
177  }
178  #endif
179  #endregion
180  }
181 }