Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Numeral.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Numeral.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Numerals
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-20
15 
16 Notes:
17 
18 --*/
19 using System;
20 using System.Diagnostics.Contracts;
21 
22 #if !FRAMEWORK_LT_4
23 using System.Numerics;
24 #endif
25 
26 namespace Microsoft.Z3
27 {
31  [ContractVerification(true)]
32  public class IntNum : IntExpr
33  {
34 
35  #region Internal
36  internal IntNum(Context ctx, IntPtr obj)
37  : base(ctx, obj)
38  {
39  Contract.Requires(ctx != null);
40  }
41  #endregion
42 
43 
47  public UInt64 UInt64
48  {
49  get
50  {
51  UInt64 res = 0;
52  if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
53  throw new Z3Exception("Numeral is not a 64 bit unsigned");
54  return res;
55  }
56  }
57 
61  public int Int
62  {
63  get
64  {
65  int res = 0;
66  if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
67  throw new Z3Exception("Numeral is not an int");
68  return res;
69  }
70  }
71 
75  public Int64 Int64
76  {
77  get
78  {
79  Int64 res = 0;
80  if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
81  throw new Z3Exception("Numeral is not an int64");
82  return res;
83  }
84  }
85 
89  public uint UInt
90  {
91  get
92  {
93  uint res = 0;
94  if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
95  throw new Z3Exception("Numeral is not a uint");
96  return res;
97  }
98  }
99 
100 #if !FRAMEWORK_LT_4
101 
102 
103 
104  public BigInteger BigInteger
105  {
106  get
107  {
108  return BigInteger.Parse(this.ToString());
109  }
110  }
111 #endif
112 
116  public override string ToString()
117  {
118  return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
119  }
120  }
121 
125  [ContractVerification(true)]
126  public class RatNum : RealExpr
127  {
131  public IntNum Numerator
132  {
133  get {
134  Contract.Ensures(Contract.Result<IntNum>() != null);
135 
136  return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject)); }
137  }
138 
142  public IntNum Denominator
143  {
144  get {
145  Contract.Ensures(Contract.Result<IntNum>() != null);
146 
147  return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject)); }
148  }
149 
150 #if !FRAMEWORK_LT_4
151 
152 
153 
154  public BigInteger BigIntNumerator
155  {
156  get
157  {
158  IntNum n = Numerator;
159  return BigInteger.Parse(n.ToString());
160  }
161  }
162 
166  public BigInteger BigIntDenominator
167  {
168  get
169  {
170  IntNum n = Denominator;
171  return BigInteger.Parse(n.ToString());
172  }
173  }
174 #endif
175 
180  public string ToDecimalString(uint precision)
181  {
182  return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
183  }
184 
188  public override string ToString()
189  {
190  return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
191  }
192 
193  #region Internal
194  internal RatNum(Context ctx, IntPtr obj)
195  : base(ctx, obj)
196  {
197  Contract.Requires(ctx != null);
198  }
199  #endregion
200  }
201 
202 
206  [ContractVerification(true)]
207  public class BitVecNum : BitVecExpr
208  {
212  public UInt64 UInt64
213  {
214  get
215  {
216  UInt64 res = 0;
217  if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
218  throw new Z3Exception("Numeral is not a 64 bit unsigned");
219  return res;
220  }
221  }
222 
226  public int Int
227  {
228  get
229  {
230  int res = 0;
231  if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
232  throw new Z3Exception("Numeral is not an int");
233  return res;
234  }
235  }
236 
240  public Int64 Int64
241  {
242  get
243  {
244  Int64 res = 0;
245  if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
246  throw new Z3Exception("Numeral is not an int64");
247  return res;
248  }
249  }
250 
254  public uint UInt
255  {
256  get
257  {
258  uint res = 0;
259  if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
260  throw new Z3Exception("Numeral is not a uint");
261  return res;
262  }
263  }
264 
265 #if !FRAMEWORK_LT_4
266 
267 
268 
269  public BigInteger BigInteger
270  {
271  get
272  {
273  return BigInteger.Parse(this.ToString());
274  }
275  }
276 #endif
277 
281  public override string ToString()
282  {
283  return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
284  }
285 
286  #region Internal
287  internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
288  #endregion
289  }
290 
294  [ContractVerification(true)]
295  public class AlgebraicNum : ArithExpr
296  {
304  public RatNum ToUpper(uint precision)
305  {
306  Contract.Ensures(Contract.Result<RatNum>() != null);
307 
308  return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
309  }
310 
318  public RatNum ToLower(uint precision)
319  {
320  Contract.Ensures(Contract.Result<RatNum>() != null);
321 
322  return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
323  }
324 
329  public string ToDecimal(uint precision)
330  {
331  Contract.Ensures(Contract.Result<string>() != null);
332 
333  return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
334  }
335 
336  #region Internal
337  internal AlgebraicNum(Context ctx, IntPtr obj)
338  : base(ctx, obj)
339  {
340  Contract.Requires(ctx != null);
341  }
342  #endregion
343  }
344 }