From 0324757fb1a12d76861a51be988690bf8de75f64 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Wed, 14 Oct 2015 12:57:50 -0600
Subject: Modified translation so that z3 runs with type checking for simple
 binary operations

---
 Source/VCExpr/VCExprASTVisitors.cs | 154 ++++++++++++++++++++++++++++++++++---
 1 file changed, 143 insertions(+), 11 deletions(-)

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

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index a1fb2ff4..c81f69e5 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST {
     Result VisitLabelOp(VCExprNAry node, Arg arg);
     Result VisitSelectOp(VCExprNAry node, Arg arg);
     Result VisitStoreOp(VCExprNAry node, Arg arg);
+    Result VisitFloatAddOp(VCExprNAry node, Arg arg);
+    Result VisitFloatSubOp(VCExprNAry node, Arg arg);
+    Result VisitFloatMulOp(VCExprNAry node, Arg arg);
+    Result VisitFloatDivOp(VCExprNAry node, Arg arg);
+    Result VisitFloatRemOp(VCExprNAry node, Arg arg);
+    Result VisitFloatMinOp(VCExprNAry node, Arg arg);
+    Result VisitFloatMaxOp(VCExprNAry node, Arg arg);
+    Result VisitFloatLeqOp(VCExprNAry node, Arg arg);
+    Result VisitFloatLtOp(VCExprNAry node, Arg arg);
+    Result VisitFloatGeqOp(VCExprNAry node, Arg arg);
+    Result VisitFloatGtOp(VCExprNAry node, Arg arg);
+    Result VisitFloatEqOp(VCExprNAry node, Arg arg);
     Result VisitBvOp(VCExprNAry node, Arg arg);
     Result VisitBvExtractOp(VCExprNAry node, Arg arg);
     Result VisitBvConcatOp(VCExprNAry node, Arg arg);
@@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();
     }
 
+    public Result VisitFloatAddOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatRemOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
     public Result VisitBvOp(VCExprNAry node, Arg arg) {
       Contract.Requires(node != null);
       throw new NotImplementedException();
@@ -189,12 +273,6 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();
     }
 
-    public Result VisitFloatDivOp(VCExprNAry node, Arg arg)
-    {
-      Contract.Requires(node != null);
-      throw new NotImplementedException();
-    }
-
     public Result VisitPowOp(VCExprNAry node, Arg arg) {
       Contract.Requires(node != null);
       throw new NotImplementedException();
@@ -1450,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
     }
+    public virtual Result VisitFloatAddOp(VCExprNAry node, Arg arg) {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatRemOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
     public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
@@ -1494,11 +1631,6 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
     }
-    public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg)
-    {
-      //Contract.Requires(node != null);
-      return StandardResult(node, arg);
-    }
     public virtual Result VisitPowOp(VCExprNAry node, Arg arg) {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
-- 
cgit v1.2.3