Float type now works correctly for simple variable declaration and comparison.

12 files changed, 49 insertions, 46 deletions

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index a4cd6574..1fb05005 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -90,12 +90,12 @@ namespace Microsoft.Basetypes
 
     [Pure]
     public static BigFloat FromBigInt(BIM v) {
-      return new BigFloat(v, 0, 23, 8); //TODO: modify for correct fp representation
+      return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation
     }
 
     public static BigFloat FromBigDec(BIM v)
     {
-      return new BigFloat(v, 0, 23, 8); //TODO: modify for correct fp representation
+      return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation
     }
 
     [Pure]
@@ -107,13 +107,13 @@ namespace Microsoft.Basetypes
       {
         switch (vals.Length) {
           case 1:
-            return Round(vals[0], 23, 8); 
+            return Round(vals[0], 8, 23); 
           case 2:
-            return new BigFloat(BIM.Parse(vals[0]), Int32.Parse(vals[1]), 23, 8);
+            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 23);
           case 3:
             return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
           case 4:
-            return new BigFloat(BIM.Parse(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
+            return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
           default:
             throw new FormatException(); //Unreachable
         }
@@ -123,11 +123,11 @@ namespace Microsoft.Basetypes
       }
     }
 
-    internal BigFloat(BIM mantissa, int exponent, int mantissaSize, int exponentSize) {
-      this.mantissa = mantissa;
-      this.mantissaSize = mantissaSize;
+    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;
@@ -197,12 +197,12 @@ namespace Microsoft.Basetypes
     /// <param name="mantissaSize"></param>
     /// <param name="exponentSize"></param>
     /// <returns></returns>
-    public static BigFloat Round(String value, int mantissaSize, int exponentSize)
+    public static BigFloat Round(String value, int exponentSize, int mantissaSize)
     {
       int i = value.IndexOf('.');
       if (i == -1)
-        return Round(BIM.Parse(value), 0, 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);
+        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>
@@ -214,7 +214,7 @@ namespace Microsoft.Basetypes
     /// <param name="mantissaSize"></param>
     /// <param name="exponentSize"></param>
     /// <returns></returns>
-    public static BigFloat Round(BIM value, BIM dec_value, int mantissaSize, int exponentSize)
+    public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)
     {
       int exp = 0;
       BIM one = new BIM(1);
@@ -262,7 +262,7 @@ namespace Microsoft.Basetypes
         }
       }
 
-      return new BigFloat(value, exp, mantissaSize, exponentSize);
+      return new BigFloat(exp, value, exponentSize, mantissaSize);
     }
 
     // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
@@ -395,7 +395,7 @@ namespace Microsoft.Basetypes
     public BigFloat Abs {
       //TODO: fix for fp functionality
       get {
-        return new BigFloat(BIM.Abs(Mantissa), Exponent, MantissaSize, ExponentSize);
+        return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);
       }
     }
 
@@ -403,7 +403,7 @@ namespace Microsoft.Basetypes
     public BigFloat Negate {
       //TODO: Modify for correct fp functionality
       get {
-        return new BigFloat(BIM.Negate(Mantissa), Exponent, MantissaSize, ExponentSize);
+        return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);
       }
     }
 
@@ -415,6 +415,8 @@ namespace Microsoft.Basetypes
     [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;
@@ -433,7 +435,7 @@ namespace Microsoft.Basetypes
         e2++;
       }
 
-      return new BigFloat(m1 + m2, e1, Math.Max(x.MantissaSize, y.MantissaSize), Math.Max(x.ExponentSize, y.ExponentSize));
+      return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);
     }
 
     [Pure]
@@ -443,7 +445,9 @@ namespace Microsoft.Basetypes
 
     [Pure]
     public static BigFloat operator *(BigFloat x, BigFloat y) {
-      return new BigFloat(x.Mantissa * y.Mantissa, x.Exponent + y.Exponent, Math.Max(x.MantissaSize, y.MantissaSize), Math.Max(x.ExponentSize, y.ExponentSize));
+      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);
     }
 
 
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 50fde975..5d41a8dd 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -330,20 +330,22 @@ namespace Microsoft.Boogie {
         return false;

       }

     }

