From 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 13 Jul 2015 19:40:09 -0600
Subject: Modified internal abstract float representation to allow user-defined
 mantissa and exponent

---
 Source/VCExpr/VCExprAST.cs | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'Source/VCExpr/VCExprAST.cs')

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;
     }
-- 
cgit v1.2.3