Modified BigFloat to avoid evaluating the floating point value before sending it to z3

6 files changed, 505 insertions, 554 deletions

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 33860a4f..e9d5e670 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -1,516 +1,490 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
-
-namespace Microsoft.Basetypes
-{
-  using BIM = System.Numerics.BigInteger;
-    
-  /// <summary>
-  /// A representation of a 32-bit floating point value
-  /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa
-  /// </summary>
-  public struct BigFloat
-  {
-    //Please note that this code outline is copy-pasted from BigDec.cs
-
-    // the internal representation
-    [Rep]
-    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 mantissaSize;
-    [Rep]
-    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 {
-        return isNegative ? -mantissa : mantissa;
-      }
-    }
-
-    public int Exponent {
-      get {
-        return exponent - (int)Math.Pow(2, exponentSize - 1); //account for shift
-      }
-    }
-
-    public int MantissaSize
-    {
-      get
-      {
-        return mantissaSize;
-      }
-    }
-
-    public int ExponentSize
-    {
-      get
-      {
-        return exponentSize;
-      }
-    }
-
-    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;
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Constructors
-
-    //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
-
-    [Pure]
-    public static BigFloat FromInt(int v) {
-      return new BigFloat(v, 0, 24, 8); //TODO: modify for correct fp representation
-    }
-
-    [Pure]
-    public static BigFloat FromBigInt(BIM v) {
-      return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation
-    }
-
-    public static BigFloat FromBigDec(BIM v)
-    {
-      return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation
-    }
-
-    [Pure]
-    public static BigFloat FromString(string v) {
-      String[] vals = v.Split(' ');
-      if (vals.Length == 0 || vals.Length > 4)
-        throw new FormatException();
-      try
-      {
-        switch (vals.Length) {
-          case 1:
-            return Round(vals[0], 8, 24); 
-          case 2:
-            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);
-          case 3:
-            return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
-          case 4:
-            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
-          default:
-            throw new FormatException(); //Unreachable
-        }
-      }
-      catch (Exception) { //Catch parsing errors
-        throw new FormatException();
-      }
-    }
-
-    internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) {
-      this.exponentSize = exponentSize;
-      this.exponent = exponent + (int)Math.Pow(2, exponentSize - 1);
-      this.mantissa = mantissa;
-      this.mantissaSize = mantissaSize;
-      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 > 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 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; }
-
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Basic object operations
-
-    [Pure]
-    [Reads(ReadsAttribute.Reads.Nothing)]
-    public override bool Equals(object obj) {
-      if (obj == null)
-        return false;
-      if (!(obj is BigFloat))
-        return false;
-
-      return (this == (BigFloat)obj);
-    }
-
-    [Pure]
-    public override int GetHashCode() {
-      return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode();
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Conversion operations
-
-    /// <summary>
-    /// 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
-    /// </summary>
-    /// <param name="value"></param>
-    /// <param name="mantissaSize"></param>
-    /// <param name="exponentSize"></param>
-    /// <returns></returns>
-    public static BigFloat Round(String value, int exponentSize, int mantissaSize)
-    {
-      int i = value.IndexOf('.');
-      if (i == -1)
-        return Round(BIM.Parse(value), 0, exponentSize, mantissaSize);
-      return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, mantissaSize);
-    }
-
-    /// <summary>
-    /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize
-    /// Returns the result of this calculation
-    /// </summary>
-    /// <param name="value"></param>
-    /// <param name="power"></param>
-    /// <param name="mantissaSize"></param>
-    /// <param name="exponentSize"></param>
-    /// <returns></returns>
-    public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)
-    {
-      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(exp, value, exponentSize, mantissaSize);
-    }
-
-    // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
-    /// <summary>
-    /// 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.
-    /// </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) {
-      //TODO: fix for fp functionality
-      BIM n = Mantissa;
-      int e = Exponent;
-      if (n.IsZero) {
-        floor = ceiling = n;
-      } else if (0 <= e) {
-        // it's an integer
-        for (; 0 < e; e--) {
-          n = n * two;
-        }
-        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 / two;  // Division rounds towards negative infinity
-        }
-
-        if (!isNegative) {
-          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) {
-      //TODO: fix for fp functionality
-      string s = Mantissa.ToString();
-      int digits = (isNegative) ?  s.Length - 1 : s.Length;
-      BIM max = BIM.Pow(10, maxDigits);
-      BIM min = -max;
-
-      if (Exponent >= 0) {
-        if (maxDigits < digits || maxDigits - digits < Exponent) {
-          return String.Format("{0}.0", (!isNegative) ? max.ToString() : min.ToString());
-        }
-        else {
-          return String.Format("{0}{1}.0", s, new string('0', Exponent));
-        }
-      }
-      else {
-        int exp = -Exponent;
-
-        if (exp < digits) {
-          int intDigits = digits - exp;
-          if (maxDigits < intDigits) {
-            return String.Format("{0}.0", (!isNegative) ? 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() {
-      //TODO: fix for fp functionality
-      string m = Mantissa.ToString();
-      var e = Exponent;
-      if (0 <= 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) {
-      //TODO: fix for fp functionality
-      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 BigFloat Abs {
-      //TODO: fix for fp functionality
-      get {
-        return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);
-      }
-    }
-
-    [Pure]
-    public BigFloat Negate {
-      //TODO: Modify for correct fp functionality
-      get {
-        return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);
-      }
-    }
-
-    [Pure]
-    public static BigFloat operator -(BigFloat x) {
-      return x.Negate;
-    }
-
-    [Pure]
-    public static BigFloat operator +(BigFloat x, BigFloat y) {
-      //TODO: Modify for correct fp functionality
-      Contract.Requires(x.ExponentSize == y.ExponentSize);
-      Contract.Requires(x.MantissaSize == y.MantissaSize);
-      BIM m1 = x.Mantissa;
-      int e1 = x.Exponent;
-      BIM m2 = y.Mantissa;
-      int e2 = y.Exponent;
-      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++;
-      }
-
-      return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);
-    }
-
-    [Pure]
-    public static BigFloat operator -(BigFloat x, BigFloat y) {
-      return x + y.Negate;
-    }
-
-    [Pure]
-    public static BigFloat operator *(BigFloat x, BigFloat y) {
-      Contract.Requires(x.ExponentSize == y.ExponentSize);
-      Contract.Requires(x.MantissaSize == y.MantissaSize);
-      return new BigFloat(x.Exponent + y.Exponent, x.Mantissa * y.Mantissa, x.MantissaSize, x.ExponentSize);
-    }
-
-
-    ////////////////////////////////////////////////////////////////////////////
-    // Some basic comparison operations
-
-    public bool IsPositive {
-      get {
-        return (!isNegative);
-      }
-    }
-
-    public bool IsNegative {
-      get {
-        return (isNegative);
-      }
-    }
-
-    public bool IsZero {
-      get {
-        return Mantissa.IsZero && Exponent == 0;
-      }
-    }
-
-    [Pure]
-    public int CompareTo(BigFloat that) {
-      if (this.exponent > that.exponent)
-        return 1;
-      if (this.exponent < that.exponent)
-        return -1;
-      if (this.Mantissa == that.Mantissa)
-        return 0;
-      return this.Mantissa > that.Mantissa ? 1 : -1;
-    }
-
-    [Pure]
-    public static bool operator ==(BigFloat x, BigFloat y) {
-      return x.CompareTo(y) == 0;
-    }
-
-    [Pure]
-    public static bool operator !=(BigFloat x, BigFloat y) {
-      return x.CompareTo(y) != 0;
-    }
-
-    [Pure]
-    public static bool operator <(BigFloat x, BigFloat y) {
-      return x.CompareTo(y) < 0;
-    }
-
-    [Pure]
-    public static bool operator >(BigFloat x, BigFloat y) {
-      return x.CompareTo(y) > 0;
-    }
-
-    [Pure]
-    public static bool operator <=(BigFloat x, BigFloat y) {
-      return x.CompareTo(y) <= 0;
-    }
-
-    [Pure]
-    public static bool operator >=(BigFloat x, BigFloat y) {
-      return x.CompareTo(y) >= 0;
-    }
-  }
-}
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+using System.Diagnostics;

+

+namespace Microsoft.Basetypes

+{

+  using BIM = System.Numerics.BigInteger;

+    

+  /// <summary>

+  /// A representation of a 32-bit floating point value

+  /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa

+  /// </summary>

+  public struct BigFloat

+  {

+    //Please note that this code outline is copy-pasted from BigDec.cs

+

+    // the internal representation

+    [Rep]

+    internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left)

+    [Rep]

+    internal readonly int mantissaSize;

+    [Rep]

+    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

+    [Rep]

+    internal readonly BigDec dec_value;

+    [Rep]

+    internal readonly bool isDec;

+

+    public BIM Mantissa {

+      get {

+        return mantissa;

+      }

+    }

+

+    public int Exponent {

+      get {

+        return exponent;

+      }

+    }

+

+    public int MantissaSize {

+      get {

+        return mantissaSize;

+      }

+    }

+

+    public int ExponentSize {

+      get {

+        return exponentSize;

+      }

+    }

+

+    public BigDec Decimal {

+      get {

+        return dec_value;

+      }

+    }

+

+    public bool IsDec {

+      get {

+        return IsDec;

+      }

+    }

+

+    public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero

+

+    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;

+    }

+

+

+    ////////////////////////////////////////////////////////////////////////////

+    // Constructors

+

+    //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

+

+    [Pure]

+    public static BigFloat FromInt(int v) {

+      return new BigFloat(v, 0, 24, 8);

+    }

+

+    [Pure]

+    public static BigFloat FromBigInt(BIM v) {

+      return new BigFloat(0, v, 8, 24);

+    }

+

+    public static BigFloat FromBigDec(BigDec v)

+    {

+      return new BigFloat(v, 8, 24);

+    }

+

+    [Pure]

+    public static BigFloat FromString(string v) {

+      String[] vals = v.Split(' ');

+      if (vals.Length == 0 || vals.Length > 4)

+        throw new FormatException();

+      try

+      {

+        switch (vals.Length) {

+          case 1:

+            return new BigFloat(BigDec.FromString(vals[0]), 8, 24); 

+          case 2:

+            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);

+          case 3:

+            return new BigFloat(BigDec.FromString(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]));

+          case 4:

+            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));