-    public virtual int FloatMantissa {

-      get {

+    public virtual int FloatExponent

+    {

+      get

+      {

         {

           Contract.Assert(false);

           throw new cce.UnreachableException();

-        } // Type.FloatMantissa should never be called

+        } // Type.FloatExponent should never be called

       }

     }

-    public virtual int FloatExponent {

+    public virtual int FloatMantissa {

       get {

         {

           Contract.Assert(false);

           throw new cce.UnreachableException();

-        } // Type.FloatExponent should never be called

+        } // Type.FloatMantissa should never be called

       }

     }

     public virtual bool IsBv {

@@ -1050,14 +1052,14 @@ namespace Microsoft.Boogie {
     public FloatType(IToken token, int exponent, int mantissa)

       : base(token) {

       Contract.Requires(token != null);

-      Mantissa = mantissa;

       Exponent = exponent;

+      Mantissa = mantissa;

     }

 

     public FloatType(int exponent, int mantissa)

       : base(Token.NoToken) {

-      Mantissa = mantissa;

       Exponent = exponent;

+      Mantissa = mantissa;

     }

 

     //-----------  Cloning  ----------------------------------

@@ -1092,7 +1094,7 @@ namespace Microsoft.Boogie {
     public override string ToString()

     {

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

-      return "(_ FP " + Exponent + " " + Mantissa + ")";

+      return "float (" + Exponent + " " + Mantissa + ")";

     }

 

     //-----------  Equality  ----------------------------------

@@ -1119,10 +1121,10 @@ namespace Microsoft.Boogie {
       //Contract.Requires(cce.NonNullElements(unifier));

       that = that.Expanded;

       if (that is TypeProxy || that is TypeVariable) {

-        return that.Unify(this, unifiableVariables, unifier);

+        return that.Unify(this, unifiableVariables, unifier); 

       }

       else {

-        return this.Equals(that);

+        return this.Equals(that); 

       }

     }

 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index bb372cfb..2550c334 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -366,7 +366,7 @@ private class BvBounds : Expr {
 			Get();

 			Type(out retTy);

 			retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); 

-		} else SynErr(97);

+		} else SynErr(99);

 		if (la.kind == 27) {

 			Get();

 			Expression(out tmp);

@@ -374,7 +374,7 @@ private class BvBounds : Expr {
 			Expect(28);

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

 			Get();

-		} else SynErr(98);

+		} else SynErr(100);

 		if (retTyd == null) {

 		 // construct a dummy type for the case of syntax error

 		 retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index c7ae9d57..3633a9c0 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsReal)

         return "Real";

       else if (t.IsFloat)

-        return t.ToString(); //TODO: Match z3 syntax

+        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax

       else if (t.IsBv) {

         return "(_ BitVec " + t.BvBits + ")";

       } else {

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 2b09362b..4a1331c5 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,7 +93,6 @@ namespace Microsoft.Boogie.SMTLib
         log = log.Replace("\r", "").Replace("\n", " ");

         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);

       }

-      Console.WriteLine(cmd); //TODO: Remove This Line

       toProver.WriteLine(cmd);

     }

 

diff --git a/float_test2.bpl b/float_test2.bpl
index fa34d8cf..956ac757 100644
--- a/float_test2.bpl
+++ b/float_test2.bpl
@@ -1,5 +1,5 @@
 procedure F() returns () {
-	var x : float;
-	var y : float;
+	var x : float(11 53);
+	var y : float(11 53);
 	assert x == y;
 }
\ No newline at end of file
diff --git a/float_test3.bpl b/float_test3.bpl
index 1b70ebf4..e93e7df7 100644
--- a/float_test3.bpl
+++ b/float_test3.bpl
@@ -1,6 +1,3 @@
  procedure F() returns () {
-	var x : float;
-	var y : float;
-	y := x - x;
-	assert y == x;
+	assert fp(5) == fp(5 8 23);
 }
\ No newline at end of file
diff --git a/float_test4.bpl b/float_test4.bpl
index 2388a281..1252dc71 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,5 +1,5 @@
  procedure F() returns () {
 	var x : float;
-	x := fp (0 0);
-	assert x == fp (0 0 23 8);
+	x := fp (.5 8 23);
+	assert x == fp (-1 0);
 }
\ No newline at end of file
diff --git a/float_test5.bpl b/float_test5.bpl
index b91e53e9..2f565b27 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,5 +1,5 @@
  procedure F() returns () {
 	var x : float;
 	x := fp (0 0);
-	assert x == fp (1 0 23 8);
+	assert x == fp (0 0 8 30);
 }
\ No newline at end of file
diff --git a/float_test6.bpl b/float_test6.bpl
index 12cfbabe..307da9f7 100644
--- a/float_test6.bpl
+++ b/float_test6.bpl
@@ -1,5 +1,5 @@
- procedure F() returns () {
+procedure F() returns () {
 	var x : float;
-	x := fp (3);
-	assert x == fp (8388608 1 23 8);
+	x := fp(1) + fp(1);
+	assert x == fp(2);
 }
\ No newline at end of file
diff --git a/float_test7.bpl b/float_test7.bpl
index ca33eb08..cc7a040b 100644
--- a/float_test7.bpl
+++ b/float_test7.bpl
@@ -1,5 +1,5 @@
- procedure F() returns () {
+procedure F() returns () {
 	var x : float;
-	x := fp (.5 23 8);
-	assert x == fp (0 -1);
+	x := fp(.1) + fp(.1) + fp(.1);
+	assert x == fp(.3);
 }
\ No newline at end of file
diff --git a/float_test8.bpl b/float_test8.bpl
index 8d881126..7c23c74f 100644
--- a/float_test8.bpl
+++ b/float_test8.bpl
@@ -1,4 +1,5 @@
 procedure F() returns () {
+	Logic=QF_FP;
 	var x : float;
 	x := fp(.1) + fp(.1);
 	assert x == fp(.2);