Z3
FPNum.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6  FPNum.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Floating Point Numerals
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2013-06-10
15 
16 Notes:
17 
18 --*/
19 using System;
21 
22 namespace Microsoft.Z3
23 {
27  [ContractVerification(true)]
28  public class FPNum : FPExpr
29  {
36  public bool Sign
37  {
38  get
39  {
40  int res = 0;
41  if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
42  throw new Z3Exception("Sign is not a Boolean value");
43  return res != 0;
44  }
45  }
46 
54  public string Significand
55  {
56  get
57  {
58  return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject);
59  }
60  }
61 
70  public UInt64 SignificandUInt64
71  {
72  get
73  {
74  UInt64 result = 0;
75  if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
76  throw new Z3Exception("Significand is not a 64 bit unsigned integer");
77  return result;
78  }
79  }
80 
84  public string Exponent
85  {
86  get
87  {
88  return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
89  }
90  }
91 
95  public Int64 ExponentInt64
96  {
97  get
98  {
99  Int64 result = 0;
100  if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0)
101  throw new Z3Exception("Exponent is not a 64 bit integer");
102  return result;
103  }
104  }
105 
106  #region Internal
107  internal FPNum(Context ctx, IntPtr obj)
108  : base(ctx, obj)
109  {
110  Contract.Requires(ctx != null);
111  }
112  #endregion
113 
117  public override string ToString()
118  {
119  return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
120  }
121  }
122 }
FloatiungPoint Numerals
Definition: FPNum.cs:28
override string ToString()
Returns a string representation of the numeral.
Definition: FPNum.cs:117
FloatingPoint Expressions
Definition: FPExpr.cs:31
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