adding references to the floating point type wherever references to the real type exist. This remains a work in progress

8 files changed, 69 insertions, 37 deletions

diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index fea8eebc..84a6ffd1 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -163,7 +163,7 @@
     </Compile>

     <Compile Include="BigDec.cs" />

     <Compile Include="BigNum.cs" />

-    <Compile Include="fp32.cs" />

+    <Compile Include="FP32.cs" />

     <Compile Include="Rational.cs" />

     <Compile Include="Set.cs" />

   </ItemGroup>

diff --git a/Source/Basetypes/fp32.cs b/Source/Basetypes/fp32.cs
index c64afa54..5d76737b 100644
--- a/Source/Basetypes/fp32.cs
+++ b/Source/Basetypes/fp32.cs
@@ -11,7 +11,7 @@ using System.Text;
 using System.Diagnostics.Contracts;
 using System.Diagnostics;
 
-namespace Basetypes
+namespace Microsoft.Basetypes
 {
   using BIM = System.Numerics.BigInteger;
     
@@ -19,7 +19,7 @@ namespace Basetypes
   /// A representation of a 32-bit floating point value
   /// Note that this value has a 1-bit sign, 8-bit exponent, and 23-bit mantissa
   /// </summary>
-  public struct fp32
+  public struct FP32
   {
     //Please note that this code outline is copy-pasted from BigDec.cs
 
@@ -43,7 +43,7 @@ namespace Basetypes
       }
     }
 
-    public static readonly fp32 ZERO = FromInt(0);
+    public static readonly FP32 ZERO = FromInt(0);
     private static readonly BIM two = new BIM(2);
     private static readonly BIM ten = new BIM(10);
 
@@ -55,17 +55,17 @@ namespace Basetypes
     //For a complete summary of where this class has been added, simply view constructor references
 
     [Pure]