+          default:

+            throw new FormatException(); //Unreachable

+        }

+      }

+      catch (Exception) { //Catch parsing errors

+        throw new FormatException();

+      }

+    }

+

+    internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) {

+      this.exponentSize = exponentSize;

+      this.exponent = exponent;

+      this.mantissa = mantissa;

+      this.mantissaSize = mantissaSize;

+      this.isDec = false;

+      this.dec_value = BigDec.ZERO;

+    }

+

+    internal BigFloat(BigDec dec_value, int exponentSize, int mantissaSize) {

+      this.exponentSize = exponentSize;

+      this.mantissaSize = mantissaSize;

+      this.exponent = 0;

+      this.mantissa = 0;

+      this.isDec = true;

+      this.dec_value = dec_value;

+    }

+

+    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; }

+

+

+

+    ////////////////////////////////////////////////////////////////////////////

+    // Basic object operations

+

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object obj) {

+      if (obj == null)

+        return false;

+      if (!(obj is BigFloat))

+        return false;

+

+      return (this == (BigFloat)obj);

+    }

+

+    [Pure]

+    public override int GetHashCode() {

+      return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode();

+    }

+

+    [Pure]

+    public override string/*!*/ ToString() {

+      Contract.Ensures(Contract.Result<string>() != null);

+      return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());

