diff options
| -rw-r--r-- | Source/Basetypes/BigDec.cs | 23 | ||||
| -rw-r--r-- | Source/UnitTests/BasetypesTests/BigDecTests.cs | 31 |
2 files changed, 50 insertions, 4 deletions
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index 4206b2f2..0aeea8b1 100644 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -6,6 +6,7 @@ using System;
using System.Text;
using System.Diagnostics.Contracts;
+using System.Diagnostics;
namespace Microsoft.Basetypes {
@@ -141,6 +142,13 @@ namespace Microsoft.Basetypes { ////////////////////////////////////////////////////////////////////////////
// Conversion operations
+ // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
+ /// <summary>
+ /// Computes the floor and ceiling of this BigDec. Note the choice of rounding towards negative
+ /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+ /// </summary>
+ /// <param name="floor">The Floor (rounded towards negative infinity)</param>
+ /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
public void FloorCeiling(out BIM floor, out BIM ceiling) {
BIM n = this.mantissa;
int e = this.exponent;
@@ -153,13 +161,20 @@ namespace Microsoft.Basetypes { }
floor = ceiling = n;
} else {
- // it's a non-zero integer, so the ceiling is one more than the fllor
+ // it's a non-zero integer, so the ceiling is one more than the floor
for (; e < 0 && !n.IsZero; e++) {
- n = n / ten; // since we're dividing by a positive number, this will round down
+ n = n / ten; // Division rounds towards negative infinity
+ }
+
+ if (this.mantissa >= 0) {
+ floor = n;
+ ceiling = n + 1;
+ } else {
+ ceiling = n;
+ floor = n - 1;
}
- floor = n;
- ceiling = n + 1;
}
+ Debug.Assert(floor <= ceiling, "Invariant was not maintained");
}
[Pure]
diff --git a/Source/UnitTests/BasetypesTests/BigDecTests.cs b/Source/UnitTests/BasetypesTests/BigDecTests.cs index cee80216..4c26a21a 100644 --- a/Source/UnitTests/BasetypesTests/BigDecTests.cs +++ b/Source/UnitTests/BasetypesTests/BigDecTests.cs @@ -24,6 +24,37 @@ namespace BasetypesTests Assert.AreEqual(-1, v.Exponent); Assert.AreEqual(new BigInteger(15.0), v.Mantissa); } + + [TestCase("0.0", 0, 0)] + [TestCase("5.0", 5, 5)] + [TestCase("5.5", 5, 6)] + [TestCase("5.9", 5, 6)] + [TestCase("15e1", 150, 150)] + [TestCase("15e-1", 1, 2)] + // Negative values + // Note we expect floor to round towards negative infinity + // and ceiling to round towards positive infinity + [TestCase("-15e-1", -2, -1)] + [TestCase("-5.0", -5, -5)] + [TestCase("-5e0", -5, -5)] + [TestCase("-5e1", -50, -50)] + [TestCase("-5e-1", -1, 0)] + [TestCase("-5.5", -6, -5)] + [TestCase("-5.9", -6, -5)] + public void FloorAndCeil(string value, int expectedFloor, int expectedCeiling) + { + var v = BigDec.FromString(value); + if (value.StartsWith ("-")) + Assert.IsTrue(v.IsNegative); + else + Assert.IsTrue(v.IsPositive || v.IsZero); + + BigInteger floor = 0; + BigInteger ceiling = 0; + v.FloorCeiling(out floor, out ceiling); + Assert.AreEqual(new BigInteger(expectedFloor), floor); + Assert.AreEqual(new BigInteger(expectedCeiling), ceiling); + } } } |