1 files changed, 380 insertions, 380 deletions
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs
index 0aeea8b1..e4666793 100644
--- a/Source/Basetypes/BigDec.cs
+++ b/Source/Basetypes/BigDec.cs
@@ -1,380 +1,380 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
-
-
-namespace Microsoft.Basetypes {
-  using BIM = System.Numerics.BigInteger;
-
-
-  /// <summary>
-  /// A representation of decimal values.
-  /// </summary>
-  public struct BigDec {
-
-    // the internal representation
-    [Rep]
-    internal readonly BIM mantissa;
-    [Rep]
-    internal readonly int exponent;
-
-    public BIM Mantissa {
-      get {
-        return mantissa;
-      }
-    }
-
-    public int Exponent {
-      get {
-        return exponent;
-      }
-    }
-
-    public static readonly BigDec ZERO = FromInt(0);
-    private static readonly BIM ten = new BIM(10);
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Constructors
-
-    [Pure]
-    public static BigDec FromInt(int v) {
-      return new BigDec(v, 0);
-    }
-
-    [Pure]
-    public static BigDec FromBigInt(BIM v) {
-      return new BigDec(v, 0);
-    }
-
-    [Pure]
-    public static BigDec FromString(string v) {
-      if (v == null) throw new FormatException();
-
-      BIM integral = BIM.Zero;
-      BIM fraction = BIM.Zero;
-      int exponent = 0;
-
-      int len = v.Length;
-
-      int i = v.IndexOf('e');
-      if (i >= 0) {
-        if (i + 1 == v.Length) throw new FormatException();
-        exponent = Int32.Parse(v.Substring(i + 1, len - i - 1));
-        len = i;
-      }
-
-      int fractionLen = 0;
-      i = v.IndexOf('.');
-      if (i >= 0) {
-        if (i + 1 == v.Length) throw new FormatException();
-        fractionLen = len - i - 1;
-        fraction = BIM.Parse(v.Substring(i + 1, fractionLen));
-        len = i;
-      }
-
-      integral = BIM.Parse(v.Substring(0, len));
-
-      if (!fraction.IsZero) {
-        while (fractionLen > 0) {
-          integral = integral * ten;
-          exponent = exponent - 1;
-          fractionLen = fractionLen - 1;
-        }
-      }
-
-      if (integral.Sign == -1) {
-        return new BigDec(integral - fraction, exponent);
-      }
-      else {
-        return new BigDec(integral + fraction, exponent);
-      }
-    }
-
-    internal BigDec(BIM mantissa, int exponent) {
-      if (mantissa.IsZero) {
-        this.mantissa = mantissa;
-        this.exponent = 0;
-      }
-      else {
-        while (mantissa % ten == BIM.Zero) {
-          mantissa = mantissa / ten;
-          exponent = exponent + 1;
-        }
-        this.mantissa = mantissa;
-        this.exponent = exponent;
-      }
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Basic object operations
-
-    [Pure]
-    [Reads(ReadsAttribute.Reads.Nothing)]
-    public override bool Equals(object obj) {
-      if (obj == null)
-        return false;
-      if (!(obj is BigDec))
-        return false;
-
-      return (this == (BigDec)obj);
-    }
-
-    [Pure]
-    public override int GetHashCode() {
-      return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode();
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // 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;
-      if (n.IsZero) {
-        floor = ceiling = n;
-      } else if (0 <= e) {
-        // it's an integer
-        for (; 0 < e; e--) {
-          n = n * ten;
-        }
-        floor = ceiling = n;
-      } else {
-        // it's a non-zero integer, so the ceiling is one more than the floor
-        for (; e < 0 && !n.IsZero; e++) {
-          n = n / ten;  // Division rounds towards negative infinity
-        }
-
-        if (this.mantissa >= 0) {
-          floor = n;
-          ceiling = n + 1;
-        } else {
-          ceiling = n;
-          floor = n - 1;
-        }
-      }
-      Debug.Assert(floor <= ceiling, "Invariant was not maintained");
-    }
-
-    [Pure]
-    public String ToDecimalString(int maxDigits) {
-      string s = this.mantissa.ToString();
-      int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1;
-      BIM max = BIM.Pow(10, maxDigits);
-      BIM min = -max;
-
-      if (this.exponent >= 0) {
-        if (maxDigits < digits || maxDigits - digits < this.exponent) {
-          return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
-        }
-        else {
-          return String.Format("{0}{1}.0", s, new string('0', this.exponent));
-        }
-      }
-      else {
-        int exp = -this.exponent;
-
-        if (exp < digits) {
-          int intDigits = digits - exp;
-          if (maxDigits < intDigits) {
-            return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
-          }
-          else {
-            int fracDigits = Math.Min(maxDigits, digits - intDigits);
-            return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
-          }
-        }
-        else {
-          int fracDigits = Math.Min(maxDigits, digits);
-          return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
-        }
-      }
-    }
-
-    [Pure]
-    public string ToDecimalString() {
-      string m = this.mantissa.ToString();
-      var e = this.exponent;
-      if (0 <= this.exponent) {
-        return m + Zeros(e) + ".0";
-      } else {
-        e = -e;
-        // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)
-        var maxK = e < m.Length ? e : m.Length - 1;
-        var last = m.Length - 1;
-        var k = 0;
-        while (k < maxK && m[last - k] == '0') {
-          k++;
-        }
-        if (0 < k) {
-          // chop off the suffix of k zeros from m and adjust e accordingly
-          m = m.Substring(0, m.Length - k);
-          e -= k;
-        }
-        if (e == 0) {
-          return m;
-        } else if (e < m.Length) {
-          var n = m.Length - e;
-          return m.Substring(0, n) + "." + m.Substring(n);
-        } else {
-          return "0." + Zeros(e - m.Length) + m;
-        }
-      }
-    }
-
-    [Pure]
-    public static string Zeros(int n) {
-      Contract.Requires(0 <= n);
-      if (n <= 10) {
-        var tenZeros = "0000000000";
-        return tenZeros.Substring(0, n);
-      } else {
-        var d = n / 2;
-        var s = Zeros(d);
-        if (n % 2 == 0) {
-          return s + s;
-        } else {
-          return s + s + "0";
-        }
-      }
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Basic arithmetic operations
-
-    [Pure]
-    public BigDec Abs {
-      get {
-        return new BigDec(BIM.Abs(this.mantissa), this.exponent);
-      }
-    }
-
-    [Pure]
-    public BigDec Negate {
-      get {
-        return new BigDec(BIM.Negate(this.mantissa), this.exponent);
-      }
-    }
-
-    [Pure]
-    public static BigDec operator -(BigDec x) {
-      return x.Negate;
-    }
-
-    [Pure]
-    public static BigDec operator +(BigDec x, BigDec y) {
-      BIM m1 = x.mantissa;
-      int e1 = x.exponent;
-      BIM m2 = y.mantissa;
-      int e2 = y.exponent;
-      if (e2 < e1) {
-        m1 = y.mantissa;
-        e1 = y.exponent;
-        m2 = x.mantissa;
-        e2 = x.exponent;
-      }
-
-      while (e2 > e1) {
-        m2 = m2 * ten;
-        e2 = e2 - 1;
-      }
-
-      return new BigDec(m1 + m2, e1);
-    }
-
-    [Pure]
-    public static BigDec operator -(BigDec x, BigDec y) {
-      return x + y.Negate;
-    }
-
-    [Pure]
-    public static BigDec operator *(BigDec x, BigDec y) {
-      return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent);
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Some basic comparison operations
-
-    public bool IsPositive {
-      get {
-        return (this.mantissa > BIM.Zero);
-      }
-    }
-
-    public bool IsNegative {
-      get {
-        return (this.mantissa < BIM.Zero);
-      }
-    }
-
-    public bool IsZero {
-      get {
-        return this.mantissa.IsZero;
-      }
-    }
-
-    [Pure]
-    public int CompareTo(BigDec that) {
-      if (this.mantissa == that.mantissa && this.exponent == that.exponent) {
-        return 0;
-      }
-      else {
-        BigDec d = this - that;
-        return d.IsNegative ? -1 : 1;
-      }
-    }
-
-    [Pure]
-    public static bool operator ==(BigDec x, BigDec y) {
-      return x.CompareTo(y) == 0;
-    }
-
-    [Pure]
-    public static bool operator !=(BigDec x, BigDec y) {
-      return x.CompareTo(y) != 0;
-    }
-
-    [Pure]
-    public static bool operator <(BigDec x, BigDec y) {
-      return x.CompareTo(y) < 0;
-    }
-
-    [Pure]
-    public static bool operator >(BigDec x, BigDec y) {
-      return x.CompareTo(y) > 0;
-    }
-
-    [Pure]
-    public static bool operator <=(BigDec x, BigDec y) {
-      return x.CompareTo(y) <= 0;
-    }
-
-    [Pure]
-    public static bool operator >=(BigDec x, BigDec y) {
-      return x.CompareTo(y) >= 0;
-    }
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+
+namespace Microsoft.Basetypes {
+  using BIM = System.Numerics.BigInteger;
+
+
+  /// <summary>
+  /// A representation of decimal values.
+  /// </summary>
+  public struct BigDec {
+
+    // the internal representation
+    [Rep]
+    internal readonly BIM mantissa;
+    [Rep]
+    internal readonly int exponent;
+
+    public BIM Mantissa {
+      get {
+        return mantissa;
+      }
+    }
+
+    public int Exponent {
+      get {
+        return exponent;
+      }
+    }
+
+    public static readonly BigDec ZERO = FromInt(0);
+    private static readonly BIM ten = new BIM(10);
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Constructors
+
+    [Pure]
+    public static BigDec FromInt(int v) {
+      return new BigDec(v, 0);
+    }
+
+    [Pure]
+    public static BigDec FromBigInt(BIM v) {
+      return new BigDec(v, 0);
+    }
+
+    [Pure]
+    public static BigDec FromString(string v) {
+      if (v == null) throw new FormatException();
+
+      BIM integral = BIM.Zero;
+      BIM fraction = BIM.Zero;
+      int exponent = 0;
+
+      int len = v.Length;
+
+      int i = v.IndexOf('e');
+      if (i >= 0) {
+        if (i + 1 == v.Length) throw new FormatException();
+        exponent = Int32.Parse(v.Substring(i + 1, len - i - 1));
+        len = i;
+      }
+
+      int fractionLen = 0;
+      i = v.IndexOf('.');
+      if (i >= 0) {
+        if (i + 1 == v.Length) throw new FormatException();
+        fractionLen = len - i - 1;
+        fraction = BIM.Parse(v.Substring(i + 1, fractionLen));
+        len = i;
+      }
+
+      integral = BIM.Parse(v.Substring(0, len));
+
+      if (!fraction.IsZero) {
+        while (fractionLen > 0) {
+          integral = integral * ten;
+          exponent = exponent - 1;
+          fractionLen = fractionLen - 1;
+        }
+      }
+
+      if (integral.Sign == -1) {
+        return new BigDec(integral - fraction, exponent);
+      }
+      else {
+        return new BigDec(integral + fraction, exponent);
+      }
+    }
+
+    internal BigDec(BIM mantissa, int exponent) {
+      if (mantissa.IsZero) {
+        this.mantissa = mantissa;
+        this.exponent = 0;
+      }
+      else {
+        while (mantissa % ten == BIM.Zero) {
+          mantissa = mantissa / ten;
+          exponent = exponent + 1;
+        }
+        this.mantissa = mantissa;
+        this.exponent = exponent;
+      }
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic object operations
+
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override bool Equals(object obj) {
+      if (obj == null)
+        return false;
+      if (!(obj is BigDec))
+        return false;
+
+      return (this == (BigDec)obj);
+    }
+
+    [Pure]
+    public override int GetHashCode() {
+      return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode();
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // 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;
+      if (n.IsZero) {
+        floor = ceiling = n;
+      } else if (0 <= e) {
+        // it's an integer
+        for (; 0 < e; e--) {
+          n = n * ten;
+        }
+        floor = ceiling = n;
+      } else {
+        // it's a non-zero integer, so the ceiling is one more than the floor
+        for (; e < 0 && !n.IsZero; e++) {
+          n = n / ten;  // Division rounds towards negative infinity
+        }
+
+        if (this.mantissa >= 0) {
+          floor = n;
+          ceiling = n + 1;
+        } else {
+          ceiling = n;
+          floor = n - 1;
+        }
+      }
+      Debug.Assert(floor <= ceiling, "Invariant was not maintained");
+    }
+
+    [Pure]
+    public String ToDecimalString(int maxDigits) {
+      string s = this.mantissa.ToString();
+      int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1;
+      BIM max = BIM.Pow(10, maxDigits);
+      BIM min = -max;
+
+      if (this.exponent >= 0) {
+        if (maxDigits < digits || maxDigits - digits < this.exponent) {
+          return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
+        }
+        else {
+          return String.Format("{0}{1}.0", s, new string('0', this.exponent));
+        }
+      }
+      else {
+        int exp = -this.exponent;
+
+        if (exp < digits) {
+          int intDigits = digits - exp;
+          if (maxDigits < intDigits) {
+            return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
+          }
+          else {
+            int fracDigits = Math.Min(maxDigits, digits - intDigits);
+            return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
+          }
+        }
+        else {
+          int fracDigits = Math.Min(maxDigits, digits);
+          return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
+        }
+      }
+    }
+
+    [Pure]
+    public string ToDecimalString() {
+      string m = this.mantissa.ToString();
+      var e = this.exponent;
+      if (0 <= this.exponent) {
+        return m + Zeros(e) + ".0";
+      } else {
+        e = -e;
+        // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)
+        var maxK = e < m.Length ? e : m.Length - 1;
+        var last = m.Length - 1;
+        var k = 0;
+        while (k < maxK && m[last - k] == '0') {
+          k++;
+        }
+        if (0 < k) {
+          // chop off the suffix of k zeros from m and adjust e accordingly
+          m = m.Substring(0, m.Length - k);
+          e -= k;
+        }
+        if (e == 0) {
+          return m;
+        } else if (e < m.Length) {
+          var n = m.Length - e;
+          return m.Substring(0, n) + "." + m.Substring(n);
+        } else {
+          return "0." + Zeros(e - m.Length) + m;
+        }
+      }
+    }
+
+    [Pure]
+    public static string Zeros(int n) {
+      Contract.Requires(0 <= n);
+      if (n <= 10) {
+        var tenZeros = "0000000000";
+        return tenZeros.Substring(0, n);
+      } else {
+        var d = n / 2;
+        var s = Zeros(d);
+        if (n % 2 == 0) {
+          return s + s;
+        } else {
+          return s + s + "0";
+        }
+      }
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic arithmetic operations
+
+    [Pure]
+    public BigDec Abs {
+      get {
+        return new BigDec(BIM.Abs(this.mantissa), this.exponent);
+      }
+    }
+
+    [Pure]
+    public BigDec Negate {
+      get {
+        return new BigDec(BIM.Negate(this.mantissa), this.exponent);
+      }
+    }
+
+    [Pure]
+    public static BigDec operator -(BigDec x) {
+      return x.Negate;
+    }
+
+    [Pure]
+    public static BigDec operator +(BigDec x, BigDec y) {
+      BIM m1 = x.mantissa;
+      int e1 = x.exponent;
+      BIM m2 = y.mantissa;
+      int e2 = y.exponent;
+      if (e2 < e1) {
+        m1 = y.mantissa;
+        e1 = y.exponent;
+        m2 = x.mantissa;
+        e2 = x.exponent;
+      }
+
+      while (e2 > e1) {
+        m2 = m2 * ten;
+        e2 = e2 - 1;
+      }
+
+      return new BigDec(m1 + m2, e1);
+    }
+
+    [Pure]
+    public static BigDec operator -(BigDec x, BigDec y) {
+      return x + y.Negate;
+    }
+
+    [Pure]
+    public static BigDec operator *(BigDec x, BigDec y) {
+      return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent);
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Some basic comparison operations
+
+    public bool IsPositive {
+      get {
+        return (this.mantissa > BIM.Zero);
+      }
+    }
+
+    public bool IsNegative {
+      get {
+        return (this.mantissa < BIM.Zero);
+      }
+    }
+
+    public bool IsZero {
+      get {
+        return this.mantissa.IsZero;
+      }
+    }
+
+    [Pure]
+    public int CompareTo(BigDec that) {
+      if (this.mantissa == that.mantissa && this.exponent == that.exponent) {
+        return 0;
+      }
+      else {
+        BigDec d = this - that;
+        return d.IsNegative ? -1 : 1;
+      }
+    }
+
+    [Pure]
+    public static bool operator ==(BigDec x, BigDec y) {
+      return x.CompareTo(y) == 0;
+    }
+
+    [Pure]
+    public static bool operator !=(BigDec x, BigDec y) {
+      return x.CompareTo(y) != 0;
+    }
+
+    [Pure]
+    public static bool operator <(BigDec x, BigDec y) {
+      return x.CompareTo(y) < 0;
+    }
+
+    [Pure]
+    public static bool operator >(BigDec x, BigDec y) {
+      return x.CompareTo(y) > 0;
+    }
+
+    [Pure]
+    public static bool operator <=(BigDec x, BigDec y) {
+      return x.CompareTo(y) <= 0;
+    }
+
+    [Pure]
+    public static bool operator >=(BigDec x, BigDec y) {
+      return x.CompareTo(y) >= 0;
+    }
+  }
+}