-    public static fp32 FromInt(int v) {
-      return new fp32(v, 0, v < 0); //TODO: modify for correct fp representation
+    public static FP32 FromInt(int v) {
+      return new FP32(v, 0, v < 0); //TODO: modify for correct fp representation
     }
 
     [Pure]
-    public static fp32 FromBigInt(BIM v) {
-      return new fp32(v, 0, v < 0); //TODO: modify for correct fp representation
+    public static FP32 FromBigInt(BIM v) {
+      return new FP32(v, 0, v < 0); //TODO: modify for correct fp representation
     }
 
     [Pure]
-    public static fp32 FromString(string v) {
+    public static FP32 FromString(string v) {
       //TODO: completely copied from BigDec.cs at the moment
       if (v == null) throw new FormatException();
 
@@ -100,10 +100,10 @@ namespace Basetypes
           fractionLen = fractionLen - 1;
         }
       }
-      return new fp32(integral - fraction, exponent, integral.Sign == -1);
+      return new FP32(integral - fraction, exponent, integral.Sign == -1);
     }
 
-    internal fp32(BIM mantissa, int exponent, bool isNegative) {
+    internal FP32(BIM mantissa, int exponent, bool isNegative) {
       this.isNegative = isNegative;
       if (mantissa.IsZero) {
         this.mantissa = mantissa;
@@ -128,10 +128,10 @@ namespace Basetypes
     public override bool Equals(object obj) {
       if (obj == null)
         return false;
-      if (!(obj is fp32))
+      if (!(obj is FP32))
         return false;
 
-      return (this == (fp32)obj);
+      return (this == (FP32)obj);
     }
 
     [Pure]
@@ -152,7 +152,7 @@ namespace Basetypes
 
     // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
     /// <summary>
-    /// Computes the floor and ceiling of this fp32. Note the choice of rounding towards negative
+    /// Computes the floor and ceiling of this FP32. 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>
@@ -277,28 +277,28 @@ namespace Basetypes
     // Basic arithmetic operations
 
     [Pure]
-    public fp32 Abs {
+    public FP32 Abs {
       //TODO: fix for fp functionality
       get {
-        return new fp32(BIM.Abs(this.mantissa), this.exponent, false);
+        return new FP32(BIM.Abs(this.mantissa), this.exponent, false);
       }
     }
 
     [Pure]
-    public fp32 Negate {
+    public FP32 Negate {
       //TODO: Modify for correct fp functionality
       get {
-        return new fp32(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0);
+        return new FP32(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0);
       }
     }
 
     [Pure]
-    public static fp32 operator -(fp32 x) {
+    public static FP32 operator -(FP32 x) {
       return x.Negate;
     }
 
     [Pure]
-    public static fp32 operator +(fp32 x, fp32 y) {
+    public static FP32 operator +(FP32 x, FP32 y) {
       //TODO: Modify for correct fp functionality
       BIM m1 = x.mantissa;
       int e1 = x.exponent;
@@ -316,18 +316,18 @@ namespace Basetypes
         e2 = e2 - 1;
       }
 
-      return new fp32(m1 + m2, e1, true);
+      return new FP32(m1 + m2, e1, true);
     }
 
     [Pure]
-    public static fp32 operator -(fp32 x, fp32 y) {
+    public static FP32 operator -(FP32 x, FP32 y) {
       return x + y.Negate;
     }
 
     [Pure]
-    public static fp32 operator *(fp32 x, fp32 y) {
+    public static FP32 operator *(FP32 x, FP32 y) {
       //TODO: modify for correct fp functionality
-      return new fp32(x.mantissa * y.mantissa, x.exponent + y.exponent, false);
+      return new FP32(x.mantissa * y.mantissa, x.exponent + y.exponent, false);
     }
 
 
@@ -353,44 +353,44 @@ namespace Basetypes
     }
 
     [Pure]
-    public int CompareTo(fp32 that) {
+    public int CompareTo(FP32 that) {
       //TODO: Modify for correct fp functionality
       if (this.mantissa == that.mantissa && this.exponent == that.exponent) {
         return 0;
       }
       else {
-        fp32 d = this - that;
+        FP32 d = this - that;
         return d.IsNegative ? -1 : 1;
       }
     }
 
     [Pure]
-    public static bool operator ==(fp32 x, fp32 y) {
+    public static bool operator ==(FP32 x, FP32 y) {
       return x.CompareTo(y) == 0;
     }
 
     [Pure]
-    public static bool operator !=(fp32 x, fp32 y) {
+    public static bool operator !=(FP32 x, FP32 y) {
       return x.CompareTo(y) != 0;
     }
 
     [Pure]
-    public static bool operator <(fp32 x, fp32 y) {
+    public static bool operator <(FP32 x, FP32 y) {
       return x.CompareTo(y) < 0;
     }
 
     [Pure]
-    public static bool operator >(fp32 x, fp32 y) {
+    public static bool operator >(FP32 x, FP32 y) {
       return x.CompareTo(y) > 0;
     }
 
     [Pure]
-    public static bool operator <=(fp32 x, fp32 y) {
+    public static bool operator <=(FP32 x, FP32 y) {
       return x.CompareTo(y) <= 0;
     }
 
     [Pure]
-    public static bool operator >=(fp32 x, fp32 y) {
+    public static bool operator >=(FP32 x, FP32 y) {
       return x.CompareTo(y) >= 0;
     }
   }
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f3a943b8..00306a5e 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -552,6 +552,21 @@ namespace Microsoft.Boogie {
         CachedHashCode = ComputeHashCode();

     }

 

+    /// <summary>

+    /// Creates a literal expression for the floating point value "v".

+    /// </summary>

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

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

+    public LiteralExpr(IToken/*!*/ tok, FP32 v, bool immutable = false)

+      : base(tok, immutable)

+    {

+      Contract.Requires(tok != null);

+      Val = v;

+      Type = Type.Float;

+      if (immutable)

+        CachedHashCode = ComputeHashCode();

+    }

+

     [Pure]

     [Reads(ReadsAttribute.Reads.Nothing)]

     public override bool Equals(object obj) {

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 97309155..ec8cd9e2 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -336,6 +336,7 @@ namespace Microsoft.Boogie {
 

     public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int);

     public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real);

+    public static readonly Type/*!*/ Float = new BasicType(SimpleType.Float);

     public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool);

     private static BvType[] bvtypeCache;

 

@@ -871,6 +872,8 @@ namespace Microsoft.Boogie {
           return "int";

         case SimpleType.Real:

           return "real";

+        case SimpleType.Float:

+          return "float";

         case SimpleType.Bool:

           return "bool";

       }

@@ -993,6 +996,13 @@ namespace Microsoft.Boogie {
         return this.T == SimpleType.Real;

       }

     }

+    public override bool IsFloat

+    {

+      get

+      {

+        return this.T == SimpleType.Float;

+      }

+    }

     public override bool IsBool {

       get {

         return this.T == SimpleType.Bool;

@@ -3526,6 +3536,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
   public enum SimpleType {

     Int,

     Real,

+    Float,

     Bool

   };

 

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 27f4eea7..fbb23cfe 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -34,7 +34,7 @@
     <IsWebBootstrapper>false</IsWebBootstrapper>

     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>

+    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -186,7 +186,7 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

-      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

+      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

     <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 9a0bab51..1d4b38b8 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -664,8 +664,11 @@ private class BvBounds : Expr {
 			ty = new BasicType(t, SimpleType.Int); 

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

 			Get();

-			ty = new BasicType(t, SimpleType.Real); 

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

+   ty = new BasicType(t, SimpleType.Real);

+  } else if (la.kind == 112837) {

+   Get();

+   ty = new BasicType(t, SimpleType.Float);

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

 			Get();

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

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

diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj
index 9b319d85..ddf310be 100644
--- a/Source/UnitTests/CoreTests/CoreTests.csproj
+++ b/Source/UnitTests/CoreTests/CoreTests.csproj
@@ -54,7 +54,7 @@
   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">

-      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

+      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

     <ProjectReference Include="..\..\Core\Core.csproj">

diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index b83983b6..7f266074 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -29,6 +29,9 @@ namespace CoreTests
 
             var literal4 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 8, /*immutable=*/true);
             Assert.AreEqual(literal4.ComputeHashCode(), literal4.GetHashCode());
+
+            var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.FP32.FromInt(0), /*immutable=*/true);
+            Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode());
         }
 
         [Test()]