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.Diagnostics;
20 using System;
21
22 namespace Microsoft.Z3
23{
27 public class FPNum : FPExpr
28 {
35 public BitVecExpr SignBV
36 {
37 get
38 {
39 return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject));
40 }
41 }
42
49 public bool Sign
50 {
51 get
52 {
53 int res = 0;
54 if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
55 throw new Z3Exception("Sign is not a Boolean value");
56 return res != 0;
57 }
58 }
59
67 public string Significand
68 {
69 get
70 {
71 return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject);
72 }
73 }
74
83 public UInt64 SignificandUInt64
84 {
85 get
86 {
87 UInt64 result = 0;
88 if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
89 throw new Z3Exception("Significand is not a 64 bit unsigned integer");
90 return result;
91 }
92 }
93
100 public BitVecExpr SignificandBV
101 {
102 get
103 {
104 return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject));
105 }
106 }
107
111 public string Exponent(bool biased = true)
112 {
113 return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0));
114 }
115
119 public Int64 ExponentInt64(bool biased = true)
120 {
121 Int64 result = 0;
122 if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, (byte)(biased? 1 : 0)) == 0)
123 throw new Z3Exception("Exponent is not a 64 bit integer");
124 return result;
125 }
126
133 public BitVecExpr ExponentBV(bool biased = true)
134 {
135 return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0)));
136 }
137
141 public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } }
142
146 public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } }
147
151 public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } }
152
156 public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } }
157
161 public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } }
162
166 public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
167
171 public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
172
173 #region Internal
174 internal FPNum(Context ctx, IntPtr obj)
175 : base(ctx, obj)
176 {
177 Debug.Assert(ctx != null);
178 }
179 #endregion
180
184 public override string ToString()
185 {
186 return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
187 }
188 }
189}
Microsoft.Z3.BitVecExpr
Bit-vector expressions
Definition: BitVecExpr.cs:32
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.FPExpr
FloatingPoint Expressions
Definition: FPExpr.cs:32
Microsoft.Z3.FPNum
FloatiungPoint Numerals
Definition: FPNum.cs:28
Microsoft.Z3.FPNum.ExponentInt64
Int64 ExponentInt64(bool biased=true)
Return the exponent value of a floating-point numeral as a signed 64-bit integer
Definition: FPNum.cs:119
Microsoft.Z3.FPNum.IsInf
bool IsInf
Indicates whether the numeral is a +oo or -oo.
Definition: FPNum.cs:146
Microsoft.Z3.FPNum.SignBV
BitVecExpr SignBV
The sign of a floating-point numeral as a bit-vector expression
Definition: FPNum.cs:36
Microsoft.Z3.FPNum.IsNegative
bool IsNegative
Indicates whether the numeral is negative.
Definition: FPNum.cs:171
Microsoft.Z3.FPNum.IsNaN
bool IsNaN
Indicates whether the numeral is a NaN.
Definition: FPNum.cs:141
Microsoft.Z3.FPNum.Significand
string Significand
The significand value of a floating-point numeral as a string
Definition: FPNum.cs:68
Microsoft.Z3.FPNum.SignificandBV
BitVecExpr SignificandBV
The significand of a floating-point numeral as a bit-vector expression
Definition: FPNum.cs:101
Microsoft.Z3.FPNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition: FPNum.cs:184
Microsoft.Z3.FPNum.IsPositive
bool IsPositive
Indicates whether the numeral is positive.
Definition: FPNum.cs:166
Microsoft.Z3.FPNum.SignificandUInt64
UInt64 SignificandUInt64
The significand value of a floating-point numeral as a UInt64
Definition: FPNum.cs:84
Microsoft.Z3.FPNum.ExponentBV
BitVecExpr ExponentBV(bool biased=true)
The exponent of a floating-point numeral as a bit-vector expression
Definition: FPNum.cs:133
Microsoft.Z3.FPNum.Sign
bool Sign
Retrieves the sign of a floating-point literal
Definition: FPNum.cs:50
Microsoft.Z3.FPNum.Exponent
string Exponent(bool biased=true)
Return the (biased) exponent value of a floating-point numeral as a string
Definition: FPNum.cs:111
Microsoft.Z3.FPNum.IsSubnormal
bool IsSubnormal
Indicates whether the numeral is subnormal.
Definition: FPNum.cs:161
Microsoft.Z3.FPNum.IsZero
bool IsZero
Indicates whether the numeral is +zero or -zero.
Definition: FPNum.cs:151
Microsoft.Z3.FPNum.IsNormal
bool IsNormal
Indicates whether the numeral is normal.
Definition: FPNum.cs:156
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Microsoft.Z3
Definition: AlgebraicNum.cs:27