Z3 |

IntNum.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 IntNum.cs
7
8 Abstract:
9
10 Z3 Managed API: Int Numerals
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-20
15
16 Notes:
17
18--*/
19 using System.Diagnostics;
20 using System;
21
22#if !FRAMEWORK_LT_4
23 using System.Numerics;
24#endif
25
26 namespace Microsoft.Z3
27{
31 public class IntNum : IntExpr
32 {
33
34 #region Internal
35 internal IntNum(Context ctx, IntPtr obj)
36 : base(ctx, obj)
37 {
38 Debug.Assert(ctx != null);
39 }
40 #endregion
41
42
46 public UInt64 UInt64
47 {
48 get
49 {
50 UInt64 res = 0;
51 if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
52 throw new Z3Exception("Numeral is not a 64 bit unsigned");
53 return res;
54 }
55 }
56
60 public int Int
61 {
62 get
63 {
64 int res = 0;
65 if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
66 throw new Z3Exception("Numeral is not an int");
67 return res;
68 }
69 }
70
74 public Int64 Int64
75 {
76 get
77 {
78 Int64 res = 0;
79 if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
80 throw new Z3Exception("Numeral is not an int64");
81 return res;
82 }
83 }
84
88 public uint UInt
89 {
90 get
91 {
92 uint res = 0;
93 if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
94 throw new Z3Exception("Numeral is not a uint");
95 return res;
96 }
97 }
98
99#if !FRAMEWORK_LT_4
103 public BigInteger BigInteger
104 {
105 get
106 {
107 return BigInteger.Parse(this.ToString());
108 }
109 }
110#endif
111
115 public override string ToString()
116 {
117 return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
118 }
119 }
120}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.IntExpr
Int expressions
Definition: IntExpr.cs:32
Microsoft.Z3.IntNum
Integer Numerals
Definition: IntNum.cs:32
Microsoft.Z3.IntNum.BigInteger
BigInteger BigInteger
Retrieve the BigInteger value.
Definition: IntNum.cs:104
Microsoft.Z3.IntNum.UInt
uint UInt
Retrieve the int value.
Definition: IntNum.cs:89
Microsoft.Z3.IntNum.UInt64
UInt64 UInt64
Retrieve the 64-bit unsigned integer value.
Definition: IntNum.cs:47
Microsoft.Z3.IntNum.Int64
Int64 Int64
Retrieve the 64-bit int value.
Definition: IntNum.cs:75
Microsoft.Z3.IntNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition: IntNum.cs:115
Microsoft.Z3.IntNum.Int
int Int
Retrieve the int value.
Definition: IntNum.cs:61
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Microsoft.Z3
Definition: AlgebraicNum.cs:27