Modified BigFloat and parser to accept correct SMT-LIB syntax

4 files changed, 192 insertions, 171 deletions

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 5b169263..8cde2cb9 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Basetypes
     

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

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

   /// </summary>

   public struct BigFloat

   {

@@ -25,33 +25,33 @@ namespace Microsoft.Basetypes
 

     // the internal representation

     [Rep]

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

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

     [Rep]

-    internal readonly int mantissaSize;

+    internal readonly int significandSize;

     [Rep]

-    internal readonly int exponent; //The value of the exponent is always positive as per fp representation requirements

+    internal readonly BigNum 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 String dec_value;

+    internal readonly String value; //Only used with second syntax

     [Rep]

-    internal readonly bool isDec;

+    internal readonly bool isNeg;

 

-    public long Mantissa {

+    public BigNum Significand {

       get {

-        return mantissa;

+        return significand;

       }

     }

 

-    public int Exponent {

+    public BigNum Exponent {

       get {

         return exponent;

       }

     }

 

-    public int MantissaSize {

+    public int SignificandSize {

       get {

-        return mantissaSize;

+        return significandSize;

       }

     }

 

@@ -61,25 +61,26 @@ namespace Microsoft.Basetypes
       }

     }

 

-    public String Decimal {

+    public bool IsNegative {

       get {

-        return dec_value;

+        return this.isNeg;

       }

     }

 

-    public bool IsDec {

+    public String Value {

       get {

-        return isDec;

+        return value;

       }

     }

 

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

+    public static BigFloat ZERO(int exponentSize, int significandSize) { return new BigFloat(false, BigNum.ZERO, BigNum.ZERO, exponentSize, significandSize); } //Does not include negative zero

 

-    private static readonly BIM two = new BIM(2);

-    private static long two_n(int n) {

-      long toReturn = 1;

+    private static readonly BigNum two = new BigNum(2);

+    private static readonly BigNum one = new BigNum(1);

+    private static BigNum two_n(int n) {

+      BigNum toReturn = one;

       for (int i = 0; i < n; i++)

-        toReturn = toReturn * 2;

+        toReturn = toReturn * two;

       return toReturn;

     }

 

@@ -95,18 +96,18 @@ namespace Microsoft.Basetypes
       return new BigFloat(v.ToString(), 8, 24);

     }

 

-    public static BigFloat FromInt(int v, int exponentSize, int mantissaSize)

+    public static BigFloat FromInt(int v, int exponentSize, int significandSize)

     {

-      return new BigFloat(v.ToString(), exponentSize, mantissaSize);

+      return new BigFloat(v.ToString(), exponentSize, significandSize);

     }

 

     public static BigFloat FromBigInt(BIM v) {

       return new BigFloat(v.ToString(), 8, 24);

     }

 

-    public static BigFloat FromBigInt(BIM v, int exponentSize, int mantissaSize)

+    public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize)

     {

-      return new BigFloat(v.ToString(), exponentSize, mantissaSize);

+      return new BigFloat(v.ToString(), exponentSize, significandSize);

     }

 

     public static BigFloat FromBigDec(BigDec v)

@@ -114,84 +115,67 @@ namespace Microsoft.Basetypes
       return new BigFloat(v.ToDecimalString(), 8, 24);

     }

 

-    public static BigFloat FromBigDec(BigDec v, int exponentSize, int mantissaSize)

+    public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize)

     {

-      return new BigFloat(v.ToDecimalString(), exponentSize, mantissaSize);

+      return new BigFloat(v.ToDecimalString(), exponentSize, significandSize);

     }

 

     [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(vals[0], 8, 24); 

-          case 2:

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

-          case 3:

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

-          case 4:

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

-          default:

-            throw new FormatException(); //Unreachable

-        }

-      }

-      catch (Exception) { //Catch parsing errors

-        throw new FormatException();

-      }

+    public static BigFloat FromString(String v, int exp, int sig) { //String must be

+      return new BigFloat(v, exp, sig);

     }

 

