From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001
From: boehmes <unknown>
Date: Thu, 27 Sep 2012 17:13:45 +0200
Subject: Boogie: added type 'real' with overloaded arithmetic operations plus
 real division '/' and (uninterpreted) real exponentiation '**', real literals
 and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod'
 are now mapped to corresponding SMT-LIB operations instead of treating them
 uninterpreted; Made unary minus valid Boogie syntax again (the expression '-
 e' used to be rewritten by the parser to '0 - e', now this is done when
 generating VCs); Extended the BigDec class with additional functionality;
 Added test cases for SMT-LIB prover backend (the Z3 API interface has been
 adapted accordingly, but is untested)

---
 Source/VCExpr/VCExprASTVisitors.cs | 40 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

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

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 1a29bbeb..1dd1cac9 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -75,12 +75,16 @@ namespace Microsoft.Boogie.VCExprAST {
     Result VisitMulOp(VCExprNAry node, Arg arg);
     Result VisitDivOp(VCExprNAry node, Arg arg);
     Result VisitModOp(VCExprNAry node, Arg arg);
+    Result VisitRealDivOp(VCExprNAry node, Arg arg);
+    Result VisitPowOp(VCExprNAry node, Arg arg);
     Result VisitLtOp(VCExprNAry node, Arg arg);
     Result VisitLeOp(VCExprNAry node, Arg arg);
     Result VisitGtOp(VCExprNAry node, Arg arg);
     Result VisitGeOp(VCExprNAry node, Arg arg);
     Result VisitSubtypeOp(VCExprNAry node, Arg arg);
     Result VisitSubtype3Op(VCExprNAry node, Arg arg);
+    Result VisitToIntOp(VCExprNAry node, Arg arg);
+    Result VisitToRealOp(VCExprNAry node, Arg arg);
     Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg);
     Result VisitIfThenElseOp(VCExprNAry node, Arg arg);
     Result VisitCustomOp(VCExprNAry node, Arg arg);
@@ -179,6 +183,16 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();
     }
 
+    public Result VisitRealDivOp(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();
+    }
+
     public Result VisitLtOp(VCExprNAry node, Arg arg) {
       Contract.Requires(node != null);
       throw new NotImplementedException();
@@ -209,6 +223,16 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();
     }
 
+    public Result VisitToIntOp(VCExprNAry node, Arg arg) {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitToRealOp(VCExprNAry node, Arg arg) {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
     public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
       Contract.Requires(node != null);
       throw new NotImplementedException();
@@ -1427,6 +1451,14 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
     }
+    public virtual Result VisitRealDivOp(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);
+    }
     public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
@@ -1451,6 +1483,14 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
     }
+    public virtual Result VisitToIntOp(VCExprNAry node, Arg arg) {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitToRealOp(VCExprNAry node, Arg arg) {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
     public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
-- 
cgit v1.2.3