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, 22 insertions, 2 deletions

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index adb3b27e..00e6fb9c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -290,12 +290,22 @@ namespace Microsoft.Boogie.VCExprAST {
     public bool VisitDivOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

-      return PrintNAry("/", node, wr);

+      return PrintNAry("div", node, wr);

     }

     public bool VisitModOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

-      return PrintNAry("%", node, wr);

+      return PrintNAry("mod", node, wr);

+    }

+    public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("/", node, wr);

+    }

+    public bool VisitPowOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("**", node, wr);

     }

     public bool VisitLtOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

@@ -327,6 +337,16 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("<::", node, wr);

     }

+    public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("int", node, wr);

+    }

+    public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("real", node, wr);

+    }

     public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);