Modified internal abstract float representation to allow user-defined mantissa and exponent

9 files changed, 242 insertions, 58 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 9297bcbc..7e7ed10a 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -561,7 +561,7 @@ namespace Microsoft.Boogie {
     {

       Contract.Requires(tok != null);

       Val = v;

-      Type = Type.Float;

+      Type = Type.GetFloatType(v.ExponentSize, v.MantissaSize);

       if (immutable)

         CachedHashCode = ComputeHashCode();

     }

@@ -638,7 +638,8 @@ namespace Microsoft.Boogie {
         } else if (Val is BigDec) {

           return Type.Real;

         } else if (Val is BigFloat) {

-          return Type.Float;

+          BigFloat temp = (BigFloat)Val;

+          return Type.GetFloatType(temp.ExponentSize, temp.MantissaSize);

         } else if (Val is BvConst) {

           return Type.GetBvType(((BvConst)Val).Bits);

         } else {

@@ -1376,9 +1377,9 @@ namespace Microsoft.Boogie {
           if (arg0type.Unify(Type.Real)) {

             return Type.Real;

           }

-          if (arg0type.Unify(Type.Float)) {

-            return Type.Float;

-          }

+          //if (arg0type.Unify(Type.Float)) {

+            //return Type.Float;

+          //}

           goto BAD_TYPE;

         case Opcode.Not:

           if (arg0type.Unify(Type.Bool)) {

@@ -1519,7 +1520,7 @@ namespace Microsoft.Boogie {
           case Opcode.RealDiv:

             return "/";

           case Opcode.FloatDiv:

-            return "/f";

+            return "/";

           case Opcode.Pow:

             return "**";

           case Opcode.Eq:

@@ -1706,10 +1707,10 @@ namespace Microsoft.Boogie {
           if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {

             return Type.Real;

           }

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

-          {

-            return Type.Float;

-          }

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

+          //{

+            //return Type.Float;

+          //}

           goto BAD_TYPE;

         case Opcode.Div:

         case Opcode.Mod:

@@ -1723,13 +1724,6 @@ namespace Microsoft.Boogie {
             return Type.Real;

           }

           goto BAD_TYPE;

-        case Opcode.FloatDiv: //TODO: Modify

-          if ((arg0type.Unify(Type.Int) || arg0type.Unify(Type.Real) || arg0type.Unify(Type.Float)) &&

-              (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real) || arg0type.Unify(Type.Float)))

-          {

-            return Type.Float;

-          }

-          goto BAD_TYPE;

         case Opcode.Pow:

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

             return Type.Real;

@@ -1761,10 +1755,10 @@ 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.Unify(Type.Float) && arg1type.Unify(Type.Float))

+          //{

+            //return Type.Bool;

+          //}

           goto BAD_TYPE;

         case Opcode.And:

         case Opcode.Or:

@@ -1809,8 +1803,8 @@ namespace Microsoft.Boogie {
         case Opcode.Pow:

           return Type.Real;

 

-        case Opcode.FloatDiv:

-          return Type.Float;

+        //case Opcode.FloatDiv:

+          //return Type.Float;

 

         case Opcode.Eq:

         case Opcode.Neq:

@@ -2267,23 +2261,14 @@ namespace Microsoft.Boogie {
           this.name = "int";

           this.type = Type.Int;

           this.argType = Type.Real;

-          this.argType2 = Type.Float;

           this.hashCode = 1;

           break;

         case CoercionType.ToReal:

           this.name = "real";

           this.type = Type.Real;

           this.argType = Type.Int;

-          this.argType2 = Type.Float;

           this.hashCode = 2;

           break;

-        case CoercionType.ToFloat:

-          this.name = "float";

-          this.type = Type.Float;

-          this.argType = Type.Int;

-          this.argType2 = Type.Real;

-          this.hashCode = 3;

-          break;

         default:

           Contract.Assert(false);

           break;

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index ae307f7a..50fde975 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -325,6 +325,27 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public virtual bool isFloat {

+      get {

+        return false;

+      }

+    }

+    public virtual int FloatMantissa {

+      get {

+        {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        } // Type.FloatMantissa should never be called

+      }

+    }

+    public virtual int FloatExponent {

+      get {

+        {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        } // Type.FloatExponent should never be called

+      }

+    }

     public virtual bool IsBv {

       get {

         return false;

@@ -341,7 +362,6 @@ 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;

 

@@ -364,6 +384,14 @@ namespace Microsoft.Boogie {
       }

     }

 

+    static public FloatType GetFloatType(int exp, int man) {

+      Contract.Requires(0 <= exp);

+      Contract.Requires(0 <= man);

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

+

+      return new FloatType(exp, man);

+    }

+

     //------------ Match formal argument types on actual argument types

     //------------ and return the resulting substitution of type variables

 

@@ -877,8 +905,6 @@ namespace Microsoft.Boogie {
           return "int";

         case SimpleType.Real:

           return "real";

-        case SimpleType.Float:

-          return "float";

         case SimpleType.Bool:

           return "bool";

       }

@@ -1001,11 +1027,6 @@ 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;

@@ -1021,6 +1042,165 @@ namespace Microsoft.Boogie {
 

   //=====================================================================

 

+  //Note that the functions in this class were directly copied from the BV class just below

+  public class FloatType : Type { 

+    public readonly int Mantissa; //Size of mantissa in bits

+    public readonly int Exponent; //Size of exponent in bits

+

+    public FloatType(IToken token, int exponent, int mantissa)

+      : base(token) {

+      Contract.Requires(token != null);

+      Mantissa = mantissa;

+      Exponent = exponent;

+    }

+

+    public FloatType(int exponent, int mantissa)

+      : base(Token.NoToken) {

+      Mantissa = mantissa;

+      Exponent = exponent;

+    }

+

+    //-----------  Cloning  ----------------------------------

+    // We implement our own clone-method, because bound type variables

+    // have to be created in the right way. It is /not/ ok to just clone

+    // everything recursively.

+

+    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap)

+    {

+      //Contract.Requires(cce.NonNullElements(varMap));

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

+      // FloatTypes are immutable anyway, we do not clone

+      return this;

+    }

+

+    public override Type CloneUnresolved()

+    {

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

+      return this;

+    }

+

+    //-----------  Linearisation  ----------------------------------

+

+    public override void Emit(TokenTextWriter stream, int contextBindingStrength)

+    {

+      //Contract.Requires(stream != null);

+      // no parentheses are necessary for bitvector-types

+      stream.SetToken(this);

+      stream.Write("{0}", this);

+    }

+

+    public override string ToString()

+    {

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

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

+    }

+

+    //-----------  Equality  ----------------------------------

+

+    [Pure]

+    public override bool Equals(Type/*!*/ that,

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables)

+    {

+      FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType;

+      return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent;

+    }

+

+    //-----------  Unification of types  -----------

+

+    public override bool Unify(Type/*!*/ that,

+                               List<TypeVariable>/*!*/ unifiableVariables,

+      // an idempotent substitution that describes the

+      // unification result up to a certain point

+                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier)

+    {

+      //Contract.Requires(that != null);

+      //Contract.Requires(unifiableVariables != null);

+      //Contract.Requires(cce.NonNullElements(unifier));

+      that = that.Expanded;

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

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

+      }

+      else {

+        return this.Equals(that);

+      }

+    }

+

+    //-----------  Substitution of free variables with types not containing bound variables  -----------------

+

+    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst)

+    {

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

+      return this;

+    }

+

+    //-----------  Hashcodes  ----------------------------------

+

+    [Pure]

+    public override int GetHashCode(List<TypeVariable> boundVariables)

+    {

+      return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode();

+    }

+

+    //-----------  Resolution  ----------------------------------

+

+    public override Type ResolveType(ResolutionContext rc)

+    {

+      //Contract.Requires(rc != null);

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

+      // nothing to resolve

+      return this;

+    }

+

+    // determine the free variables in a type, in the order in which the variables occur

+    public override List<TypeVariable>/*!*/ FreeVariables

+    {

+      get

+      {

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

+

+        return new List<TypeVariable>();  // bitvector-type are closed

+      }

+    }

+

+    public override List<TypeProxy/*!*/>/*!*/ FreeProxies

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));

+        return new List<TypeProxy/*!*/>();

+      }

+    }

+

+    //-----------  Getters/Issers  ----------------------------------

+

+    public override bool IsFloat {

+      get {

+        return true;

+      }

+    }

+    public override int FloatMantissa {

+      get {

+        return Mantissa;

+      }

+    }

+    public override int FloatExponent {

+      get {

+        return Exponent;

+      }

+    }

+

+    public override Absy StdDispatch(StandardVisitor visitor)

+    {

+      //Contract.Requires(visitor != null);

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

+      return visitor.VisitFloatType(this);

+    }

+

+  }

+

+  //=====================================================================

+

   public class BvType : Type {

     public readonly int Bits;

 

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

     Int,

     Real,

-    Float,

     Bool

   };

 

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

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

    Get();

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

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

+   }

