Z3 |

BitVecNum.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 BitVecNum.cs
7
8 Abstract:
9
10 Z3 Managed API: BitVec 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 BitVecNum : BitVecExpr
32 {
36 public UInt64 UInt64
37 {
38 get
39 {
40 UInt64 res = 0;
41 if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
42 throw new Z3Exception("Numeral is not a 64 bit unsigned");
43 return res;
44 }
45 }
46
50 public int Int
51 {
52 get
53 {
54 int res = 0;
55 if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
56 throw new Z3Exception("Numeral is not an int");
57 return res;
58 }
59 }
60
64 public Int64 Int64
65 {
66 get
67 {
68 Int64 res = 0;
69 if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
70 throw new Z3Exception("Numeral is not an int64");
71 return res;
72 }
73 }
74
78 public uint UInt
79 {
80 get
81 {
82 uint res = 0;
83 if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
84 throw new Z3Exception("Numeral is not a uint");
85 return res;
86 }
87 }
88
89#if !FRAMEWORK_LT_4
93 public BigInteger BigInteger
94 {
95 get
96 {
97 return BigInteger.Parse(this.ToString());
98 }
99 }
100#endif
101
105 public override string ToString()
106 {
107 return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
108 }
109
113 public string ToBinaryString()
114 {
115 return Native.Z3_get_numeral_binary_string(Context.nCtx, NativeObject);
116 }
117
118 #region Internal
119 internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
120 #endregion
121 }
122}
Microsoft.Z3.BitVecExpr
Bit-vector expressions
Definition: BitVecExpr.cs:32
Microsoft.Z3.BitVecNum
Bit-vector numerals
Definition: BitVecNum.cs:32
Microsoft.Z3.BitVecNum.ToBinaryString
string ToBinaryString()
Returns a binary string representation of the numeral.
Definition: BitVecNum.cs:113
Microsoft.Z3.BitVecNum.BigInteger
BigInteger BigInteger
Retrieve the BigInteger value.
Definition: BitVecNum.cs:94
Microsoft.Z3.BitVecNum.UInt
uint UInt
Retrieve the int value.
Definition: BitVecNum.cs:79
Microsoft.Z3.BitVecNum.UInt64
UInt64 UInt64
Retrieve the 64-bit unsigned integer value.
Definition: BitVecNum.cs:37
Microsoft.Z3.BitVecNum.Int64
Int64 Int64
Retrieve the 64-bit int value.
Definition: BitVecNum.cs:65
Microsoft.Z3.BitVecNum.ToString
override string ToString()
Returns a decimal string representation of the numeral.
Definition: BitVecNum.cs:105
Microsoft.Z3.BitVecNum.Int
int Int
Retrieve the int value.
Definition: BitVecNum.cs:51
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Microsoft.Z3
Definition: AlgebraicNum.cs:27