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, 62 insertions, 6 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 1561aec0..3035c9de 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -328,6 +328,8 @@ namespace Microsoft.Boogie.VCExprAST {
         }

       } else if (node.Val is BigNum) {

         return Gen.Integer(node.asBigNum);

+      } else if (node.Val is BigDec) {

+        return Gen.Real(node.asBigDec);

       } else if (node.Val is BvConst) {

         return Gen.Bitvector((BvConst)node.Val);

       } else {

@@ -961,8 +963,20 @@ namespace Microsoft.Boogie.VCExprAST {
     public VCExpr Visit(UnaryOperator unaryOperator) {

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

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1);

-      return Gen.Not(this.args);

+      Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Neg || unaryOperator.Op == UnaryOperator.Opcode.Not);

+      Contract.Assert(this.args.Count == 1);

+      if (unaryOperator.Op == UnaryOperator.Opcode.Neg) {

+        VCExpr e = cce.NonNull(this.args[0]);

+        if (cce.NonNull(e.Type).IsInt) {

+          return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);

+        }

+        else {

+          return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);

+        }

+      }

+      else {

+        return Gen.Not(this.args);

+      }

     }

 

     public VCExpr Visit(BinaryOperator binaryOperator) {

@@ -996,6 +1010,21 @@ namespace Microsoft.Boogie.VCExprAST {
       return this.args[0];

     }

 

+    public VCExpr Visit(ArithmeticCoercion arithCoercion) {

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

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      Contract.Assert(this.args.Count == 1);

+      switch (arithCoercion.Coercion) {

+        case ArithmeticCoercion.CoercionType.ToInt:

+          return Gen.Function(VCExpressionGenerator.ToIntOp, this.args);

+        case ArithmeticCoercion.CoercionType.ToReal:

+          return Gen.Function(VCExpressionGenerator.ToRealOp, this.args);

+        default:

+          Contract.Assert(false);

+          return null;

+      }

+    }

+

     public VCExpr Visit(IfThenElse ite) {

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

       Contract.Ensures(Contract.Result<VCExpr>() != null);

@@ -1012,15 +1041,42 @@ namespace Microsoft.Boogie.VCExprAST {
 

       switch (app.Op) {

         case BinaryOperator.Opcode.Add:

-          return Gen.Function(VCExpressionGenerator.AddOp, args);

+          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {

+            return Gen.Function(VCExpressionGenerator.AddIOp, args);

+          }

+          else {

+            return Gen.Function(VCExpressionGenerator.AddROp, args);

+          }

         case BinaryOperator.Opcode.Sub:

-          return Gen.Function(VCExpressionGenerator.SubOp, args);

+          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {

+            return Gen.Function(VCExpressionGenerator.SubIOp, args);

+          }

+          else {

+            return Gen.Function(VCExpressionGenerator.SubROp, args);

+          }

         case BinaryOperator.Opcode.Mul:

-          return Gen.Function(VCExpressionGenerator.MulOp, args);

+          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {

+            return Gen.Function(VCExpressionGenerator.MulIOp, args);

+          }

+          else {

+            return Gen.Function(VCExpressionGenerator.MulROp, args);

+          }

         case BinaryOperator.Opcode.Div:

-          return Gen.Function(VCExpressionGenerator.DivOp, args);

+          return Gen.Function(VCExpressionGenerator.DivIOp, args);

         case BinaryOperator.Opcode.Mod:

           return Gen.Function(VCExpressionGenerator.ModOp, args);

+        case BinaryOperator.Opcode.RealDiv:

+          VCExpr arg0 = cce.NonNull(args[0]);

+          VCExpr arg1 = cce.NonNull(args[1]);

+          if (cce.NonNull(arg0.Type).IsInt) {

+            arg0 = Gen.Function(VCExpressionGenerator.ToRealOp, arg0);

+          }

+          if (cce.NonNull(arg1.Type).IsInt) {

+            arg1 = Gen.Function(VCExpressionGenerator.ToRealOp, arg1);

+          }

+          return Gen.Function(VCExpressionGenerator.DivROp, arg0, arg1);

+        case BinaryOperator.Opcode.Pow:

+          return Gen.Function(VCExpressionGenerator.PowOp, args);

         case BinaryOperator.Opcode.Eq:

         case BinaryOperator.Opcode.Iff:

           // we don't distinguish between equality and equivalence at this point