-    internal BigFloat(int exponent, long mantissa, int exponentSize, int mantissaSize) {

+    public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) {

       this.exponentSize = exponentSize;

       this.exponent = exponent;

-      this.mantissa = mantissa;

-      this.mantissaSize = mantissaSize;

-      this.isDec = false;

-      this.dec_value = "";

+      this.significand = significand;

+      this.significandSize = significandSize;

+      this.isNeg = sign;

+      this.value = "";

     }

 

-    internal BigFloat(String dec_value, int exponentSize, int mantissaSize) {

+    public BigFloat(String value, int exponentSize, int significandSize) {

       this.exponentSize = exponentSize;

-      this.mantissaSize = mantissaSize;

-      this.exponent = 0;

-      this.mantissa = 0;

-      this.isDec = true;

-      this.dec_value = dec_value;

+      this.significandSize = significandSize;

+      this.exponent = BigNum.ZERO;

+      this.significand = BigNum.ZERO;

+      this.value = value;

+      this.isNeg = value[0] == '-';

       //Special cases:

-      if (this.dec_value.Equals("+oo") || this.dec_value.Equals("-oo") || this.dec_value.Equals("-zero"))

+      if (this.value.Equals("+oo") || this.value.Equals("-oo") || this.value.Equals("-zero"))

         return;

-      if (this.dec_value.ToLower().Equals("nan")) {

-        this.dec_value = "NaN";

+      if (this.value.ToLower().Equals("nan")) {

+        this.value = "NaN";

         return;

       }

-      if (this.dec_value.Equals("INF") || this.dec_value.Equals("+INF")) {

-        this.dec_value = "+oo";

+      if (this.value.Equals("INF") || this.value.Equals("+INF"))

+      {

+        this.value = "+oo";

         return;

       }

-      if (this.dec_value.Equals("-INF")) {

-        this.dec_value = "-oo";

+      if (this.value.Equals("-INF"))

+      {

+        this.value = "-oo";

         return;

       }

-      if (this.dec_value.Equals("+zero")) {

-        this.dec_value = "0.0";

+      if (this.value.Equals("+zero"))

+      {

+        this.value = "0.0";

         return;

       }

       //End special cases

-      if (this.dec_value.IndexOf('.') == -1 && this.dec_value.IndexOf('e') == -1)

-        this.dec_value += ".0"; //Assures that the decimal value is a "real" number

-      if (this.dec_value.IndexOf('.') == 0)

-        this.dec_value = "0" + this.dec_value; //Assures that decimals always have a 0 in front

+      if (this.value.IndexOf('.') == -1 && this.value.IndexOf('e') == -1)

+        this.value += ".0"; //Assures that the decimal value is a "real" number

+      if (this.value.IndexOf('.') == 0)

+        this.value = "0" + this.value; //Assures that decimals always have a 0 in front

     }

 

-    private BIM maxMantissa()

+    private BigNum maxsignificand()

     {

-      BIM result = new BIM(1);

-      for (int i = 0; i < mantissaSize; i++)

+      BigNum result = one;

+      for (int i = 0; i < significandSize; i++)

         result = result * two;

-      return result - 1;

+      return result - one;

     }

     private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }

 

@@ -213,13 +197,13 @@ namespace Microsoft.Basetypes
 

     [Pure]

     public override int GetHashCode() {

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

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

     }

 

     [Pure]

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

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

-      return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());

+      return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;

     }

 

 

@@ -229,41 +213,41 @@ namespace Microsoft.Basetypes
     /// <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

+    /// the returned fp assumes the given significand and exponent size

     /// </summary>

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

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

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

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

     /// <returns></returns>

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

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

     {

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

+        return Round(BigNum.FromString(value), BigNum.ZERO, exponentSize, significandSize);

+      return Round(i == 0 ? BigNum.ZERO : BigNum.FromString(value.Substring(0, i)), BigNum.FromString(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);

     }

 

     /// <summary>

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

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

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

     /// Returns the result of this calculation

     /// </summary>

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

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

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

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

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

     /// <returns></returns>

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

+    public static BigFloat Round(BigNum value, BigNum dec_value, int exponentSize, int significandSize)

     {

       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

+      BigNum one = new BigNum(1);

+      BigNum ten = new BigNum(10);

+      BigNum dec_max = new BigNum(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);

+          dec_max = new BigNum(10);

           while (dec_max < dec_value)

             dec_max = dec_max * ten;

           dec_value = dec_value + dec_max;

@@ -275,7 +259,7 @@ namespace Microsoft.Basetypes
         exp++;

       }

       if (value.IsZero && !dec_value.IsZero) {

-        dec_max = new BIM(10);

+        dec_max = new BigNum(10);

         while (dec_max < dec_value)

           dec_max = dec_max * ten;

         while (value.IsZero) {//Multiply by two, decrement exponent by 1

@@ -288,12 +272,12 @@ namespace Microsoft.Basetypes
         }

       }

 

-      //Second, calculate the mantissa

-      value = new BIM(0); //remove implicit bit

-      dec_max = new BIM(10);

+      //Second, calculate the significand

+      value = new BigNum(0); //remove implicit bit

+      dec_max = new BigNum(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

+      for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated

         dec_value = dec_value * two;

         if (dec_value >= dec_max) {

           dec_value = dec_value - dec_max;

@@ -301,7 +285,7 @@ namespace Microsoft.Basetypes
         }

       }

 

-      return new BigFloat(exp, Int64.Parse(value.ToString()), exponentSize, mantissaSize);

+      return new BigFloat(false, BigNum.ZERO, BigNum.FromString(value.ToString()), exponentSize, significandSize); //Sign not actually checked...

     }

 

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

@@ -312,30 +296,32 @@ namespace Microsoft.Basetypes
     /// </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) {

+    public void FloorCeiling(out BigNum floor, out BigNum ceiling) {

       //TODO: fix for fp functionality

-      BIM n = Mantissa;

-      int e = Exponent;

+      BigNum n = Significand;

+      BigNum e = Exponent;

       if (n.IsZero) {

         floor = ceiling = n;

-      } else if (0 <= e) {

+      } else if (BigNum.ZERO <= e) {

         // it's an integer

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

+        for (; BigNum.ZERO < e; e = e - one)

+        {

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

+        for (; BigNum.ZERO < e && !n.IsZero; e = e + one)

+        {

           n = n / two;  // Division rounds towards negative infinity

         }

 

         if (!IsNegative) {

           floor = n;

-          ceiling = n + 1;

+          ceiling = n + one;

         } else {

           ceiling = n;

-          floor = n - 1;

+          floor = n - one;

         }

       }

       Debug.Assert(floor <= ceiling, "Invariant was not maintained");

@@ -352,7 +338,7 @@ namespace Microsoft.Basetypes
     [Pure]

     public string ToDecimalString() {

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

-      return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());

+      return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;

     }

 

     [Pure]

@@ -380,18 +366,16 @@ namespace Microsoft.Basetypes
     [Pure]

     public BigFloat Abs {

       get {

-        if (IsDec)

-          return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : this;

-        return new BigFloat(Exponent, Math.Abs(Mantissa), ExponentSize, MantissaSize);

+        return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);

       }

     }

 

     [Pure]

     public BigFloat Negate {

       get {

-        if (IsDec)

-          return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : new BigFloat("-" + dec_value, ExponentSize, MantissaSize);

-        return new BigFloat(Exponent, -Mantissa, ExponentSize, MantissaSize);

+        if (value != "")

+          return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);

+        return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);

       }

     }

 

