Z3
BitVecNum.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;
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 BitVecNum : BitVecExpr
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 BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
113  #endregion
114  }
115 }
override string ToString()
Returns a string representation of the numeral.
Definition: BitVecNum.cs:106
using System
static int Z3_get_numeral_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2)
Definition: Native.cs:3702
Bit-vector numerals
Definition: BitVecNum.cs:32
static string Z3_get_numeral_string(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3638
static int Z3_get_numeral_uint64(Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2)
Definition: Native.cs:3694
def Int(name, ctx=None)
Definition: z3py.py:2742
Bit-vector expressions
Definition: BitVecExpr.cs:31
static int Z3_get_numeral_uint(Z3_context a0, Z3_ast a1, [In, Out] ref uint a2)
Definition: Native.cs:3686
static int Z3_get_numeral_int(Z3_context a0, Z3_ast a1, [In, Out] ref int a2)
Definition: Native.cs:3678
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27