Merge pull request #35 from Checkmate50/master

Floating Point Support

1 files changed, 91 insertions, 0 deletions

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 76340f97..c2d99d77 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1424,6 +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)
+    {
+      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));
@@ -1472,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
       return CastArgumentsToOldType(node, bindings, 0);
     }
+    public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
     public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {
       Contract.Requires((bindings != null));
       Contract.Requires((node != null));