From 28a20e6eba2919e008f70874b4c12a3ce7ad049c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Thu, 17 Sep 2015 03:14:27 -0600
Subject: Added initial support for float addition

---
 Source/VCExpr/VCExprAST.cs | 62 +++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 59 insertions(+), 3 deletions(-)

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

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 36692f30..c44800fc 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -357,6 +357,15 @@ namespace Microsoft.Boogie {
       return new VCExprBoogieFunctionOp(func);
     }
 
+    // Float nodes
+
+    public VCExpr AddFOp(VCExpr f1, VCExpr f2)
+    {
+      Contract.Requires(f1 != null);
+      Contract.Requires(f2 != null);
+      return Function(new VCExprFloatOp(f1.Type.FloatExponent, f1.Type.FloatMantissa));
+    }
+
     // Bitvector nodes
 
     public VCExpr Bitvector(BvConst bv) {
@@ -403,7 +412,6 @@ namespace Microsoft.Boogie {
       DivOp,
       ModOp,
       RealDivOp,
-      FloatDivOp,
       PowOp,
       LtOp,
       LeOp,
@@ -1309,8 +1317,6 @@ namespace Microsoft.Boogie.VCExprAST {
             return visitor.VisitModOp(expr, arg);
           case VCExpressionGenerator.SingletonOp.RealDivOp:
             return visitor.VisitRealDivOp(expr, arg);
-          case VCExpressionGenerator.SingletonOp.FloatDivOp:
-            return visitor.VisitFloatDivOp(expr, arg);
           case VCExpressionGenerator.SingletonOp.PowOp:
             return visitor.VisitPowOp(expr, arg);
           case VCExpressionGenerator.SingletonOp.LtOp:
@@ -1668,6 +1674,56 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
+  /////////////////////////////////////////////////////////////////////////////////
+  // Float operators
+
+  public class VCExprFloatOp : VCExprOp {
+    public readonly int Mantissa;
+    public readonly int Exponent;
+
+    public override int Arity {
+      get {
+        return 1;
+      }
+    }
+    public override int TypeParamArity {
+      get {
+        return 0;
+      }
+    }
+    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+      //Contract.Requires(cce.NonNullElements(typeArgs));
+      //Contract.Requires(cce.NonNullElements(args));
+      Contract.Ensures(Contract.Result<Type>() != null);
+      return Type.GetFloatType(Exponent, Mantissa);
+    }
+
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override bool Equals(object that) {
+      if (Object.ReferenceEquals(this, that))
+        return true;
+      if (that is VCExprFloatOp)
+        return this.Exponent == ((VCExprFloatOp)that).Exponent && this.Mantissa == ((VCExprFloatOp)that).Mantissa;
+      return false;
+    }
+    [Pure]
+    public override int GetHashCode() {
+      return Exponent * 81748912 + Mantissa * 67867979;
+    }
+
+    internal VCExprFloatOp(int exp, int man) {
+      this.Exponent = exp;
+      this.Mantissa = man;
+    }
+    public override Result Accept<Result, Arg>
+           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+      //Contract.Requires(visitor != null);
+      //Contract.Requires(expr != null);
+      return visitor.VisitBvOp(expr, arg);
+    }
+  }
+
   /////////////////////////////////////////////////////////////////////////////////
   // Bitvector operators
 
-- 
cgit v1.2.3