@@ -404,26 +388,26 @@ namespace Microsoft.Basetypes
     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);

-      long m1 = x.Mantissa;

-      int e1 = x.Exponent;

-      long m2 = y.Mantissa;

-      int e2 = y.Exponent;

-      m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit

-      m2 = m2 + two_n(y.mantissaSize + 1);

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

+      BigNum m1 = x.significand;

+      BigNum e1 = x.Exponent;

+      BigNum m2 = y.significand;

+      BigNum e2 = y.Exponent;

+      m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit

+      m2 = m2 + two_n(y.significandSize + 1);

       if (e2 > e1) {

-        m1 = y.Mantissa;

+        m1 = y.significand;

         e1 = y.Exponent;

-        m2 = x.Mantissa;

+        m2 = x.significand;

         e2 = x.Exponent;

       }

 

       while (e2 < e1) {

-        m2 = m2 / 2;

-        e2++;

+        m2 = m2 / two;

+        e2 = e2 + one;

       }

 

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

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

     }

 

     [Pure]

@@ -434,8 +418,8 @@ namespace Microsoft.Basetypes
     [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);

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

+      return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);

     }

 

 

@@ -444,9 +428,9 @@ namespace Microsoft.Basetypes
 

     public bool IsSpecialType {

       get {

-        if (!IsDec)

+        if (value == "")

           return false;

-        return (dec_value.Equals("NaN") || dec_value.Equals("+oo") || dec_value.Equals("-oo") || dec_value.Equals("-zero"));

+        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("-zero"));

       }

     }

 