+    }

+

+

+    ////////////////////////////////////////////////////////////////////////////

+    // Conversion operations

+

+    /// <summary>

+    /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!

+    /// 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

+    /// </summary>

+    /// <param name="value"></param>

+    /// <param name="mantissaSize"></param>

+    /// <param name="exponentSize"></param>

+    /// <returns></returns>

+    public static BigFloat Round(String value, int exponentSize, int mantissaSize)

+    {

+      int i = value.IndexOf('.');

+      if (i == -1)

+        return Round(BIM.Parse(value), 0, exponentSize, mantissaSize);

+      return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, mantissaSize);

+    }

+

+    /// <summary>

+    /// NOTE:  THIS METHOD MAY NOT WORK AS EXPECTED!!!!

+    /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize

+    /// Returns the result of this calculation

+    /// </summary>

+    /// <param name="value"></param>

+    /// <param name="power"></param>

+    /// <param name="mantissaSize"></param>

+    /// <param name="exponentSize"></param>

+    /// <returns></returns>

+    public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)

+    {

+      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(exp, value, exponentSize, mantissaSize);

+    }

+

+    // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).

+    /// <summary>

+    /// NOTE:  THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!!

+    /// 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.

+    /// </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) {

+      //TODO: fix for fp functionality

+      BIM n = Mantissa;

