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)

1 files changed, 40 insertions, 0 deletions

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