@@ -456,15 +440,9 @@ namespace Microsoft.Basetypes
       }

     }

 

-    public bool IsNegative {

-      get {

-        return (isDec && dec_value[0] == '-') || mantissa < 0;

-      }

-    }

-

     public bool IsZero {

       get {

-        return Mantissa == 0 && Exponent == 0;

+        return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO;

       }

     }

 

@@ -474,9 +452,9 @@ namespace Microsoft.Basetypes
         return 1;

       if (this.exponent < that.exponent)

         return -1;

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

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

         return 0;

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

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

     }

 

     [Pure]

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 5fcb1cdc..bf35ccbe 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -668,17 +668,35 @@ private class BvBounds : Expr {
    ty = new BasicType(t, SimpleType.Real);

   } else if (la.kind == 98) {

    Get();

-   if (la.kind == 9) {

-     Get();

-     Expect(3);

-     int exp = Int32.Parse(t.val);

-     Expect(3);

-     int man = Int32.Parse(t.val);

-     ty = new FloatType(t, exp, man);

-     Expect(10);

+   if (la.kind == 3) {

+    Expect(3);

+    switch (Int32.Parse(t.val)) {

+    case 16:

+        ty = new FloatType(t, 5, 11);

+        break;

+    case 32:

+        ty = new FloatType(t, 8, 24);

+        break;

+    case 64:

+        ty = new FloatType(t, 11, 53);

+        break;

+    case 128:

+        ty = new FloatType(t, 15, 113);

+        break;

+    default:

+        SynErr(3);

+        break;

+    }

+   }

+   else {

+    Expect(19);

+    Expect(3);

+    int exp = Int32.Parse(t.val);

+    Expect(3);

+    int man = Int32.Parse(t.val);

+    ty = new FloatType(t, exp, man);

+    Expect(20);

    }

-   else

-    ty = new FloatType(t, 8, 24);

   } else if (la.kind == 16) {

 			Get();

 			ty = new BasicType(t, SimpleType.Bool); 

@@ -1813,9 +1831,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
   case 98: {

       Get();

       x = t;

-      Expect(9);

+      Expect(19);

       Expression(out e);

-      Expect(10);

+      Expect(20);

       e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });

       break;

     }

