diff --git a/Source/AbstractInterpretation/IntervalDomain.cs b/Source/AbstractInterpretation/IntervalDomain.cs
index 5985b9a18..9ad818279 100644
--- a/Source/AbstractInterpretation/IntervalDomain.cs
+++ b/Source/AbstractInterpretation/IntervalDomain.cs
@@ -326,7 +326,7 @@ static Expr NumberToExpr(BigInteger n, Type ty)
}
else if (ty.IsFloat)
{
- return Expr.Literal(BaseTypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand));
+ return Expr.Literal(BaseTypes.BigFloat.FromBigInt(n, ty.FloatSignificand, ty.FloatExponent));
}
else
{
@@ -958,9 +958,19 @@ public override Expr VisitLiteralExpr(LiteralExpr node)
}
else if (node.Val is BigFloat)
{
- ((BigFloat) node.Val).FloorCeiling(out var floor, out var ceiling);
- Lo = floor;
- Hi = ceiling;
+ var bf = (BigFloat) node.Val;
+ if (bf.IsNaN || bf.IsInfinity)
+ {
+ // NaN and infinity have no meaningful integer bounds
+ Lo = null;
+ Hi = null;
+ }
+ else
+ {
+ bf.FloorCeiling(out var floor, out var ceiling);
+ Lo = floor;
+ Hi = ceiling;
+ }
}
else if (node.Val is bool)
{
diff --git a/Source/BaseTypes/BigFloat.cs b/Source/BaseTypes/BigFloat.cs
index 40db11b1d..df9fe709b 100644
--- a/Source/BaseTypes/BigFloat.cs
+++ b/Source/BaseTypes/BigFloat.cs
@@ -1,711 +1,1295 @@
-using System;
+using System;
using System.Diagnostics.Contracts;
-using System.Linq;
-using System.Text;
-using BIM = System.Numerics.BigInteger;
+using System.Numerics;
namespace Microsoft.BaseTypes
{
///
- /// A representation of a floating-point value
- /// Note that this value has a 1-bit sign, along with an exponent and significand whose sizes must be greater than 1
+ /// A representation of a floating-point value using IEEE 754-2019 format.
+ /// Note that this value has a 1-bit sign, along with an exponent and significand whose sizes must be greater than 1.
+ /// Uses IEEE 754-2019 representation internally with configurable significand and exponent sizes.
///
- public struct BigFloat
+ public readonly struct BigFloat
{
- //Please note that this code outline is copy-pasted from BigDec.cs
+ #region Fields and Properties
+
+ // IEEE 754 representation fields
+ private readonly BigInteger significand; // Trailing significand field (without leading bit for normal numbers)
+ private readonly BigInteger exponent; // Biased exponent value
+ private readonly bool signBit; // Sign bit: true = negative, false = positive
+
+ // Cached values for performance
+ private readonly BigInteger bias; // Exponent bias value
+ private readonly BigInteger maxExponent; // Maximum exponent value
+ private readonly BigInteger leadingBit; // Power value for the implicit leading significand bit
+
+ // SignificandSize represents the precision: trailing significand field width + 1 (for the implicit leading significand bit)
+ // For IEEE 754 double: SignificandSize = 53 (52-bit trailing significand field + 1 implicit leading significand bit)
+ // The trailing significand field always uses SignificandSize - 1 bits
+ public int SignificandSize { get; }
+ public int ExponentSize { get; } // Total bits for exponent
+ public bool IsZero => significand == 0 && exponent == 0;
+ public bool IsNaN => exponent == maxExponent && significand != 0;
+ public bool IsInfinity => exponent == maxExponent && significand == 0;
+ public bool IsSubnormal => exponent == 0 && significand != 0;
+ public bool IsNormal => exponent > 0 && exponent < maxExponent;
+ public bool IsNegative => signBit;
+ public bool IsPositive => !signBit;
+ public bool IsFinite => !IsNaN && !IsInfinity;
+
+ #endregion
+
+ // ============================================================================
+ // PUBLIC INTERFACE
+ // ============================================================================
+
+ #region Constructors and Factory Methods
- // the internal representation
- internal readonly BIM
- significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
-
- internal readonly int significandSize; //The bit size of the significand
- internal readonly BIM exponent; //The value of the exponent is always positive as per fp representation requirements
- internal readonly int exponentSize; //The bit size of the exponent
- internal readonly String value; //Only used with second syntax
- internal readonly bool isSignBitSet; //Stores the sign bit in the fp representaiton
-
- public int SignificandSize
+ ///
+ /// Initializes a new instance of the struct.
+ /// Primary constructor for IEEE 754 representation
+ ///
+ /// The sign bit: true for negative, false for positive
+ /// The trailing significand field (without implicit leading significand bit for normal numbers)
+ /// The biased exponent value
+ /// Total bits for significand (including implicit leading significand bit)
+ /// Total bits for exponent
+ public BigFloat(bool signBit, BigInteger significand, BigInteger exponent, int significandSize, int exponentSize)
+ : this(signBit, significand, exponent, significandSize, exponentSize, false)
{
- get { return significandSize; }
}
- public int ExponentSize
+ ///
+ /// Initializes a new instance of the struct.
+ /// Internal constructor with optional validation bypass
+ ///
+ private BigFloat(bool signBit, BigInteger significand, BigInteger exponent, int significandSize, int exponentSize, bool skipValidation)
{
- get { return exponentSize; }
- }
+ if (!skipValidation)
+ {
+ ValidateSizeParameters(significandSize, exponentSize);
+ if (significand < 0) {
+ throw new ArgumentException("Significand must be non-negative (IEEE 754 significands are unsigned)", nameof(significand));
+ }
+ if (exponent < 0) {
+ throw new ArgumentException("Exponent must be non-negative (biased representation)", nameof(exponent));
+ }
- public static BigFloat ZERO = new BigFloat(false, BIM.Zero, BIM.Zero, 24, 8); //Does not include negative zero
+ // IEEE 754: The trailing significand field width is significandSize - 1 bits
+ // For normal numbers, the leading bit of the significand is implicitly encoded in the biased exponent
+ if (significand.GetBitLength() > significandSize - 1) {
+ throw new ArgumentException($"Trailing significand field requires {significand.GetBitLength()} bits but only {significandSize - 1} bits are available", nameof(significand));
+ }
- ////////////////////////////////////////////////////////////////////////////
- // Constructors
+ if (exponent > GetMaxExponent(exponentSize)) {
+ throw new ArgumentException($"Exponent {exponent} exceeds maximum value {GetMaxExponent(exponentSize)} for {exponentSize}-bit exponent size", nameof(exponent));
+ }
+ }
- //Please note that these constructors will be called throughout boogie
- //For a complete summary of where this class has been added, simply view constructor references
+ this.signBit = signBit;
+ this.significand = significand;
+ this.exponent = exponent;
+ SignificandSize = significandSize;
+ ExponentSize = exponentSize;
+
+ // Initialize cached values
+ bias = GetBias(exponentSize);
+ maxExponent = GetMaxExponent(exponentSize);
+ leadingBit = GetLeadingBitPower(significandSize);
+ }
+ ///
+ /// Tries to parse a string representation of a BigFloat with IEEE 754 compliant behavior
+ ///
+ /// The string to parse in format: [-]0x^.^e*f*e* or 0NaN*e* or 0+/-oo*e*
+ /// The parsed BigFloat value if successful; default(BigFloat) otherwise
+ /// True if the parse was successful; false otherwise
[Pure]
- public static BigFloat FromInt(int v)
+ public static bool TryParse(string s, out BigFloat result)
{
- return new BigFloat(v.ToString(), 24, 8);
+ return TryParseFloatString(s, strict: false, out result);
}
- public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize)
+ ///
+ /// Tries to parse a string representation of a BigFloat with strict Boogie verification requirements.
+ /// This method enforces:
+ /// - No precision loss (significand must have trailing zeros for full nibble inclusion)
+ /// - No extreme underflow (rejects values that would underflow to zero)
+ /// - Strict size validation
+ ///
+ /// DESIGN NOTE: This "strict" mode is arguably overly restrictive. It rejects:
+ /// - ALL extreme underflow, even representable subnormals (e.g., 0x0.8e-126f24e8)
+ /// - ANY precision loss, even standard IEEE 754 rounding
+ ///
+ ///
+ /// The string to parse in format: [-]0x^.^e*f*e* or 0NaN*e* or 0+/-oo*e*
+ /// The parsed BigFloat value if successful; default(BigFloat) otherwise
+ /// True if the parse was successful; false otherwise
+ [Pure]
+ public static bool TryParseExact(string s, out BigFloat result)
{
- return new BigFloat(v.ToString(), significandSize, exponentSize);
+ return TryParseFloatString(s, strict: true, out result);
}
+ ///
+ /// Parses a string representation of a BigFloat with IEEE 754 compliant behavior
+ ///
+ /// The string to parse in format: [-]0x^.^e*f*e* or 0NaN*e* or 0+/-oo*e*
+ /// The parsed BigFloat value
[Pure]
- public static BigFloat FromString(String s)
+ public static BigFloat FromString(string s)
{
- /*
- * String must be either of the format [-]0x^.^e*f*e*
- * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e*
- * Where ^ indicates a hexadecimal value and * indicates an integer value
- */
-
- int posLastE = s.LastIndexOf('e');
-
- int expSize = int.Parse(s.Substring(posLastE + 1));
- if (expSize <= 1)
+ if (TryParse(s, out var result))
{
- throw new FormatException("Exponent size must be greater than 1");
+ return result;
}
+ throw new FormatException($"Unable to parse '{s}' as BigFloat");
+ }
- int posLastF = s.LastIndexOf('f');
- int posSig = posLastF + 1;
- if (posLastF == -1)
- {
- //NaN, +oo, -oo
- posSig = 4;
+ ///
+ /// Parses a string representation of a BigFloat with strict Boogie verification requirements.
+ /// This method enforces:
+ /// - No precision loss (significand must have trailing zeros for full nibble inclusion)
+ /// - No extreme underflow (rejects values that would underflow to zero)
+ /// - Strict size validation with FormatException
+ ///
+ /// DESIGN NOTE: This "strict" mode is arguably overly restrictive. It rejects:
+ /// - ALL extreme underflow, even representable subnormals (e.g., 0x0.8e-126f24e8)
+ /// - ANY precision loss, even standard IEEE 754 rounding
+ ///
+ ///
+ /// The string to parse in format: [-]0x^.^e*f*e* or 0NaN*e* or 0+/-oo*e*
+ /// The parsed BigFloat value
+ [Pure]
+ public static BigFloat FromStringStrict(string s)
+ {
+ if (TryParseExact(s, out var result)) {
+ return result;
}
+ throw new FormatException($"Unable to parse '{s}' as BigFloat in strict mode");
+ }
- int sigSize = int.Parse(s.Substring(posSig, posLastE - posSig));
- if (sigSize <= 1)
- {
- throw new FormatException("Significand size must be greater than 1");
- }
+ ///
+ /// Core parsing logic that handles both IEEE 754 compliant and Boogie strict parsing modes
+ ///
+ /// The string to parse
+ /// When true, enforces Boogie's verification requirements (no precision loss, no extreme underflow);
+ /// when false, follows IEEE 754 standard (allows graceful underflow and rounding)
+ /// The parsed BigFloat value if successful; default(BigFloat) otherwise
+ /// True if the parse was successful; false otherwise
+ private static bool TryParseFloatString(string s, bool strict, out BigFloat result)
+ {
+ result = default;
- if (posLastF == -1)
- {
- //NaN, +oo, -oo
- return new BigFloat(s.Substring(1, 3), sigSize, expSize);
+ if (string.IsNullOrEmpty(s)) {
+ return false;
}
- bool isSignBitSet = s[0] == '-';
-
- int posX = s.IndexOf('x');
- int posSecondLastE = s.LastIndexOf('e', posLastE - 1);
+ // Reject any leading or trailing whitespace
+ if (s != s.Trim()) {
+ return false;
+ }
- string hexSig = s.Substring(posX + 1, posSecondLastE - (posX + 1));
- BIM oldExp = BIM.Parse(s.Substring(posSecondLastE + 1, posLastF - (posSecondLastE + 1)));
+ // Parse size specifiers: f[sigSize]e[expSize]
+ var posLastE = s.LastIndexOf('e');
+ if (posLastE == -1) {
+ return false;
+ }
- string binSig = string.Join(string.Empty,
- hexSig.Select(
- c => (c == '.' ? "." : Convert.ToString(Convert.ToInt32(c.ToString(), 16), 2).PadLeft(4, '0'))
- )
- );
+ var expSizeStr = s[(posLastE + 1)..];
- int posDec = binSig.IndexOf('.');
+ if (!int.TryParse(expSizeStr, out var exponentSize)) {
+ return false;
+ }
- binSig = binSig.Remove(posDec, 1);
+ // Extract significand size
+ var posLastF = s.LastIndexOf('f');
+ var sigSizeStart = posLastF == -1 ? 4 : posLastF + 1; // Special values start at 4, normal after 'f'
- int posFirstOne = binSig.IndexOf('1');
- int posLastOne = binSig.LastIndexOf('1');
+ var sigSizeStr = s[sigSizeStart..posLastE];
- if (posFirstOne == -1)
- {
- return new BigFloat(isSignBitSet, 0, 0, sigSize, expSize);
+ if (sigSizeStart >= posLastE ||
+ !int.TryParse(sigSizeStr, out var significandSize) ||
+ !(significandSize > 1 && exponentSize > 1)) {
+ return false;
}
- binSig = binSig.Substring(posFirstOne, posLastOne - posFirstOne + 1);
+ // Parse content: hex format or special value
+ return posLastF != -1 ?
+ TryParseHexFormat(s[..posLastF], significandSize, exponentSize, strict, out result) :
+ TryCreateSpecialFromString(s[1..4], significandSize, exponentSize, out result);
+ }
- BIM bias = BIM.Pow(2, expSize - 1) - 1;
- BIM upperBound = 2 * bias + 1;
+ ///
+ /// Creates a BigFloat from an integer value (default: double precision)
+ ///
+ [Pure] public static BigFloat FromInt(int v) => ConvertIntegerToBigFloat(v, 53, 11);
+ [Pure] public static BigFloat FromInt(int v, int significandSize, int exponentSize) => ConvertIntegerToBigFloat(v, significandSize, exponentSize);
+ public static BigFloat FromBigInt(BigInteger v, int significandSize, int exponentSize) => ConvertIntegerToBigFloat(v, significandSize, exponentSize);
- BIM newExp = 4 * oldExp + bias + (posDec - posFirstOne - 1);
+ ///
+ /// Converts a rational number to a BigFloat.
+ /// Returns false if the number cannot be accurately represented as a BigFloat.
+ ///
+ /// The numerator of the rational number
+ /// The denominator of the rational number
+ /// The size of the significand in bits
+ /// The size of the exponent in bits
+ /// The resulting BigFloat
+ /// True if the conversion is exact, false otherwise
+ [Pure]
+ public static bool FromRational(
+ BigInteger numerator,
+ BigInteger denominator,
+ int significandSize,
+ int exponentSize,
+ out BigFloat result)
+ {
+ ValidateSizeParameters(significandSize, exponentSize);
- if (newExp <= 0)
- {
- if (-newExp <= (sigSize - 1) - binSig.Length)
- {
- binSig = new string('0', (int)-newExp) + binSig;
- newExp = 0;
- }
- }
- else
- {
- binSig = binSig.Substring(1);
+ // Handle sign and zero
+ var isNegative = (numerator < 0) != (denominator < 0);
+ if (numerator.IsZero) {
+ result = CreateZero(isNegative, significandSize, exponentSize);
+ return true;
}
- if (newExp < 0 || newExp >= upperBound)
- {
- throw new FormatException("The given exponent cannot fit in the bit size " + expSize);
+ // Work with absolute values
+ numerator = BigInteger.Abs(numerator);
+ denominator = BigInteger.Abs(denominator);
+
+ // Scale numerator for precision
+ // Use long to avoid overflow in bit length calculation
+ var scaleBitsLong = (long)significandSize + 3 + (denominator.GetBitLength() - numerator.GetBitLength());
+ var scaleBits = scaleBitsLong < 0 ? BigInteger.Zero : new BigInteger(scaleBitsLong);
+ var scaledNumerator = BigIntegerMath.LeftShift(numerator, scaleBits);
+ var quotient = BigInteger.DivRem(scaledNumerator, denominator, out var remainder);
+
+ // Apply rounding if inexact
+ var isExact = remainder.IsZero;
+ if (!isExact) {
+ quotient = ApplyRoundToNearestEven(quotient, remainder, denominator);
}
- binSig = binSig.PadRight(sigSize - 1, '0');
+ var quotientBits = quotient.GetBitLength();
+ var biasedExp = GetBias(exponentSize) + quotientBits - scaleBits - 1;
+ if (biasedExp > GetMaxExponent(exponentSize) - 1) {
+ result = CreateInfinity(isNegative, significandSize, exponentSize);
+ return false;
+ }
+ var targetBits = significandSize - 1;
+ var minBiasedExp = 2 - significandSize;
+
+ if (biasedExp <= 0) {
+ if (biasedExp < minBiasedExp) {
+ isExact = false;
+
+ if (biasedExp == minBiasedExp - 1) {
+ if (quotient == BigIntegerMath.LeftShift(BigInteger.One, quotientBits - 1)) {
+ result = CreateZero(isNegative, significandSize, exponentSize);
+ } else {
+ var (boundaryShifted, _) = ApplyShiftWithRounding(quotient, BigInteger.One);
+ result = boundaryShifted > 0
+ ? new BigFloat(isNegative, 1, 0, significandSize, exponentSize)
+ : CreateZero(isNegative, significandSize, exponentSize);
+ }
+ } else {
+ result = CreateZero(isNegative, significandSize, exponentSize);
+ }
+ } else {
+ var shiftAmount = (quotientBits - targetBits) - biasedExp;
+ var (shifted, _) = ApplyShiftWithRounding(quotient, shiftAmount);
+
+ if (shifted >= BigInteger.One << targetBits) {
+ result = new BigFloat(isNegative, 0, 1, significandSize, exponentSize);
+ } else {
+ result = new BigFloat(isNegative, shifted, 0, significandSize, exponentSize);
+ }
+ }
+ } else {
+ var (normalShifted, wasExact) = ApplyShiftWithRounding(quotient, quotientBits - significandSize);
+ isExact &= wasExact;
- if (binSig.Length > sigSize - 1)
- {
- throw new FormatException("The given significand cannot fit in the bit size " + (sigSize - 1));
+ var leadingBitMask = GetLeadingBitPower(significandSize) - 1;
+ result = new BigFloat(isNegative, normalShifted & leadingBitMask, biasedExp, significandSize, exponentSize);
}
- BIM newSig = 0;
- foreach (char b in binSig)
- {
- if (b != '.')
- {
- newSig <<= 1;
- newSig += b - '0';
- }
+ return isExact;
+ }
+
+ ///
+ /// Converts a BigDec (decimal) value to a BigFloat.
+ /// Returns false if the number cannot be accurately represented as a BigFloat.
+ ///
+ /// The BigDec value to convert
+ /// The size of the significand in bits
+ /// The size of the exponent in bits
+ /// The resulting BigFloat
+ /// True if the conversion is exact, false otherwise
+ [Pure]
+ public static bool FromBigDec(
+ BigDec value,
+ int significandSize,
+ int exponentSize,
+ out BigFloat result)
+ {
+ BigInteger numerator, denominator;
+
+ if (value.Exponent >= 0) {
+ numerator = value.Mantissa * BigInteger.Pow(10, value.Exponent);
+ denominator = BigInteger.One;
+ } else {
+ numerator = value.Mantissa;
+ denominator = BigInteger.Pow(10, -value.Exponent);
}
- return new BigFloat(isSignBitSet, newSig, newExp, sigSize, expSize);
+ return FromRational(numerator, denominator, significandSize, exponentSize, out result);
}
- public BigFloat(bool isSignBitSet, BIM significand, BIM exponent, int significandSize, int exponentSize)
+ #endregion
+
+ #region Validation and Parameter Checking
+
+ ///
+ /// Validates that significand and exponent sizes meet minimum requirements (must be > 1)
+ ///
+ /// The size of the significand in bits
+ /// The size of the exponent in bits
+ private static void ValidateSizeParameters(int significandSize, int exponentSize)
{
- this.exponentSize = exponentSize;
- this.exponent = exponent;
- this.significand = significand;
- this.significandSize = significandSize;
- this.isSignBitSet = isSignBitSet;
- this.value = "";
+ if (significandSize <= 1) {
+ throw new ArgumentException($"Significand size must be greater than 1, got {significandSize}", nameof(significandSize));
+ }
+ if (exponentSize <= 1) {
+ throw new ArgumentException($"Exponent size must be greater than 1, got {exponentSize}", nameof(exponentSize));
+ }
}
- public BigFloat(String value, int significandSize, int exponentSize)
+ private static void ValidateSizeCompatibility(BigFloat x, BigFloat y)
{
- this.exponentSize = exponentSize;
- this.significandSize = significandSize;
- this.exponent = BIM.Zero;
- this.significand = BIM.Zero;
- this.value = value;
- if (value.Equals("nan"))
- {
- this.value = "NaN";
+ if (x.ExponentSize != y.ExponentSize) {
+ throw new ArgumentException($"Exponent sizes must match: {x.ExponentSize} != {y.ExponentSize}");
}
- this.isSignBitSet = value[0] == '-';
+ if (x.SignificandSize != y.SignificandSize) {
+ throw new ArgumentException($"Significand sizes must match: {x.SignificandSize} != {y.SignificandSize}");
+ }
}
- ////////////////////////////////////////////////////////////////////////////
- // Basic object operations
+ ///
+ /// Gets the mathematical exponent value (E for use in E - bias), handling subnormal numbers correctly
+ /// For subnormal numbers, returns 1 as per IEEE 754 specification
+ ///
+ private BigInteger GetActualExponent() => exponent == 0 ? BigInteger.One : exponent;
+
+ #endregion
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
+ #region Arithmetic Helpers
+
+ private static (BigInteger significand, BigInteger exponent) PrepareOperand(BigFloat operand, BigInteger leadingBit)
{
- if (obj == null)
- {
- return false;
+ var sig = operand.significand;
+ var exp = operand.GetActualExponent();
+ if (operand.exponent > 0) {
+ sig |= leadingBit;
}
+ return (sig, exp);
+ }
- if (!(obj is BigFloat))
- {
- return false;
+ ///
+ /// Prepares operands for multiplication/division operations (with combined sign calculation)
+ ///
+ private static ((BigInteger sig, BigInteger exp) x, (BigInteger sig, BigInteger exp) y, bool resultSign) PrepareOperandsForMultDiv(BigFloat x, BigFloat y)
+ {
+ var leadingBit = x.leadingBit;
+ var resultSign = x.signBit ^ y.signBit;
+ var (xSig, xExp) = PrepareOperand(x, leadingBit);
+ var (ySig, yExp) = PrepareOperand(y, leadingBit);
+
+ return ((xSig, xExp), (ySig, yExp), resultSign);
+ }
+
+ private static BigInteger ApplyRoundToNearestEven(BigInteger quotient, BigInteger remainder, BigInteger denominator)
+ {
+ // Round up if remainder > denominator/2, or if remainder == denominator/2 and quotient is odd
+ if (remainder * 2 > denominator || (remainder * 2 == denominator && !quotient.IsEven)) {
+ quotient++;
}
- return (this == (BigFloat) obj);
+ return quotient;
}
- [Pure]
- public override int GetHashCode()
+ private static BigInteger GetMask(BigInteger bits)
{
- return significand.GetHashCode() * 13 + exponent.GetHashCode();
+ if (bits <= 0) {
+ return BigInteger.Zero;
+ }
+ return BigIntegerMath.LeftShift(BigInteger.One, bits) - 1;
}
- [Pure]
- public override string ToString()
+ private static (BigInteger result, bool isExact) ApplyShiftWithRounding(BigInteger value, BigInteger shift)
{
- Contract.Ensures(Contract.Result() != null);
- if (value == "")
- {
- byte[] sigBytes = significand.ToByteArray();
- StringBuilder binSig = new StringBuilder();
+ // Handle left shifts (no rounding needed)
+ if (shift <= 0) {
+ return (BigIntegerMath.LeftShift(value, -shift), true);
+ }
- if (exponent == 0)
- {
- binSig.Append('0');
- }
- else
- {
- binSig.Append('1'); //hidden bit
- }
+ // Handle shifts that would result in zero
+ if (value.GetBitLength() <= shift) {
+ return (BigInteger.Zero, !value.IsZero);
+ }
- for (int i = significandSize - 2; i >= 0; --i)
- {
- //little endian
- if (i / 8 < sigBytes.Length)
- {
- binSig.Append((char) ('0' + ((sigBytes[i / 8] >> (i % 8)) & 1)));
- }
- else
- {
- binSig.Append('0');
- }
- }
+ // For very large right shifts, perform in chunks
+ var remaining = shift;
+ var current = value;
- BIM bias = BIM.Pow(2, exponentSize - 1) - 1;
- if (exponent == 0)
- {
- --bias;
+ // Shift by int.MaxValue chunks if needed
+ while (remaining > int.MaxValue) {
+ current >>= int.MaxValue;
+ remaining -= int.MaxValue;
+ if (current.IsZero) {
+ return (BigInteger.Zero, false);
}
+ }
- int moveDec = ((int) ((exponent - bias) % 4) + 4) % 4;
- BIM finalExp = (exponent - bias - moveDec) / 4;
+ // Perform final shift with IEEE 754 round-to-nearest-even
+ var intShift = (int)remaining;
+ var mask = (BigInteger.One << intShift) - 1;
+ var lostBits = current & mask;
+ var result = current >> intShift;
- string leftBinSig = binSig.ToString().Substring(0, moveDec + 1);
- string rightBinSig = binSig.ToString().Substring(moveDec + 1);
+ // If no bits lost, result is exact
+ if (lostBits.IsZero) {
+ return (result, true);
+ }
- leftBinSig = new string('0', 4 - leftBinSig.Length % 4) + leftBinSig;
- rightBinSig = rightBinSig + new string('0', 4 - rightBinSig.Length % 4);
+ // Round to nearest even
+ var halfBit = BigInteger.One << (intShift - 1);
+ if (lostBits > halfBit || (lostBits == halfBit && !result.IsEven)) {
+ result++;
+ }
- StringBuilder leftHexSig = new StringBuilder();
- StringBuilder rightHexSig = new StringBuilder();
+ return (result, false);
+ }
- for (int i = 0; i < leftBinSig.Length / 4; ++i)
- {
- leftHexSig.AppendFormat("{0:X}", Convert.ToByte(leftBinSig.Substring(i * 4, 4), 2));
- }
+ // Public convenience methods for special values
+ public static BigFloat CreateZero(bool isNegative, int significandSize, int exponentSize) =>
+ new (isNegative, 0, 0, significandSize, exponentSize, true);
+ public static BigFloat CreateInfinity(bool isNegative, int significandSize, int exponentSize) =>
+ new (isNegative, 0, GetMaxExponent(exponentSize), significandSize, exponentSize);
+ public static BigFloat CreateNaN(bool isNegative, int significandSize, int exponentSize) =>
+ new (isNegative, GetSignificandMask(significandSize - 1), GetMaxExponent(exponentSize), significandSize, exponentSize);
- for (int i = 0; i < rightBinSig.Length / 4; ++i)
- {
- rightHexSig.AppendFormat("{0:X}", Convert.ToByte(rightBinSig.Substring(i * 4, 4), 2));
- }
+ ///
+ /// Tries to create special values from string representation for SMT-LIB integration.
+ /// Supports: "NaN", "+oo", "-oo" (case insensitive)
+ ///
+ /// Special value string ("NaN", "+oo", "-oo")
+ /// Significand size in bits
+ /// Exponent size in bits
+ /// The resulting BigFloat if successful; default(BigFloat) otherwise
+ /// True if the special value was recognized and created; false otherwise
+ public static bool TryCreateSpecialFromString(string specialValue, int sigSize, int expSize, out BigFloat result) {
+ switch (specialValue.ToLowerInvariant()) {
+ case "nan":
+ result = CreateNaN(false, sigSize, expSize);
+ return true;
+ case "+oo":
+ result = CreateInfinity(false, sigSize, expSize);
+ return true;
+ case "-oo":
+ result = CreateInfinity(true, sigSize, expSize);
+ return true;
+ default:
+ result = default;
+ return false;
+ }
+ }
- return String.Format("{0}0x{1}.{2}e{3}f{4}e{5}", isSignBitSet ? "-" : "", leftHexSig, rightHexSig, finalExp,
- significandSize, exponentSize);
+ ///
+ /// Convert integer to BigFloat using direct IEEE 754 conversion
+ ///
+ private static BigFloat ConvertIntegerToBigFloat(BigInteger value, int significandSize, int exponentSize)
+ {
+ ValidateSizeParameters(significandSize, exponentSize);
+ if (!FromRational(value, 1, significandSize, exponentSize, out var f)) {
+ throw new ArgumentException($"The value {value} cannot be represented exactly with {significandSize}-bit significand and {exponentSize}-bit exponent", nameof(value));
}
- return String.Format("0{0}{1}e{2}", value, significandSize, exponentSize);
+ return f;
}
+ #endregion
+
+ #region IEEE 754 Operations
+
+ // IEEE 754 helper methods
+ public static BigInteger GetBias(int exponentSize) => (BigInteger.One << (exponentSize - 1)) - 1;
+ public static BigInteger GetMaxExponent(int exponentSize) => (BigInteger.One << exponentSize) - 1;
+ public static BigInteger GetLeadingBitPower(int significandSize) => BigInteger.One << (significandSize - 1); // Returns power value for the implicit leading significand bit
+ public static BigInteger GetSignificandMask(int significandSize) => (BigInteger.One << significandSize) - 1;
+
+ #endregion
+
+ // ============================================================================
+ // ARITHMETIC AND COMPARISON OPERATIONS
+ // ============================================================================
+
+ #region Arithmetic Operations
- ////////////////////////////////////////////////////////////////////////////
- // Conversion operations
+ [Pure] public static BigFloat operator -(BigFloat x) => new (!x.signBit, x.significand, x.exponent, x.SignificandSize, x.ExponentSize);
+ [Pure] public static BigFloat Abs(BigFloat x) => x.signBit ? -x : x;
+ [Pure] public static BigFloat Max(BigFloat x, BigFloat y) => x.IsNaN || y.IsNaN ? (x.IsNaN ? x : y) : (x >= y ? x : y);
+ [Pure] public static BigFloat Min(BigFloat x, BigFloat y) => x.IsNaN || y.IsNaN ? (x.IsNaN ? x : y) : (x <= y ? x : y);
+ [Pure] public static BigFloat CopySign(BigFloat x, BigFloat y) => x.signBit == y.signBit ? x : -x;
- // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
///
- /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
- /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+ /// Returns the sign: -1 for negative, 0 for zero/NaN, 1 for positive
///
- /// Floor (rounded towards negative infinity)
- /// Ceiling (rounded towards positive infinity)
- public void FloorCeiling(out BIM floor, out BIM ceiling)
- {
- Contract.Requires(value == "");
+ public int Sign() => IsNaN || IsZero ? 0 : (signBit ? -1 : 1);
- BIM sig = significand;
- BIM exp = exponent;
+ [Pure]
+ public static BigFloat operator +(BigFloat x, BigFloat y)
+ {
+ ValidateSizeCompatibility(x, y);
- BIM hiddenBitPow = BIM.Pow(2, significandSize - 1);
+ // Handle special values
+ var specialResult = HandleSpecialValues(x, y, ArithmeticOperation.Addition);
+ if (specialResult.HasValue) {
+ return specialResult.Value;
+ }
- if (exponent > 0)
- {
- sig += hiddenBitPow;
+ // Handle zeros
+ if (x.IsZero && y.IsZero) {
+ // IEEE 754: opposite signs sum to +0
+ var zeroResult = x.signBit != y.signBit ? CreateZero(false, x.SignificandSize, x.ExponentSize) : x;
+ return zeroResult;
}
- else
- {
- ++exp;
+ if (x.IsZero) {
+ return y;
+ }
+ if (y.IsZero) {
+ return x;
}
- exp -= (BIM.Pow(2, exponentSize - 1) - 1) + (significandSize - 1);
+ // Prepare signed operands
+ var (xSig, xExp) = PrepareOperand(x, x.leadingBit);
+ var (ySig, yExp) = PrepareOperand(y, y.leadingBit);
- if (exp >= BIM.Zero)
- {
- while (exp >= int.MaxValue)
- {
- sig <<= int.MaxValue;
- exp -= int.MaxValue;
- }
+ var xSigned = x.signBit ? -xSig : xSig;
+ var ySigned = y.signBit ? -ySig : ySig;
+
+ var expDiff = xExp - yExp;
- sig <<= (int) exp;
- floor = ceiling = (isSignBitSet ? -sig : sig);
+ // If operands are far apart, the smaller cannot affect the larger
+ // For same sign: no cancellation possible
+ // For opposite signs: when difference > significandSize + 1, the smaller value
+ // shifts completely out of range and doesn't affect the result
+ if (BigInteger.Abs(expDiff) > x.SignificandSize + 1) {
+ var farApartResult = expDiff > 0 ? x : y;
+ return farApartResult;
}
- else
- {
- exp = -exp;
- if (exp > significandSize)
- {
- if (sig == 0)
- {
- floor = ceiling = 0;
- }
- else
- {
- ceiling = isSignBitSet ? 0 : 1;
- floor = ceiling - 1;
- }
- }
- else
- {
- BIM frac = sig & ((BIM.One << (int) exp) - 1);
- sig >>= (int) exp; //Guaranteed to fit in a 32-bit integer
-
- if (frac == 0)
- {
- floor = ceiling = (isSignBitSet ? -sig : sig);
- }
- else
- {
- ceiling = isSignBitSet ? -sig : sig + 1;
- floor = ceiling - 1;
- }
- }
+ // Align significands and add
+ var sum = expDiff == 0 ? xSigned + ySigned :
+ expDiff > 0 ? xSigned + BigIntegerMath.RightShift(ySigned, expDiff) :
+ BigIntegerMath.RightShift(xSigned, -expDiff) + ySigned;
+
+ if (sum == 0) {
+ var zeroSumResult = CreateZero(x.signBit && y.signBit, x.SignificandSize, x.ExponentSize);
+ return zeroSumResult;
}
+
+ // Normalize result
+ var isNegative = sum < 0;
+ var absSum = isNegative ? -sum : sum;
+
+ var baseExp = xExp > yExp ? xExp : yExp;
+ var (normSig, normExp) = NormalizeAndRound(absSum, baseExp, x.SignificandSize);
+
+ var result = HandleExponentBounds(normSig, normExp, isNegative, x.SignificandSize, x.ExponentSize);
+ return result;
}
- public String ToBVString()
+ [Pure] public static BigFloat operator -(BigFloat x, BigFloat y) => x + -y;
+
+ [Pure]
+ public static BigFloat operator *(BigFloat x, BigFloat y)
{
- if (value != "")
- {
- return "_ " + value + " " + exponentSize + " " + significandSize;
+ ValidateSizeCompatibility(x, y);
+
+ // Handle special values
+ var specialResult = HandleSpecialValues(x, y, ArithmeticOperation.Multiplication);
+ if (specialResult.HasValue) {
+ return specialResult.Value;
}
- else if (value == "")
- {
- return "fp (_ bv" + (isSignBitSet ? "1" : "0") + " 1) (_ bv" + exponent + " " + exponentSize + ") (_ bv" +
- significand + " " + (significandSize - 1) + ")";
+
+ // Handle multiplication by zero - should always produce zero
+ if (x.IsZero || y.IsZero) {
+ return CreateZero(x.signBit ^ y.signBit, x.SignificandSize, x.ExponentSize);
}
- else
- {
- return "(_ to_fp " + exponentSize + " " + significandSize + ") (_ bv" + value + " " +
- (exponentSize + significandSize).ToString() + ")";
+
+ // Prepare operands and calculate result sign
+ var ((xSig, xExp), (ySig, yExp), resultSign) = PrepareOperandsForMultDiv(x, y);
+
+ // Multiply and check for zero
+ var product = xSig * ySig;
+ if (product == 0) {
+ return CreateZero(resultSign, x.SignificandSize, x.ExponentSize);
}
- }
- ////////////////////////////////////////////////////////////////////////////
- // Basic arithmetic operations
+ // Normalize and round the product
+ var (normalizedProduct, normalShift) = NormalizeAndRound(product, BigInteger.Zero, x.SignificandSize);
+
+ // Calculate the final exponent - all values are already BigInteger
+ var bias = x.bias;
+ var resultExp = xExp + yExp - bias + normalShift - (x.SignificandSize - 1);
+
+ // Handle overflow, underflow, and create final result
+ return HandleExponentBounds(normalizedProduct, resultExp, resultSign, x.SignificandSize, x.ExponentSize);
+ }
[Pure]
- public static BigFloat operator -(BigFloat x)
+ public static BigFloat operator /(BigFloat x, BigFloat y)
{
- if (x.value != "")
- {
- if (x.value[0] == '-')
- {
- return new BigFloat("+oo", x.significandSize, x.exponentSize);
- }
+ ValidateSizeCompatibility(x, y);
- if (x.value[0] == '+')
- {
- return new BigFloat("-oo", x.significandSize, x.exponentSize);
- }
+ // Handle special cases
+ var specialResult = HandleSpecialValues(x, y, ArithmeticOperation.Division);
+ if (specialResult.HasValue) {
+ return specialResult.Value;
+ }
+
+ // Prepare operands and calculate result sign
+ var ((xSig, xExp), (ySig, yExp), resultSign) = PrepareOperandsForMultDiv(x, y);
- return new BigFloat("NaN", x.significandSize, x.exponentSize);
+ // Shift dividend left for precision and divide with rounding
+ var shiftedDividend = BigIntegerMath.LeftShift(xSig, x.SignificandSize + 1);
+ var quotient = BigInteger.DivRem(shiftedDividend, ySig, out var remainder);
+ quotient = ApplyRoundToNearestEven(quotient, remainder, ySig);
+
+ if (quotient == 0) {
+ return CreateZero(resultSign, x.SignificandSize, x.ExponentSize);
}
- return new BigFloat(!x.isSignBitSet, x.significand, x.exponent, x.significandSize, x.exponentSize);
+ // Normalize and calculate final exponent
+ var (normalizedQuotient, normalShift) = NormalizeAndRound(quotient, BigInteger.Zero, x.SignificandSize);
+ var resultExp = xExp - yExp + x.bias + normalShift - 2;
+
+ return HandleExponentBounds(normalizedQuotient, resultExp, resultSign, x.SignificandSize, x.ExponentSize);
}
- [Pure]
- public static BigFloat operator +(BigFloat x, BigFloat y)
+ private static (BigInteger significand, BigInteger exponent) NormalizeAndRound(BigInteger value, BigInteger exponent, int targetBits)
{
- Contract.Requires(x.exponentSize == y.exponentSize);
- Contract.Requires(x.significandSize == y.significandSize);
-
- if (x.value != "" || y.value != "")
- {
- if (x.value == "NaN" || y.value == "NaN" || x.value == "+oo" && y.value == "-oo" ||
- x.value == "-oo" && y.value == "+oo")
- {
- return new BigFloat("NaN", x.significandSize, x.exponentSize);
- }
+ var valueBits = value.GetBitLength();
+ var shift = valueBits - targetBits;
- if (x.value != "")
- {
- return new BigFloat(x.value, x.significandSize, x.exponentSize);
- }
+ // Use IEEE 754 compliant shift and round method
+ var (shiftedValue, _) = ApplyShiftWithRounding(value, shift);
+ var adjustedExponent = exponent + shift;
- return new BigFloat(y.value, y.significandSize, y.exponentSize);
+ // Handle potential overflow from rounding (only for right shifts)
+ if (shift > 0 && shiftedValue.GetBitLength() > targetBits) {
+ shiftedValue >>= 1;
+ adjustedExponent++;
}
- if (x.exponent > y.exponent)
- {
- BigFloat temp = x;
- x = y;
- y = temp;
+ return (shiftedValue, adjustedExponent);
+ }
+
+ private static BigFloat HandleExponentBounds(BigInteger significand, BigInteger exponent, bool isNegative, int significandSize, int exponentSize)
+ {
+ var maxExponent = GetMaxExponent(exponentSize);
+
+ // Handle overflow to infinity
+ if (exponent >= maxExponent) {
+ return CreateInfinity(isNegative, significandSize, exponentSize);
}
- BIM xsig = x.significand, ysig = y.significand;
- BIM xexp = x.exponent, yexp = y.exponent;
+ // Handle normal numbers
+ if (exponent > 0) {
+ // Remove implicit leading bit for storage (it's encoded in the biased exponent)
+ var leadingBitMask = GetLeadingBitPower(significandSize) - 1;
+ return new BigFloat(isNegative, significand & leadingBitMask, exponent, significandSize, exponentSize);
+ }
- if (yexp - xexp > x.significandSize) //One of the numbers is relatively insignificant
- {
- return new BigFloat(y.isSignBitSet, y.significand, y.exponent, y.significandSize, y.exponentSize);
+ // Handle complete underflow to zero
+ var bias = GetBias(exponentSize);
+ if (exponent < BigInteger.One - bias - (significandSize - 1)) {
+ return CreateZero(isNegative, significandSize, exponentSize);
}
- BIM hiddenBitPow = BIM.Pow(2, x.significandSize - 1);
+ // Handle subnormal numbers with gradual underflow
+ var (shiftedSig, _) = ApplyShiftWithRounding(significand, BigInteger.One - exponent);
- if (xexp > 0)
- {
- xsig += hiddenBitPow;
+ // Check if rounding caused overflow back to smallest normal number
+ if (shiftedSig.GetBitLength() == significandSize) {
+ return new BigFloat(isNegative, 0, 1, significandSize, exponentSize);
}
- else
- {
- ++xexp;
+
+ return new BigFloat(isNegative, shiftedSig, 0, significandSize, exponentSize);
+ }
+
+ ///
+ /// Arithmetic operation types for special value handling
+ ///
+ private enum ArithmeticOperation
+ {
+ Addition,
+ Multiplication,
+ Division
+ }
+
+ ///
+ /// Handles special value cases for all arithmetic operations
+ /// Returns null if no special case applies
+ ///
+ private static BigFloat? HandleSpecialValues(BigFloat x, BigFloat y, ArithmeticOperation operation)
+ {
+ // NaN propagation - always first priority
+ if (x.IsNaN || y.IsNaN) {
+ return CreateNaN(false, x.SignificandSize, x.ExponentSize);
}
- if (yexp > 0)
+ var resultSign = x.signBit ^ y.signBit;
+ var sigSize = x.SignificandSize;
+ var expSize = x.ExponentSize;
+
+ switch (operation)
{
- ysig += hiddenBitPow;
+ case ArithmeticOperation.Addition:
+ if (x.IsInfinity && y.IsInfinity) {
+ return x.signBit != y.signBit ? CreateNaN(false, sigSize, expSize) : x;
+ }
+
+ if (x.IsInfinity) {
+ return x;
+ }
+
+ if (y.IsInfinity) {
+ return y;
+ }
+
+ break;
+
+ case ArithmeticOperation.Multiplication:
+ if ((x.IsInfinity && y.IsZero) || (y.IsInfinity && x.IsZero)) {
+ return CreateNaN(false, sigSize, expSize);
+ }
+
+ if (x.IsInfinity || y.IsInfinity) {
+ return CreateInfinity(resultSign, sigSize, expSize);
+ }
+
+ break;
+
+ case ArithmeticOperation.Division:
+ if (y.IsZero) {
+ return x.IsZero ? CreateNaN(false, sigSize, expSize) : CreateInfinity(resultSign, sigSize, expSize);
+ }
+
+ if (x.IsZero) {
+ return CreateZero(resultSign, sigSize, expSize);
+ }
+
+ if (x.IsInfinity && y.IsInfinity) {
+ return CreateNaN(false, sigSize, expSize);
+ }
+
+ if (x.IsInfinity) {
+ return CreateInfinity(resultSign, sigSize, expSize);
+ }
+
+ if (y.IsInfinity) {
+ return CreateZero(resultSign, sigSize, expSize);
+ }
+
+ break;
}
- else
- {
- ++yexp;
+
+ return null; // No special case applies
+ }
+
+ #endregion
+
+ #region Mathematical Operations
+
+ ///
+ /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
+ /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+ ///
+ /// Floor (rounded towards negative infinity)
+ /// Ceiling (rounded towards positive infinity)
+ public void FloorCeiling(out BigInteger floor, out BigInteger ceiling)
+ {
+ // Handle special cases
+ if (IsNaN || IsInfinity) {
+ throw new InvalidOperationException($"Cannot compute floor/ceiling of {(IsNaN ? "NaN" : "infinity")} value");
}
- if (x.isSignBitSet)
- {
- xsig = -xsig;
+ if (IsZero) {
+ floor = ceiling = 0;
+ return;
}
- if (y.isSignBitSet)
- {
- ysig = -ysig;
+ // Convert to rational and compute integer part
+ var significandValue = IsNormal ? (significand | leadingBit) : significand;
+ var shift = (IsNormal ? GetActualExponent() : BigInteger.One) - bias - (SignificandSize - 1);
+
+ BigInteger integerPart;
+ bool hasRemainder;
+
+ if (shift >= 0) {
+ integerPart = BigIntegerMath.LeftShift(significandValue, shift);
+ hasRemainder = false;
+ } else if (-shift >= SignificandSize) {
+ integerPart = 0;
+ hasRemainder = true;
+ } else {
+ var absShift = -shift;
+ integerPart = BigIntegerMath.RightShift(significandValue, absShift);
+ hasRemainder = (significandValue & GetMask(absShift)) != 0;
}
- xsig >>= (int) (yexp - xexp); //Guaranteed to fit in a 32-bit integer
+ // Apply sign and compute floor/ceiling
+ if (signBit) {
+ floor = hasRemainder ? -integerPart - 1 : -integerPart;
+ ceiling = -integerPart;
+ } else {
+ floor = integerPart;
+ ceiling = hasRemainder ? integerPart + 1 : integerPart;
+ }
+ }
- ysig += xsig;
+ #endregion
- bool isNeg = ysig < 0;
+ #region Comparison Operations
- ysig = BIM.Abs(ysig);
+ ///
+ /// Compares this BigFloat with another BigFloat for ordering purposes.
+ /// This method follows the specification for C#'s Single.CompareTo method.
+ /// As a result, it handles NaNs differently than how the ==, !=, <, >, <=, and >= operators do.
+ /// For example, the expression (0.0f / 0.0f).CompareTo(0.0f / 0.0f) should return 0,
+ /// whereas the expression (0.0f / 0.0f) == (0.0f / 0.0f) should return false.
+ ///
+ /// IMPORTANT: This dual behavior is intentional and correct:
+ /// - CompareTo: Provides consistent total ordering for sorting (NaN == NaN returns 0)
+ /// - == operator: Follows IEEE 754 mathematical semantics (NaN == NaN returns false)
+ ///
+ /// This allows collections containing NaN values to be sorted while maintaining
+ /// IEEE 754 compliance for mathematical operations.
+ ///
+ /// The BigFloat to compare with
+ ///
+ /// Less than zero: This instance is less than 'that'
+ /// Zero: This instance equals 'that' (including NaN == NaN for ordering)
+ /// Greater than zero: This instance is greater than 'that'
+ ///
+ public int CompareTo(BigFloat that)
+ {
+ // Validate size compatibility first
+ ValidateSizeCompatibility(this, that);
- if (ysig == 0)
- {
- return new BigFloat(x.isSignBitSet && y.isSignBitSet, 0, 0, x.significandSize, x.exponentSize);
+ // NaN handling - special ordering for collections
+ if (IsNaN || that.IsNaN) {
+ if (IsNaN && that.IsNaN) {
+ return 0;
+ }
+ return IsNaN ? 1 : -1;
}
- if (ysig >= hiddenBitPow * 2)
- {
- ysig >>= 1;
- ++yexp;
+ // Infinity handling
+ if (IsInfinity || that.IsInfinity) {
+ if (IsInfinity && that.IsInfinity && signBit == that.signBit) {
+ return 0;
+ }
+ if (IsInfinity) {
+ return signBit ? -1 : 1;
+ }
+ return that.signBit ? 1 : -1;
}
- while (ysig < hiddenBitPow && yexp > 1)
- {
- ysig <<= 1;
- --yexp;
+ // Zero handling - IEEE 754: +0 == -0
+ if (IsZero && that.IsZero) {
+ return 0;
}
- if (ysig < hiddenBitPow)
- {
- yexp = 0;
- }
- else
- {
- ysig -= hiddenBitPow;
+ // Sign comparison
+ if (signBit != that.signBit) {
+ return signBit ? -1 : 1;
}
- if (yexp >= BIM.Pow(2, x.exponentSize) - 1)
- {
- return new BigFloat(y.isSignBitSet ? "-oo" : "+oo", x.significandSize, x.exponentSize);
+ // Same sign - compare magnitude
+ var cmp = exponent.CompareTo(that.exponent);
+ if (cmp == 0) {
+ cmp = significand.CompareTo(that.significand);
}
- return new BigFloat(isNeg, ysig, yexp, x.significandSize, x.exponentSize);
+ return signBit ? -cmp : cmp;
}
- [Pure]
- public static BigFloat operator -(BigFloat x, BigFloat y)
- {
- return x + -y;
- }
+ [Pure] public static bool operator ==(BigFloat x, BigFloat y) =>
+ (!x.IsNaN && !y.IsNaN) && ((x.IsZero && y.IsZero) || x.CompareTo(y) == 0);
+
+ [Pure] public static bool operator !=(BigFloat x, BigFloat y) => !(x == y);
+
+ [Pure] public static bool operator <(BigFloat x, BigFloat y) =>
+ (!x.IsNaN && !y.IsNaN) && x.CompareTo(y) < 0;
+
+ [Pure] public static bool operator >(BigFloat x, BigFloat y) =>
+ (!x.IsNaN && !y.IsNaN) && x.CompareTo(y) > 0;
+
+ [Pure] public static bool operator <=(BigFloat x, BigFloat y) =>
+ (!x.IsNaN && !y.IsNaN) && x.CompareTo(y) <= 0;
+
+ [Pure] public static bool operator >=(BigFloat x, BigFloat y) =>
+ (!x.IsNaN && !y.IsNaN) && x.CompareTo(y) >= 0;
+
+ [Pure] public override bool Equals(object obj) => obj is BigFloat bigFloat && this == bigFloat;
+
+ [Pure] public override int GetHashCode() =>
+ HashCode.Combine(significand, exponent, signBit, SignificandSize, ExponentSize);
+
+ #endregion
+
+ #region String Representation
[Pure]
- public static BigFloat operator *(BigFloat x, BigFloat y)
+ public string ToDecimalString()
{
- Contract.Requires(x.exponentSize == y.exponentSize);
- Contract.Requires(x.significandSize == y.significandSize);
-
- if (x.value == "NaN" || y.value == "NaN" || (x.value == "+oo" || x.value == "-oo") && y.IsZero ||
- (y.value == "+oo" || y.value == "-oo") && x.IsZero)
- {
- return new BigFloat("NaN", x.significandSize, x.exponentSize);
+ // Handle special values
+ if (IsNaN) {
+ return "NaN";
}
-
- if (x.value != "" || y.value != "")
- {
- bool xSignBitSet = x.value == "" ? x.isSignBitSet : x.value[0] == '-';
- bool ySignBitSet = y.value == "" ? y.isSignBitSet : y.value[0] == '-';
- return new BigFloat((xSignBitSet ^ ySignBitSet ? "-" : "+") + "oo", x.significandSize, x.exponentSize);
+ if (IsInfinity) {
+ return signBit ? "-Infinity" : "Infinity";
+ }
+ if (IsZero) {
+ return signBit ? "-0" : "0";
}
- BIM xsig = x.significand, ysig = y.significand;
- BIM xexp = x.exponent, yexp = y.exponent;
+ // Convert to rational number
+ var significandValue = IsNormal ? (significand | leadingBit) : significand;
+ var shift = (IsNormal ? GetActualExponent() : BigInteger.One) - bias - (SignificandSize - 1);
- BIM hiddenBitPow = BIM.Pow(2, x.significandSize - 1);
+ // Calculate numerator and denominator
+ var (numerator, denominator) = shift >= 0
+ ? (BigIntegerMath.LeftShift(significandValue, shift), BigInteger.One)
+ : (significandValue, BigIntegerMath.LeftShift(BigInteger.One, -shift));
- if (xexp > 0)
- {
- xsig += hiddenBitPow;
- }
- else
- {
- ++xexp;
+ if (signBit) {
+ numerator = -numerator;
}
- if (yexp > 0)
- {
- ysig += hiddenBitPow;
+ // Convert to decimal with appropriate scale
+ var desiredScale = denominator.GetBitLength() * 0.31; // Approximate decimal digits needed
+ if (desiredScale > int.MaxValue - 1) {
+ throw new OverflowException($"Cannot convert to decimal string: required scale {desiredScale:E} exceeds maximum supported scale {int.MaxValue}");
}
- else
- {
- ++yexp;
+ var scale = (int)desiredScale;
+ var scaled = BigInteger.Abs(numerator) * BigInteger.Pow(10, scale) / denominator;
+ var str = scaled.ToString().PadLeft(scale + 1, '0');
+
+ // Format with decimal point
+ if (scale == 0) {
+ return signBit && !IsZero ? "-" + str : str;
}
- ysig *= xsig;
- yexp += xexp - (BIM.Pow(2, x.exponentSize - 1) - 1) - (x.significandSize - 1);
+ var intPart = str[..^scale];
+ var fracPart = str[^scale..].TrimEnd('0');
+ var result = fracPart.Length > 0 ? $"{intPart}.{fracPart}" : intPart;
- while (ysig >= hiddenBitPow * 2 || yexp <= 0)
- {
- ysig >>= 1;
- ++yexp;
+ return signBit ? "-" + result : result;
+ }
+
+ public override string ToString()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ // Handle special values
+ if (exponent == maxExponent) {
+ return $"0{(significand == 0 ? $"{(signBit ? "-" : "+")}oo" : "NaN")}{SignificandSize}e{ExponentSize}";
}
- while (ysig < hiddenBitPow && yexp > 1)
- {
- ysig <<= 1;
- --yexp;
+ // Handle zero
+ if (IsZero) {
+ return $"{(signBit ? "-" : "")}0x0.0e0f{SignificandSize}e{ExponentSize}";
}
- if (ysig < hiddenBitPow)
- {
- yexp = 0;
+ // Get significand and binary exponent
+ var significandBits = IsSubnormal ? significand : (significand | leadingBit);
+ var binaryExp = (IsSubnormal ? BigInteger.One - bias : exponent - bias) - (SignificandSize - 1);
+
+ // Calculate hex exponent and adjust significand for bit remainder
+ var hexExp = binaryExp / 4;
+ var bitRemainder = (int)(binaryExp % 4);
+
+ if (bitRemainder < 0) {
+ significandBits <<= (4 + bitRemainder);
+ hexExp--;
+ } else if (bitRemainder > 0) {
+ significandBits <<= bitRemainder;
}
- else
- {
- ysig -= hiddenBitPow;
+
+ // Convert to hex and format as H.HHH
+ var hexStr = significandBits.ToString("X");
+ if (hexStr.Length == 1) {
+ return $"{(signBit ? "-" : "")}0x{hexStr}.0e{hexExp}f{SignificandSize}e{ExponentSize}";
}
- if (yexp >= BIM.Pow(2, x.exponentSize) - 1)
- {
- return new BigFloat(x.isSignBitSet ^ y.isSignBitSet ? "-oo" : "+oo", x.significandSize, x.exponentSize);
+ // Format with decimal point after first digit
+ var fracPart = hexStr[1..].TrimEnd('0');
+ if (fracPart.Length == 0) {
+ fracPart = "0";
}
+ hexExp += hexStr.Length - 1;
- return new BigFloat(x.isSignBitSet ^ y.isSignBitSet, ysig, yexp, x.significandSize, x.exponentSize);
+ return $"{(signBit ? "-" : "")}0x{hexStr[0]}.{fracPart}e{hexExp}f{SignificandSize}e{ExponentSize}";
}
+ #endregion
- ////////////////////////////////////////////////////////////////////////////
- // Some basic comparison operations
-
- public bool IsZero
- {
- get { return value == "" && significand.IsZero && exponent.IsZero; }
- }
+ #region String Parsing
///
- /// This method follows the specification for C#'s Single.CompareTo method.
- /// As a result, it handles NaNs differently than how the ==, !=, <, >, <=, and >= operators do.
- /// For example, the expression (0.0f / 0.0f).CompareTo(0.0f / 0.0f) should return 0,
- /// whereas the expression (0.0f / 0.0f) == (0.0f / 0.0f) should return false.
+ /// Tries to parse hex format BigFloat strings according to the specification
///
- [Pure]
- public int CompareTo(BigFloat that)
+ /// The hex format string to parse (without size suffixes)
+ /// The significand size in bits
+ /// The exponent size in bits
+ /// When true, enforces Boogie's strict parsing rules (no precision loss, no extreme underflow);
+ /// when false, follows IEEE 754 standard behavior
+ /// The parsed BigFloat value if successful; default(BigFloat) otherwise
+ /// True if the parse was successful; false otherwise
+ private static bool TryParseHexFormat(string s, int sigSize, int expSize, bool strict, out BigFloat result)
{
- Contract.Requires(exponentSize == that.exponentSize);
- Contract.Requires(significandSize == that.significandSize);
+ result = default;
- if (value == "" && that.value == "")
- {
- int cmpThis = IsZero ? 0 : isSignBitSet ? -1 : 1;
- int cmpThat = that.IsZero ? 0 : that.isSignBitSet ? -1 : 1;
-
- if (cmpThis == cmpThat)
- {
- if (exponent == that.exponent)
- {
- return cmpThis * significand.CompareTo(that.significand);
- }
+ // Parse format: [-]0x.e
+ var posX = s.IndexOf("0x", StringComparison.Ordinal);
+ var posE = s.LastIndexOf('e');
+ if (posX < 0 || posE <= posX + 2) {
+ return false;
+ }
- return cmpThis * exponent.CompareTo(that.exponent);
- }
+ // Extract hex significand and find decimal point
+ var hexPart = s[(posX + 2)..posE];
+ var dotPos = hexPart.IndexOf('.');
+ var exponentPart = s[(posE + 1)..];
+
+ // Check for spaces in the exponent part
+ if (exponentPart.Contains(' ')) {
+ return false;
+ }
+
+ if (dotPos < 0 ||
+ !TryParseHex(hexPart[..dotPos], out var intPart) ||
+ !TryParseHex(hexPart[(dotPos + 1)..], out var fracPart) ||
+ !BigInteger.TryParse(exponentPart, out var decExp)) {
+ return false;
+ }
+
+ // Build significand from hex parts
+ var fracBits = ((long)hexPart.Length - dotPos - 1) * 4;
+ var sig = BigIntegerMath.LeftShift(intPart, fracBits) | fracPart;
+ var isNegative = s.Length > 0 && s[0] == '-';
+
+ if (sig == 0) {
+ result = CreateZero(isNegative, sigSize, expSize);
+ return true;
+ }
- if (cmpThis == 0)
- {
- return -cmpThat;
+ // Calculate biased exponent
+ var msbPos = sig.GetBitLength() - 1;
+ var biasedExp = new BigInteger(msbPos - fracBits) + (decExp * 4) + GetBias(expSize);
+
+ // Handle overflow/underflow/normal cases
+ if (biasedExp >= GetMaxExponent(expSize)) {
+ if (strict) {
+ return false;
}
+ result = CreateInfinity(isNegative, sigSize, expSize);
+ return true;
+ }
- return cmpThis;
+ if (biasedExp <= 0) {
+ return HandleUnderflow(isNegative, sig, biasedExp, sigSize, expSize, strict, out result);
}
- if (value == that.value)
- {
- return 0;
+ // Normal number - check precision loss and normalize
+ var shift = new BigInteger(msbPos) - (sigSize - 1);
+ if (strict && shift > 0 && shift < sig.GetBitLength() && (sig & GetMask(shift)) != 0) {
+ return false;
}
- if (value == "NaN" || that.value == "+oo" || value == "-oo" && that.value != "NaN")
- {
- return -1;
+ // Apply IEEE 754 rounding instead of truncation
+ BigInteger roundedSig;
+ BigInteger adjustedBiasedExp = biasedExp;
+
+ if (shift > 0) {
+ var (shifted, _) = ApplyShiftWithRounding(sig, shift);
+ roundedSig = shifted;
+
+ // Check if rounding caused overflow to next power of 2
+ if (roundedSig.GetBitLength() > sigSize) {
+ roundedSig >>= 1;
+ adjustedBiasedExp++;
+
+ // Check for exponent overflow
+ if (adjustedBiasedExp >= GetMaxExponent(expSize)) {
+ if (strict) {
+ return false;
+ }
+ result = CreateInfinity(isNegative, sigSize, expSize);
+ return true;
+ }
+ }
+
+ roundedSig &= (GetLeadingBitPower(sigSize) - 1);
+ } else {
+ roundedSig = BigIntegerMath.RightShift(sig, shift) & (GetLeadingBitPower(sigSize) - 1);
}
- return 1;
+ result = new BigFloat(isNegative, roundedSig, adjustedBiasedExp, sigSize, expSize);
+ return true;
}
- [Pure]
- public static bool operator ==(BigFloat x, BigFloat y)
+ private static bool TryParseHex(string hex, out BigInteger value)
{
- if (x.value == "NaN" || y.value == "NaN")
- {
+ value = 0;
+ // Boogie spec requires at least one hex digit, so empty strings are invalid
+ if (hex.Length == 0) {
return false;
}
-
- return x.CompareTo(y) == 0;
+ return BigInteger.TryParse("0" + hex, System.Globalization.NumberStyles.HexNumber, null, out value);
}
- [Pure]
- public static bool operator !=(BigFloat x, BigFloat y)
+ private static bool HandleUnderflow(bool signBit, BigInteger sig, BigInteger biasedExp, int sigSize, int expSize, bool strict, out BigFloat result)
{
- if (x.value == "NaN" || y.value == "NaN")
- {
+ result = default;
+ var bias = GetBias(expSize);
+ var minSubnormalExp = BigInteger.One - bias - (sigSize - 1);
+ var actualExp = biasedExp - bias;
+
+ // Complete underflow to zero
+ if (actualExp < minSubnormalExp) {
+ if (strict) {
+ return false;
+ }
+ result = CreateZero(signBit, sigSize, expSize);
return true;
}
- return x.CompareTo(y) != 0;
- }
+ // Calculate required shift for subnormal representation
+ var currentMsb = sig.GetBitLength() - 1;
+ var targetPosition = actualExp - minSubnormalExp;
+ var shiftAmount = new BigInteger(currentMsb) - targetPosition;
- [Pure]
- public static bool operator <(BigFloat x, BigFloat y)
- {
- if (x.value == "NaN" || y.value == "NaN")
- {
- return false;
+ // Apply shift with IEEE 754 rounding
+ var (subnormalSig, _) = ApplyShiftWithRounding(sig, shiftAmount);
+
+ if (subnormalSig.IsZero) {
+ if (strict) {
+ return false;
+ }
+ result = CreateZero(signBit, sigSize, expSize);
+ return true;
}
- return x.CompareTo(y) < 0;
+ // Check if rounding caused overflow to normal range
+ if (subnormalSig.GetBitLength() > sigSize - 1) {
+ if (strict) {
+ return false;
+ }
+ // Overflow to smallest normal number
+ result = new BigFloat(signBit, 0, 1, sigSize, expSize);
+ return true;
+ }
+
+ result = new BigFloat(signBit, subnormalSig, 0, sigSize, expSize);
+ return true;
}
- [Pure]
- public static bool operator >(BigFloat x, BigFloat y)
+ ///
+ /// Converts to SMT-LIB format string
+ ///
+ public string ToSMTLibString() =>
+ exponent == maxExponent ?
+ $"_ {(significand == 0 ? $"{(signBit ? "-" : "+")}oo" : "NaN")} {ExponentSize} {SignificandSize}" :
+ $"fp (_ bv{(signBit ? "1" : "0")} 1) (_ bv{exponent} {ExponentSize}) (_ bv{significand} {SignificandSize - 1})";
+
+ #endregion
+ }
+
+ ///
+ /// Helper class for BigInteger arithmetic operations that require shift amounts larger than int.MaxValue
+ ///
+ internal static class BigIntegerMath
+ {
+ ///
+ /// Left shift operation that handles BigInteger shift amounts
+ ///
+ /// The value to shift
+ /// The number of bits to shift left (can be negative for right shift)
+ /// The result of value << shift, handling shifts larger than int.MaxValue
+ public static BigInteger LeftShift(BigInteger value, BigInteger shift)
{
- if (x.value == "NaN" || y.value == "NaN")
- {
- return false;
+ if (shift < 0) {
+ return RightShift(value, -shift);
+ }
+ if (shift == 0 || value == 0) {
+ return value;
}
- return x.CompareTo(y) > 0;
- }
+ // Perform shift in chunks of int.MaxValue
+ var result = value;
+ var remaining = shift;
- [Pure]
- public static bool operator <=(BigFloat x, BigFloat y)
- {
- if (x.value == "NaN" || y.value == "NaN")
- {
- return false;
+ while (remaining > 0) {
+ var currentShift = remaining > int.MaxValue ? int.MaxValue : (int)remaining;
+ result <<= currentShift;
+ remaining -= currentShift;
}
- return x.CompareTo(y) <= 0;
+ return result;
}
- [Pure]
- public static bool operator >=(BigFloat x, BigFloat y)
+ ///
+ /// Right shift operation that handles BigInteger shift amounts
+ ///
+ /// The value to shift
+ /// The number of bits to shift right (can be negative for left shift)
+ /// The result of value >> shift, handling shifts larger than int.MaxValue
+ public static BigInteger RightShift(BigInteger value, BigInteger shift)
{
- if (x.value == "NaN" || y.value == "NaN")
- {
- return false;
+ if (shift < 0) {
+ return LeftShift(value, -shift);
+ }
+ if (shift == 0) {
+ return value;
+ }
+
+ // Early exit if result would be zero
+ if (value.GetBitLength() <= shift) {
+ return BigInteger.Zero;
+ }
+
+ // Perform shift in chunks of int.MaxValue
+ var result = value;
+ var remaining = shift;
+
+ while (remaining > 0) {
+ var currentShift = remaining > int.MaxValue ? int.MaxValue : (int)remaining;
+ result >>= currentShift;
+ remaining -= currentShift;
+
+ // Early exit if we've shifted to zero
+ if (result.IsZero) {
+ return BigInteger.Zero;
+ }
}
- return x.CompareTo(y) >= 0;
+ return result;
}
}
}
\ No newline at end of file
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 17f40bbd5..3db314713 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -1977,11 +1977,9 @@ Float
(
float (. s = t.val; .)
)
- (. try {
- n = BigFloat.FromString(s);
- } catch (FormatException e) {
- this.SemErr("incorrectly formatted floating point, " + e.Message);
- n = BigFloat.ZERO;
+ (. if (!BigFloat.TryParseExact(s, out n)) {
+ this.SemErr("incorrectly formatted floating point");
+ n = BigFloat.CreateZero(false, 24, 8);
}
.)
.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 4de7b517c..a28c94891 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -2473,11 +2473,9 @@ void Float(out BigFloat n) {
string s = "";
Expect(7);
s = t.val;
- try {
- n = BigFloat.FromString(s);
- } catch (FormatException e) {
- this.SemErr("incorrectly formatted floating point, " + e.Message);
- n = BigFloat.ZERO;
+ if (!BigFloat.TryParseExact(s, out n)) {
+ this.SemErr("incorrectly formatted floating point");
+ n = BigFloat.CreateZero(false, 24, 8);
}
}
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index c4c3ed464..bd0ee0130 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
- 3.5.4
+ 3.5.5
net8.0
false
Boogie
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 25bec5f69..0f9353c28 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -29,6 +29,7 @@ An instance of the Model class represents a single model returned from the SMT s
using System.Collections.Generic;
using System.Text;
using System.Text.RegularExpressions;
+using Microsoft.BaseTypes;
namespace Microsoft.Boogie
{
@@ -44,7 +45,8 @@ public enum ElementKind
Boolean,
Uninterpreted,
Array,
- DataValue
+ DataValue,
+ Float
}
public abstract class Element
@@ -187,6 +189,26 @@ public override string ToString()
}
}
+ public class Float : Element
+ {
+ internal Float(Model p, string n) : base(p)
+ {
+ Literal = n;
+ }
+
+ public readonly string Literal;
+
+ public override ElementKind Kind
+ {
+ get { return ElementKind.Float; }
+ }
+
+ public override string ToString()
+ {
+ return Literal;
+ }
+ }
+
public class Boolean : Element
{
public bool Value;
@@ -716,7 +738,14 @@ public Element ConstructElement(string name)
}
else
{
- return null;
+ // Try parsing as BigFloat
+ try {
+ var _ = BigFloat.FromString(name);
+ return new Float(this, name);
+ } catch {
+ // Not a valid number at all
+ return null;
+ }
}
}
else if (name[0] == '*' || name.StartsWith("val!") || name.Contains("!val!"))
diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj
index dc907880d..7133d6fad 100644
--- a/Source/Model/Model.csproj
+++ b/Source/Model/Model.csproj
@@ -6,6 +6,7 @@
+
diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
index e58b25eac..18430d907 100644
--- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
@@ -601,7 +601,10 @@ public override async Task