+      int e = Exponent;

+      if (n.IsZero) {

+        floor = ceiling = n;

+      } else if (0 <= e) {

+        // it's an integer

+        for (; 0 < e; e--) {

+          n = n * two;

+        }

+        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 / two;  // Division rounds towards negative infinity

+        }

+

+        if (!IsNegative) {

+          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) {

+      //TODO: fix for fp functionality 

+      {

+        throw new NotImplementedException();

+      }

+    }

+

+    [Pure]

+    public string ToDecimalString() {

+      //TODO: fix for fp functionality

+      string m = Mantissa.ToString();

+      var e = Exponent;

+      if (0 <= 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) {

+      //TODO: fix for fp functionality

+      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 BigFloat Abs {

+      //TODO: fix for fp functionality

+      get {

+        return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);

+      }

+    }

+

+    [Pure]

+    public BigFloat Negate {

+      //TODO: Modify for correct fp functionality

+      get {

+        return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);

+      }

+    }

+

+    [Pure]

+    public static BigFloat operator -(BigFloat x) {

+      return x.Negate;

+    }

+

+    [Pure]

+    public static BigFloat operator +(BigFloat x, BigFloat y) {

+      //TODO: Modify for correct fp functionality

+      Contract.Requires(x.ExponentSize == y.ExponentSize);

+      Contract.Requires(x.MantissaSize == y.MantissaSize);

+      BIM m1 = x.Mantissa;

+      int e1 = x.Exponent;

+      BIM m2 = y.Mantissa;

+      int e2 = y.Exponent;

+      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++;

+      }

+

+      return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);

+    }

+

+    [Pure]

+    public static BigFloat operator -(BigFloat x, BigFloat y) {

+      return x + y.Negate;

+    }

+

+    [Pure]

+    public static BigFloat operator *(BigFloat x, BigFloat y) {

+      Contract.Requires(x.ExponentSize == y.ExponentSize);

+      Contract.Requires(x.MantissaSize == y.MantissaSize);

+      return new BigFloat(x.Exponent + y.Exponent, x.Mantissa * y.Mantissa, x.MantissaSize, x.ExponentSize);

+    }

+

+

+    ////////////////////////////////////////////////////////////////////////////

+    // Some basic comparison operations

+

+    public bool IsPositive {

+      get {

+        return !IsNegative;

+      }

+    }

+

+    public bool IsNegative {

+      get {

+        return (isDec && dec_value >= BigDec.ZERO) || mantissa >= 0;

+      }

+    }

+

+    public bool IsZero {

+      get {

+        return Mantissa.IsZero && Exponent == 0;

+      }

+    }

+

+    [Pure]

+    public int CompareTo(BigFloat that) {

+      if (this.exponent > that.exponent)

+        return 1;

+      if (this.exponent < that.exponent)

+        return -1;

+      if (this.Mantissa == that.Mantissa)

+        return 0;

+      return this.Mantissa > that.Mantissa ? 1 : -1;

+    }

+

+    [Pure]

+    public static bool operator ==(BigFloat x, BigFloat y) {

+      return x.CompareTo(y) == 0;

+    }

+

+    [Pure]

+    public static bool operator !=(BigFloat x, BigFloat y) {

+      return x.CompareTo(y) != 0;

+    }