@@ -1887,29 +1905,45 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
   /// <param name="n"></param>

  void Float(out BigFloat n)

  {

-   //To be modified

-   string s = "";

    try

    {

-     if (la.kind == 97)

-     {

-       //Expected format = fp (a b) || fp (a b c d)

+     if (la.kind == 97) {

+       bool negative = false;

+       int exp, sig;

+       BigNum exp_val, sig_val, value;

+       //Expected format = fp(sign exp_val sig_val) || fp<exp sig>(value)

        Get(); //Skip the fp token

        Get();

-       if (t.val != "(") { throw new FormatException(); }

-       while (la.kind == 1 || la.kind == 3 || la.kind == 6 || la.kind == 4 || la.kind == 74 || la.kind == 75) { //Get values between the parens

+       if (t.val == "(") {

          Get();

-         if (t.val == "-" || t.val == "+") //special sign case (la.kind == 74 or 75)

-          s += t.val;

-         else

-          s += t.val + " ";

+         negative = Boolean.Parse(t.val);

+         BvLit(out exp_val, out exp);

+         BvLit(out sig_val, out sig);

+         n = new BigFloat(negative, exp_val, sig_val, exp, sig);

+       }

+       else if (t.val == "<") {

+         Expect(14);

+         exp = Int32.Parse(t.val);

+         Expect(14);

+         sig = Int32.Parse(t.val);

+         int size;

+         BvLit(out value, out size);

+         if (size != exp + sig)

+         {

+           this.SemErr("The given bitvector size of " + size + "does not match the provided floating-point size of " + (exp + sig));

+           n = BigFloat.ZERO(8, 24);

+           return;

+         }

+         n = new BigFloat(t.val, exp, sig);

+       }

+       else {

+         throw new FormatException();

        }

-       Get();

-       if (t.val != ")") { throw new FormatException(); }

      }

-     else SynErr(137);

-

-     n = BigFloat.FromString(s.Trim());

+     else {

+       n = BigFloat.ZERO(8, 24);

+       SynErr(137);

+     }

    }

    catch (FormatException)

    {

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7c3ae960..59b6b7e7 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -205,10 +205,10 @@ namespace Microsoft.Boogie.SMTLib
       {

         BigFloat lit = ((VCExprFloatLit)node).Val;

         if (lit.IsSpecialType) {

-          wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ")");

+          wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ")");

           return true;

         }

-        wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ") RNE ");

+        wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ") RNE ");

         if (lit.IsNegative)

           // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")

           wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());

diff --git a/fp_documentation.txt b/fp_documentation.txt
index 09e60b9a..d3fafdcb 100644
--- a/fp_documentation.txt
+++ b/fp_documentation.txt
@@ -10,7 +10,9 @@ Declaring Variables:
 The syntax for declaring a floating point variable is as follows:

 var name: float(exp man);

 Where exp is the size of the float exponent and man is the size of the float mantissa

+Please note that 

 

+**REMOVE THIS SYNTAX**

 It is also acceptable to use the following syntax:

 var name: float();

 This syntax assumes the float exponent to be size 8 and the mantissa to be size 24

@@ -23,10 +25,11 @@ Declares a variable called x with a exponent sized 11 and mantissa sized 53
 Declaring Constants:

 

 All of the following syntax are viable for declaring a floating point constant:

-float(dec)

-float(exp_val man_val)

-float(dec exp man)

-float(exp_val man_val exp man)

+**REMOVE THE FIRST OF THESE TWO SYNTAXES**

+fp(dec)

+fp(exp_val man_val)

+fp(dec exp man)

+fp(exp_val man_val exp man)

 

 Where dec is the decimal value of the constant,

 exp_val/man_value are the integer values of their respective fields,

@@ -68,6 +71,8 @@ Where exp and man are the sizes of the exponent and mantissa respectively
 --------------------------------------------------------------------------------

 Known Issues:

 

+float16, float32, float64, and float128 still need to be added

+

 There is currently no way to convert from a floating point to any other data type

 

 There is currently no way to convert the value of a variable to a floating point type

@@ -76,4 +81,8 @@ var x : real;
 fp(x);

 

 Statements of the following form cause a parser error (parenthesis followed by fp constant)

-... (fp(1) + fp(1));
\ No newline at end of file
+... (fp(1) + fp(1));

+

+Attempts by Boogie to infer the behavior of loops fail when floating points are involved

+

+Describing loop behavior manually is untested (using loop unroll appears to work)
\ No newline at end of file