Z3
FiniteDomainNum.cs
Go to the documentation of this file.
1/*++
2Copyright (<c>) 2012 Microsoft Corporation
3
4Module Name:
5
6 FiniteDomainNum.cs
7
8Abstract:
9
10 Z3 Managed API: Finite-domain Numerals
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2015-12-02
15
16Notes:
17
18--*/
19using System.Diagnostics;
20using System;
21
22#if !FRAMEWORK_LT_4
23using System.Numerics;
24#endif
25
26namespace Microsoft.Z3
27{
32 {
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
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
110 #region Internal
111 internal FiniteDomainNum(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
112 #endregion
113 }
114}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Finite-domain expressions
Finite-domain numerals
BigInteger BigInteger
Retrieve the BigInteger value.
uint UInt
Retrieve the int value.
UInt64 UInt64
Retrieve the 64-bit unsigned integer value.
Int64 Int64
Retrieve the 64-bit int value.
override string ToString()
Returns a string representation of the numeral.
int Int
Retrieve the int value.
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32