Special fp types (such as infinity and NaN are now translated by boogie

4 files changed, 64 insertions, 28 deletions

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index bbc39db4..6cf94feb 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Basetypes
 

     // the internal representation

     [Rep]

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

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

     [Rep]

     internal readonly int mantissaSize;

     [Rep]

@@ -37,7 +37,7 @@ namespace Microsoft.Basetypes
     [Rep]

     internal readonly bool isDec;

 

-    public BIM Mantissa {

+    public long Mantissa {

       get {

         return mantissa;

       }

@@ -69,17 +69,17 @@ namespace Microsoft.Basetypes
 

     public bool IsDec {

       get {

-        return IsDec;

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

+    private static long two_n(int n) {

+      long toReturn = 1;

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

-        toReturn = toReturn * two;

+        toReturn = toReturn * 2;

       return toReturn;

     }

 

@@ -96,10 +96,14 @@ namespace Microsoft.Basetypes
     }

 

     [Pure]

-    public static BigFloat FromBigInt(BIM v) {

+    public static BigFloat FromLong(long v) {

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

     }

 

+    public static BigFloat FromBigInt(BIM v) {

+      return FromLong(Int64.Parse(v.ToString())); //Sketchy.  Hope this doesn't cause problems

+    }

+

     public static BigFloat FromBigDec(BigDec v)

     {

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

@@ -116,11 +120,11 @@ namespace Microsoft.Basetypes
           case 1:

             return new BigFloat(vals[0], 8, 24); 

           case 2:

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

+            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]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));

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

           default:

             throw new FormatException(); //Unreachable

         }

@@ -130,7 +134,7 @@ namespace Microsoft.Basetypes
       }

     }

 

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

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

       this.exponentSize = exponentSize;

       this.exponent = exponent;

       this.mantissa = mantissa;

@@ -146,8 +150,30 @@ namespace Microsoft.Basetypes
       this.mantissa = 0;

       this.isDec = true;

       this.dec_value = dec_value;

+      //Special cases:

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

+        return;

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

+        this.dec_value = "NaN";

+        return;

+      }

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

+        this.dec_value = "+oo";

+        return;

+      }

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

+        this.dec_value = "-oo";

+        return;

+      }

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

+        this.dec_value = "0.0";

+        return;

+      }

+      //End special cases

       if (this.dec_value.IndexOf(".") == -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

     }

 

     private BIM maxMantissa()

@@ -265,7 +291,7 @@ namespace Microsoft.Basetypes
         }

       }

 

-      return new BigFloat(exp, value, exponentSize, mantissaSize);

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

     }

 

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

@@ -345,7 +371,7 @@ namespace Microsoft.Basetypes
     public BigFloat Abs {

       //TODO: fix for fp functionality

       get {

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

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

       }

     }

 

@@ -353,7 +379,7 @@ namespace Microsoft.Basetypes
     public BigFloat Negate {

       //TODO: Modify for correct fp functionality

       get {

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

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

       }

     }

 

@@ -367,9 +393,9 @@ namespace Microsoft.Basetypes
       //TODO: Modify for correct fp functionality

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

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

-      BIM m1 = x.Mantissa;

+      long m1 = x.Mantissa;

       int e1 = x.Exponent;

-      BIM m2 = y.Mantissa;

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

@@ -381,7 +407,7 @@ namespace Microsoft.Basetypes
       }

 

       while (e2 < e1) {

-        m2 = m2 / two;

+        m2 = m2 / 2;

         e2++;

       }

 

@@ -404,6 +430,14 @@ namespace Microsoft.Basetypes
     ////////////////////////////////////////////////////////////////////////////

     // Some basic comparison operations

 

+    public bool IsSpecialType {

+      get {

+        if (!IsDec)

+          return false;

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

+      }

+    }

+

     public bool IsPositive {

       get {

         return !IsNegative;

@@ -418,7 +452,7 @@ namespace Microsoft.Basetypes
 

     public bool IsZero {

       get {

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

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

       }

     }

 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 889d7be8..5fcb1cdc 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1897,9 +1897,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
        Get(); //Skip the fp token

        Get();

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

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

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

          Get();

-         if (t.val == "-") //special negative case (la.kind == 75)

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

           s += t.val;

          else

           s += t.val + " ";

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 629f7e2d..7c3ae960 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -204,7 +204,11 @@ namespace Microsoft.Boogie.SMTLib
       else if (node is VCExprFloatLit)

       {

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

-        wr.Write(("((_ to_fp 8 24) roundTowardZero "));

+        if (lit.IsSpecialType) {

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

+          return true;

+        }

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

         if (lit.IsNegative)

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

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

@@ -620,31 +624,31 @@ namespace Microsoft.Boogie.SMTLib
 

       public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("fp.add roundTowardZero", node, options);

+        WriteApplication("fp.add RNE", node, options);

         return true;

       }

 

       public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("fp.sub roundTowardZero", node, options);

+        WriteApplication("fp.sub RNE", node, options);

         return true;

       }

 

       public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("fp.mul roundTowardZero", node, options);

+        WriteApplication("fp.mul RNE", node, options);

         return true;

       }

 

       public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("fp.div roundTowardZero", node, options);

+        WriteApplication("fp.div RNE", node, options);

         return true;

       }

 

       public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("fp.rem roundTowardZero", node, options);

+        WriteApplication("fp.rem RNE", node, options);

         return true;

       }

 

diff --git a/float_test8.bpl b/float_test8.bpl
index 32fb8863..554dcf00 100644
--- a/float_test8.bpl
+++ b/float_test8.bpl
@@ -1,5 +1,3 @@
 procedure F() returns () {
-	var x : float;
-	x := fp(0.1) + fp(0.1);
-	assert x == fp(0.2);
+	assert fp(-oo)==fp(-oo);
 }
\ No newline at end of file