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, 4 insertions, 4 deletions

diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs
index 7eb93541..879ab6d6 100644
--- a/Source/VCExpr/BigLiteralAbstracter.cs
+++ b/Source/VCExpr/BigLiteralAbstracter.cs
@@ -120,7 +120,7 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       if (lit.IsNegative)

-        return Gen.Function(VCExpressionGenerator.SubOp,

+        return Gen.Function(VCExpressionGenerator.SubIOp,

                             Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));

       else

         return RepresentPos(lit);

@@ -145,7 +145,7 @@ namespace Microsoft.Boogie.VCExprAST {
         BigNum dist = lit - Literals[index - 1].Key;

         if (dist < resDistance) {

           resDistance = dist;

-          res = Gen.Function(VCExpressionGenerator.AddOp,

+          res = Gen.Function(VCExpressionGenerator.AddIOp,

                              Literals[index - 1].Value, Gen.Integer(dist));

         }

       }

@@ -154,7 +154,7 @@ namespace Microsoft.Boogie.VCExprAST {
         BigNum dist = Literals[index].Key - lit;

         if (dist < resDistance) {

           resDistance = dist;

-          res = Gen.Function(VCExpressionGenerator.SubOp,

+          res = Gen.Function(VCExpressionGenerator.SubIOp,

                              Literals[index].Value, Gen.Integer(dist));

         }

       }

@@ -198,7 +198,7 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Requires(bExpr != null);

 

       BigNum dist = bValue - aValue;

-      VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr);

+      VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubIOp, bExpr, aExpr);

       if (dist <= ConstantDistanceTPO)

         // constants that are sufficiently close to each other are put

         // into a precise relationship