Modified translation so that z3 runs with type checking for simple binary operations

1 files changed, 143 insertions, 11 deletions

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);