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

1 files changed, 11 insertions, 8 deletions

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;

     }