19using System.Diagnostics;
54 if (Native.Z3_fpa_get_numeral_sign(
Context.nCtx, NativeObject, ref res) == 0)
55 throw new Z3Exception(
"Sign is not a Boolean value");
71 return Native.Z3_fpa_get_numeral_significand_string(
Context.nCtx, NativeObject);
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");
113 return Native.Z3_fpa_get_numeral_exponent_string(
Context.nCtx, NativeObject, (
byte)(biased ? 1 : 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");
135 return new BitVecExpr(
Context, Native.Z3_fpa_get_numeral_exponent_bv(
Context.nCtx, NativeObject, (
byte)(biased ? 1 : 0)));
141 public bool IsNaN {
get {
return Native.Z3_fpa_is_numeral_nan(
Context.nCtx, NativeObject) != 0; } }
146 public bool IsInf {
get {
return Native.Z3_fpa_is_numeral_inf(
Context.nCtx, NativeObject) != 0; } }
151 public bool IsZero{
get {
return Native.Z3_fpa_is_numeral_zero(
Context.nCtx, NativeObject) != 0; } }
156 public bool IsNormal {
get {
return Native.Z3_fpa_is_numeral_normal(
Context.nCtx, NativeObject) != 0; } }
161 public bool IsSubnormal {
get {
return Native.Z3_fpa_is_numeral_subnormal(
Context.nCtx, NativeObject) != 0; } }
166 public bool IsPositive {
get {
return Native.Z3_fpa_is_numeral_positive(
Context.nCtx, NativeObject) != 0; } }
171 public bool IsNegative {
get {
return Native.Z3_fpa_is_numeral_negative(
Context.nCtx, NativeObject) != 0; } }
177 Debug.Assert(ctx !=
null);
186 return Native.Z3_get_numeral_string(
Context.nCtx, NativeObject);
The main interaction with Z3 happens via the Context.
FloatingPoint Expressions
Int64 ExponentInt64(bool biased=true)
Return the exponent value of a floating-point numeral as a signed 64-bit integer
bool IsInf
Indicates whether the numeral is a +oo or -oo.
BitVecExpr SignBV
The sign of a floating-point numeral as a bit-vector expression
bool IsNegative
Indicates whether the numeral is negative.
bool IsNaN
Indicates whether the numeral is a NaN.
string Significand
The significand value of a floating-point numeral as a string
BitVecExpr SignificandBV
The significand of a floating-point numeral as a bit-vector expression
override string ToString()
Returns a string representation of the numeral.
bool IsPositive
Indicates whether the numeral is positive.
UInt64 SignificandUInt64
The significand value of a floating-point numeral as a UInt64
BitVecExpr ExponentBV(bool biased=true)
The exponent of a floating-point numeral as a bit-vector expression
bool Sign
Retrieves the sign of a floating-point literal
string Exponent(bool biased=true)
Return the (biased) exponent value of a floating-point numeral as a string
bool IsSubnormal
Indicates whether the numeral is subnormal.
bool IsZero
Indicates whether the numeral is +zero or -zero.
bool IsNormal
Indicates whether the numeral is normal.
The exception base class for error reporting from Z3