Z3
FiniteDomainNum.cs
Go to the documentation of this file.
1 /*++
2 Copyright (<c>) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  FiniteDomainNum.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Finite-domain Numerals
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2015-12-02
15 
16 Notes:
17 
18 --*/
19 using System;
21 
22 #if !FRAMEWORK_LT_4
23 using System.Numerics;
24 #endif
25 
26 namespace Microsoft.Z3
27 {
31  [ContractVerification(true)]
33  {
37  public UInt64 UInt64
38  {
39  get
40  {
41  UInt64 res = 0;
42  if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
43  throw new Z3Exception("Numeral is not a 64 bit unsigned");
44  return res;
45  }
46  }
47 
51  public int Int
52  {
53  get
54  {
55  int res = 0;
56  if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
57  throw new Z3Exception("Numeral is not an int");
58  return res;
59  }
60  }
61 
65  public Int64 Int64
66  {
67  get
68  {
69  Int64 res = 0;
70  if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
71  throw new Z3Exception("Numeral is not an int64");
72  return res;
73  }
74  }
75 
79  public uint UInt
80  {
81  get
82  {
83  uint res = 0;
84  if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
85  throw new Z3Exception("Numeral is not a uint");
86  return res;
87  }
88  }
89 
90 #if !FRAMEWORK_LT_4
91  public BigInteger BigInteger
95  {
96  get
97  {
98  return BigInteger.Parse(this.ToString());
99  }
100  }
101 #endif
102 
106  public override string ToString()
107  {
108  return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
109  }
110 
111  #region Internal
112  internal FiniteDomainNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
113  #endregion
114  }
115 }
Finite-domain numerals
override string ToString()
Returns a string representation of the numeral.
def Int(name, ctx=None)
Definition: z3py.py:2808
Finite-domain expressions
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:30