+

+    [Pure]

+    public static bool operator <(BigFloat x, BigFloat y) {

+      return x.CompareTo(y) < 0;

+    }

+

+    [Pure]

+    public static bool operator >(BigFloat x, BigFloat y) {

+      return x.CompareTo(y) > 0;

+    }

+

+    [Pure]

+    public static bool operator <=(BigFloat x, BigFloat y) {

+      return x.CompareTo(y) <= 0;

+    }

+

+    [Pure]

+    public static bool operator >=(BigFloat x, BigFloat y) {

+      return x.CompareTo(y) >= 0;

+    }

+  }

+}

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 181076a7..cf6fb922 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1702,10 +1702,10 @@ namespace Microsoft.Boogie {
             return Type.Real;

           }

           if (arg0type.IsFloat && arg0type.Unify(arg1type)) {

-            return new FloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);

+            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);

           }

           if (arg1type.IsFloat && arg1type.Unify(arg0type)) {

-            return new FloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);

+            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);

           }

           goto BAD_TYPE;

         case Opcode.Div:

@@ -1719,6 +1719,12 @@ namespace Microsoft.Boogie {
               (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) {

             return Type.Real;

           }

+          if (arg0type.IsFloat && arg0type.Unify(arg1type)) {

+            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);

+          }

+          if (arg1type.IsFloat && arg1type.Unify(arg0type)) {

+            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);

+          }

           goto BAD_TYPE;

         case Opcode.Pow:

           if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {

@@ -1751,10 +1757,9 @@ namespace Microsoft.Boogie {
           if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {

             return Type.Bool;

           }

-          //if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))

-          //{

-            //return Type.Bool;

-          //}

+          if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) {

+            return Type.Bool;

+          }

           goto BAD_TYPE;

         case Opcode.And:

         case Opcode.Or:

@@ -1799,9 +1804,6 @@ namespace Microsoft.Boogie {
         case Opcode.Pow:

           return Type.Real;

 

-        //case Opcode.FloatDiv:

-          //return Type.Float;

-

         case Opcode.Eq:

         case Opcode.Neq:

         case Opcode.Gt:

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 3633a9c0..f030870e 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -689,12 +689,6 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

-      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

-      { //TODO: match z3

-        WriteApplication("/f", node, options);

-        return true;

-      }

-

       public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {

         WriteApplication("real_pow", node, options);

         return true;

@@ -746,12 +740,6 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

-      public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)

-      {

-        WriteApplication("to_float", node, options);

-        return true;

-      }

-

       private string ExtractDatatype(Function func) {

         if (func is DatatypeSelector) {

           DatatypeSelector selector = (DatatypeSelector) func;

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 8b79b0e5..00e6fb9c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -302,12 +302,6 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("/", node, wr);

     }

-    public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)

-    {

-      //Contract.Requires(wr != null);

-      //Contract.Requires(node != null);

-      return PrintNAry("/f", node, wr);

-    }

     public bool VisitPowOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

@@ -353,12 +347,6 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("real", node, wr);

     }

-    public bool VisitToFloatOp(VCExprNAry node, TextWriter wr)

-    {

-      //Contract.Requires(wr != null);

-      //Contract.Requires(node != null);

-      return PrintNAry("float", node, wr);

-    }

     public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

diff --git a/float_test5.bpl b/float_test5.bpl
index c3d279f2..be72b988 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,5 +1,4 @@
- procedure F() returns () {
+procedure F() returns () {
 	var x : float;
-	var y : float;
-	assert x + y == fp(0);
+	assert x - x == fp(0);
 }
\ No newline at end of file
diff --git a/float_test6.bpl b/float_test6.bpl
index 307da9f7..423bc45a 100644
--- a/float_test6.bpl
+++ b/float_test6.bpl
@@ -1,5 +1,5 @@
 procedure F() returns () {
 	var x : float;
-	x := fp(1) + fp(1);
-	assert x == fp(2);
+	var y : float;
+	assert (x + x) + (y + y) == fp(0);
 }
\ No newline at end of file