+   else

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

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

 			Get();

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

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 0323d4db..97215cfb 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,6 +103,12 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Type>() != null);

       return this.VisitType(node);

     }

+    public virtual Type VisitFloatType(FloatType node)

+    {

+      Contract.Requires(node != null);

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

+      return this.VisitType(node);

+    }

     public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {

       Contract.Requires(node != null);

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

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index b834aa6b..c7ae9d57 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 "Real"; //TODO: Make to be a float

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

       else if (t.IsBv) {

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

       } else {

@@ -690,7 +690,7 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

-      {

+      { //TODO: match z3

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

         return true;

       }

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4a1331c5..2b09362b 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,6 +93,7 @@ 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/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 942116eb..f0dc505d 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -1005,12 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST {
         if (cce.NonNull(e.Type).IsInt) {

           return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);

         }

-        else if (cce.NonNull(e.Type).IsReal) {

+        else {// if (cce.NonNull(e.Type).IsReal) {

           return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);

         }

-        else  {//is float

-          return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e);

-        } 

+        //else  {//is float

+          //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e);

+        //} 

       }

       else {

         return Gen.Not(this.args);

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 4632b1e4..5e821ea2 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1424,13 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return CastArguments(node, Type.Real, bindings, 0);

     }

-    public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)

+    /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)

     {

       Contract.Requires((bindings != null));

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

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

       return CastArguments(node, Type.Float, bindings, 0);

-    }

