From 25fca02e1deb9e60e6e330803731c9b4fcd45d34 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 18 May 2015 22:08:43 -0600 Subject: added interpretation of floating point constants to the parser --- Source/Basetypes/BigFloat.cs | 155 +++++++++++++++++++++++++++++++++---------- 1 file changed, 119 insertions(+), 36 deletions(-) (limited to 'Source/Basetypes') diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 0b35c237..a4cd6574 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -25,21 +25,19 @@ namespace Microsoft.Basetypes // the internal representation [Rep] - internal readonly Boolean[] mantissa; //Note that the first element of the mantissa array is the least significant bit for coding simplicity + internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left) [Rep] internal readonly Boolean isNegative; //The left-most (sign) bit in the float representation [Rep] - internal readonly int exponent; + internal readonly int mantissaSize; [Rep] - internal readonly int exponentSize; //The maximum bit size of the exponent + internal readonly int exponent; //The value of the exponent is always positive as per fp representation requirements + [Rep] + internal readonly int exponentSize; //The bit size of the exponent public BIM Mantissa { get { - BIM toReturn = 0; - for (int i = 0; i < mantissa.Length; i++) - if (mantissa[i]) - toReturn += (int) Math.Pow(2, i); - return isNegative ? -toReturn : toReturn; + return isNegative ? -mantissa : mantissa; } } @@ -53,7 +51,7 @@ namespace Microsoft.Basetypes { get { - return mantissa.Length; + return mantissaSize; } } @@ -65,8 +63,18 @@ namespace Microsoft.Basetypes } } - public static readonly BigFloat ZERO = FromInt(0); + public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero + public static BigFloat INF(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard + public static BigFloat NEGINF(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard + public static BigFloat NAN(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard + private static readonly BIM two = new BIM(2); + private static BIM two_n(int n) { + BIM toReturn = new BIM(1); + for (int i = 0; i < n; i++) + toReturn = toReturn * two; + return toReturn; + } //////////////////////////////////////////////////////////////////////////// @@ -116,17 +124,39 @@ namespace Microsoft.Basetypes } internal BigFloat(BIM mantissa, int exponent, int mantissaSize, int exponentSize) { - this.mantissa = new Boolean[mantissaSize]; + this.mantissa = mantissa; + this.mantissaSize = mantissaSize; this.exponentSize = exponentSize; - this.exponent = exponent; - //TODO: Add overflow check for exponent vs exponent size + this.exponent = exponent + (int)Math.Pow(2, exponentSize - 1); + if (exponent < 0) { //ZERO case since the exponent is less than the minimum + mantissa = 0; + exponent = 0; + this.isNegative = false; + return; + } + this.isNegative = mantissa < 0; if (this.isNegative) - mantissa = -mantissa; + mantissa = -mantissa; // ==> mantissa > 0 + + BIM max = maxMantissa(); + while (this.mantissa > max) { + this.mantissa = this.mantissa / two; + this.exponent++; + } + + //TODO: Add overflow check for exponent vs exponent size + //this.exponent = this.exponent % this.exponentSize; ?? } - private int maxExponent() { return (int)Math.Pow(2, exponentSize - 1) - 1; } - private int minExponent() { return -(int)Math.Pow(2, exponentSize - 1); } + private BIM maxMantissa() + { + BIM result = new BIM(1); + for (int i = 0; i < mantissaSize; i++) + result = result * two; + return result - 1; + } + private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } @@ -151,25 +181,32 @@ namespace Microsoft.Basetypes [Pure] public override string/*!*/ ToString() { - //TODO: modify to reflect floating points Contract.Ensures(Contract.Result() != null); - return String.Format("{0}e{1}", Mantissa.ToString(), Exponent.ToString()); + return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); } //////////////////////////////////////////////////////////////////////////// // Conversion operations + /// + /// Converts the given decimal value (provided as a string) to the nearest floating point approximation + /// the returned fp assumes the given mantissa and exponent size + /// + /// + /// + /// + /// public static BigFloat Round(String value, int mantissaSize, int exponentSize) { int i = value.IndexOf('.'); if (i == -1) return Round(BIM.Parse(value), 0, mantissaSize, exponentSize); - return Round(BIM.Parse(value.Substring(0, i - 1)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), mantissaSize, exponentSize); + return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), mantissaSize, exponentSize); } /// - /// Converts value.dec_value to a float with mantissaSize, exponentSize + /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize /// Returns the result of this calculation /// /// @@ -178,8 +215,54 @@ namespace Microsoft.Basetypes /// /// public static BigFloat Round(BIM value, BIM dec_value, int mantissaSize, int exponentSize) - { //TODO: round the given decimal to the nearest fp value - return new BigFloat(0, 0, mantissaSize, exponentSize); + { + int exp = 0; + BIM one = new BIM(1); + BIM ten = new BIM(10); + BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations + + //First, determine the exponent + while (value > one) { //Divide by two, increment exponent by 1 + if (!(value % two).IsZero) { //Add "1.0" to the decimal + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + dec_value = dec_value + dec_max; + } + value = value / two; + if (!(dec_value % ten).IsZero) + dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division + dec_value = dec_value / two; + exp++; + } + if (value.IsZero && !dec_value.IsZero) { + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + while (value.IsZero) {//Multiply by two, decrement exponent by 1 + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + one; + } + exp--; + } + } + + //Second, calculate the mantissa + value = new BIM(0); //remove implicit bit + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + for (int i = mantissaSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the mantissa is fully calculated + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation + } + } + + return new BigFloat(value, exp, mantissaSize, exponentSize); } // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). @@ -336,16 +419,18 @@ namespace Microsoft.Basetypes int e1 = x.Exponent; BIM m2 = y.Mantissa; int e2 = y.Exponent; - if (e2 < e1) { + m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit + m2 = m2 + two_n(y.mantissaSize + 1); + if (e2 > e1) { m1 = y.Mantissa; e1 = y.Exponent; m2 = x.Mantissa; e2 = x.Exponent; } - while (e2 > e1) { - m2 = m2 * two; - e2 = e2 - 1; + while (e2 < e1) { + m2 = m2 / two; + e2++; } return new BigFloat(m1 + m2, e1, Math.Max(x.MantissaSize, y.MantissaSize), Math.Max(x.ExponentSize, y.ExponentSize)); @@ -358,7 +443,6 @@ namespace Microsoft.Basetypes [Pure] public static BigFloat operator *(BigFloat x, BigFloat y) { - //TODO: modify for correct fp functionality return new BigFloat(x.Mantissa * y.Mantissa, x.Exponent + y.Exponent, Math.Max(x.MantissaSize, y.MantissaSize), Math.Max(x.ExponentSize, y.ExponentSize)); } @@ -368,13 +452,13 @@ namespace Microsoft.Basetypes public bool IsPositive { get { - return (Mantissa > BIM.Zero); + return (!isNegative); } } public bool IsNegative { get { - return (Mantissa < BIM.Zero); + return (isNegative); } } @@ -386,14 +470,13 @@ namespace Microsoft.Basetypes [Pure] public int CompareTo(BigFloat that) { - //TODO: Modify for correct fp functionality - if (this.mantissa == that.mantissa && this.exponent == that.exponent) { + if (this.exponent > that.exponent) + return 1; + if (this.exponent < that.exponent) + return -1; + if (this.Mantissa == that.Mantissa) return 0; - } - else { - BigFloat d = this - that; - return d.IsNegative ? -1 : 1; - } + return this.Mantissa > that.Mantissa ? 1 : -1; } [Pure] -- cgit v1.2.3