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)

3 files changed, 93 insertions, 14 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index df40df3d..ad0c2239 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -139,8 +139,12 @@ namespace Microsoft.Boogie.Z3 {
             {

                 case TermKind.Numeral:

                     var numstr = arg.GetNumeralString();

-                    var bignum = Basetypes.BigNum.FromString(numstr);

-                    res = gen.Integer(bignum);

+                    if (arg.GetSort().GetSortKind() == SortKind.Int) {

+                      res = gen.Integer(Basetypes.BigNum.FromString(numstr));

+                    }

+                    else {

+                      res = gen.Real(Basetypes.BigDec.FromString(numstr));

+                    }

                     break;

                 case TermKind.App:

                     var args = arg.GetAppArgs();

@@ -151,8 +155,14 @@ namespace Microsoft.Boogie.Z3 {
                     switch (arg.GetAppDecl().GetKind())

                     {

                         case DeclKind.Add:

-                            if (vcargs.Length == 0)

-                                res = gen.Integer(Basetypes.BigNum.FromInt(0));

+                            if (vcargs.Length == 0) {

+                              if (arg.GetSort().GetSortKind() == SortKind.Int) {

+                                res = gen.Integer(Basetypes.BigNum.ZERO);

+                              }

+                              else {

+                                res = gen.Real(Basetypes.BigDec.ZERO);

+                              }

+                            }

                             else

                             {

                                 res = vcargs[0];

@@ -167,7 +177,7 @@ namespace Microsoft.Boogie.Z3 {
                             break;

                         case DeclKind.Div:

                             Debug.Assert(vcargs.Length == 2);

-                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);

+                            res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]);

                             break;

                         case DeclKind.Eq:

                             Debug.Assert(vcargs.Length == 2);

@@ -243,8 +253,22 @@ namespace Microsoft.Boogie.Z3 {
                             break;

                         case DeclKind.Uminus:

                             Debug.Assert(vcargs.Length == 1);

-                            var bigzero = Basetypes.BigNum.FromInt(0);

-                            res = gen.Function(VCExpressionGenerator.SubOp, gen.Integer(bigzero), vcargs[0]);

+                            var argzero = null;

+                            if (vcargs[0].Type.IsInt) {

+                              argzero = gen.Integer(Basetypes.BigNum.ZERO);

+                            }

+                            else {

+                              argzero = gen.Real(Basetypes.BigDec.ZERO);

+                            }

+                            res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]);

+                            break;

+                        case DeclKind.ToInt:

+                            Debug.Assert(vcargs.Length == 1);

+                            res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]);

+                            break;

+                        case DeclKind.ToReal:

+                            Debug.Assert(vcargs.Length == 1);

+                            res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]);

                             break;

                         case DeclKind.Uninterpreted:

                             var name = arg.GetAppDecl().GetDeclName();

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index e1c6de0b..879211f7 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -51,7 +51,8 @@ namespace Microsoft.Boogie.Z3
             public bool Equals(BasicType x, BasicType y)

             {

                 return (x.IsBool == y.IsBool) &&

-                       (x.IsInt == y.IsInt);

+                       (x.IsInt == y.IsInt) &&

+                       (x.IsReal == y.IsReal);

             }

 

             public int GetHashCode(BasicType basicType)

@@ -60,6 +61,8 @@ namespace Microsoft.Boogie.Z3
                     return 1;

                 else if (basicType.IsInt)

                     return 2;

+                else if (basicType.IsReal)

+                  return 3;

                 else

                     throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");

             }

@@ -175,6 +178,10 @@ namespace Microsoft.Boogie.Z3
             {

                 typeAst = z3.MkIntSort();

             }

+            else if (basicType.IsReal)

+            {

+                typeAst = z3.MkRealSort();

+            }

             else

                 throw new Exception("Unknown Basic Type " + basicType.ToString());

             return typeAst;

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index 0605a854..e56a7950 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -15,6 +15,8 @@ using Microsoft.Z3;
 

 namespace Microsoft.Boogie.Z3

 {

+    using System.Numerics.BigInteger;

+

     public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>

     {

         private Z3apiOpLineariser opLineariser = null;

@@ -110,7 +112,7 @@ namespace Microsoft.Boogie.Z3
             return z3.MkSub(unwrapChildren);

           }

 

-          if (op == VCExpressionGenerator.DivOp) {

+          if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) {

             return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);

           }

 

@@ -126,6 +128,14 @@ namespace Microsoft.Boogie.Z3
             return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);

           }

 

+          if (op == VCExpressionGenerator.ToIntOp) {

+            return z3.MkToInt(unwrapChildren[0]);

+          }

+

+          if (op == VCExpressionGenerator.ToRealOp) {

+            return z3.MkToReal(unwrapChildren[0]);

+          }

+

           throw new Exception("unhandled boogie operator");

         }

 

@@ -139,11 +149,25 @@ namespace Microsoft.Boogie.Z3
             else if (node == VCExpressionGenerator.False)

                 return cm.z3.MkFalse();

             else if (node is VCExprIntLit)

-              return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());

-            else

-            {

-                Contract.Assert(false);

-                throw new cce.UnreachableException();

+                return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());

+            else if (node is VCExprRealLit) {

+                string m = ((VCExprRealLit)node).Val.Mantissa.ToString();

+                BigInteger e = ((VCExprRealLit)node).Val.Exponent;

+                string f = BigInteger.Pow(10, e.Abs);

+

+                if (e == 0) {

+                    return cm.z3.MkNumeral(m, cm.z3.MkRealSort());

+                }

+                else if (((VCExprRealLit)node).Val.Exponent > 0) {

+                    return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));

+                }

+                else {

+                    return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));

+                }

+            }

+            else {

+              Contract.Assert(false);

+              throw new cce.UnreachableException();

             }

         }

 

@@ -548,6 +572,18 @@ namespace Microsoft.Boogie.Z3
                 return WriteApplication(node.Op, node, options);

             }

 

+            public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

+              return WriteApplication(node.Op, node, options);

+            }

+

+            public Term VisitPowOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

+              return WriteApplication(node.Op, node, options);

+            }

+

             public Term VisitLtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

@@ -590,6 +626,18 @@ namespace Microsoft.Boogie.Z3
                 return WriteApplication(node.Op, node, options);

             }

 

+            public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

+              return WriteApplication(node.Op, node, options);

+            }

+

+            public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

+              return WriteApplication(node.Op, node, options);

+            }

+

             public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);