+    }*/

     public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

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

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 291d6d42..36692f30 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -324,16 +324,16 @@ namespace Microsoft.Boogie {
 

     public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);

-    public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float);

+    //public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);

-    public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float);

+   // public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);

-    public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float);

+    //public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);

-    public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float);

+    //public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float);

     public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);

     public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real);

     public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);

@@ -347,7 +347,7 @@ namespace Microsoft.Boogie {
     public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();

     public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int);

     public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real);

-    public static readonly VCExprOp ToFloatOp = new VCExprNAryOp(1, Type.Float);

+    //public static readonly VCExprOp ToFloatOp = new VCExprNAryOp(1, Type.Float);

 

     public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);

 

@@ -433,13 +433,16 @@ namespace Microsoft.Boogie {
       SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);

       SingletonOpDict.Add(AddIOp, SingletonOp.AddOp);

       SingletonOpDict.Add(AddROp, SingletonOp.AddOp);

+      //SingletonOpDict.Add(AddFOp, SingletonOp.AddOp);

       SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);

       SingletonOpDict.Add(SubROp, SingletonOp.SubOp);

+      //SingletonOpDict.Add(SubFOp, SingletonOp.SubOp);

       SingletonOpDict.Add(MulIOp, SingletonOp.MulOp);

       SingletonOpDict.Add(MulROp, SingletonOp.MulOp);

+      //SingletonOpDict.Add(MulFOp, SingletonOp.MulOp);

       SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);

       SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);

-      SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp);

+      //SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp);

       SingletonOpDict.Add(ModOp, SingletonOp.ModOp);

       SingletonOpDict.Add(PowOp, SingletonOp.PowOp);

       SingletonOpDict.Add(LtOp, SingletonOp.LtOp);

@@ -450,7 +453,7 @@ namespace Microsoft.Boogie {
       SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);

       SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);

       SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);

-      SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp);

+      //SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp);

     }

 

     ////////////////////////////////////////////////////////////////////////////////

@@ -876,7 +879,7 @@ namespace Microsoft.Boogie.VCExprAST {
   {

     public readonly BigFloat Val;

     internal VCExprFloatLit(BigFloat val)

-      : base(Type.Float)

+      : base(Type.GetFloatType(val.ExponentSize, val.MantissaSize))

     {

       this.Val = val;

     }