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

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 6a2cbb6a..cf125c76 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -115,7 +115,7 @@ namespace Microsoft.Boogie.SMTLib
           }

           sb.Append(']');

           TypeToStringHelper(m.Result, sb);

-        } else if (t.IsBool || t.IsInt || t.IsBv) {

+        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) {

           sb.Append(TypeToString(t));

         } else {

           System.IO.StringWriter buffer = new System.IO.StringWriter();

@@ -137,6 +137,8 @@ namespace Microsoft.Boogie.SMTLib
         return "Bool";

       else if (t.IsInt)

         return "Int";

+      else if (t.IsReal)

+        return "Real";

       else if (t.IsBv) {

         return "(_ BitVec " + t.BvBits + ")";

       } else {

@@ -181,7 +183,16 @@ namespace Microsoft.Boogie.SMTLib
           wr.Write("(- 0 {0})", lit.Abs);

         else

           wr.Write(lit);

-      } else {

+      } 

+      else if (node is VCExprRealLit) {

+        BigDec lit = ((VCExprRealLit)node).Val;

+        if (lit.IsNegative)

+          // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")

+          wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString(20));

+        else

+          wr.Write(lit.ToDecimalString(20));

+      }

+      else {

         Contract.Assert(false);

         throw new cce.UnreachableException();

       }

@@ -609,13 +620,23 @@ namespace Microsoft.Boogie.SMTLib
 

       public bool VisitDivOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("int_div", node, options);

+        WriteApplication("div", node, options);

         return true;

       }

 

       public bool VisitModOp(VCExprNAry node, LineariserOptions options)

       {

-        WriteApplication("int_mod", node, options);

+        WriteApplication("mod", node, options);

+        return true;

+      }

+

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

+        WriteApplication("/", node, options);

+        return true;

+      }

+

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

+        WriteApplication("real_pow", node, options);

         return true;

       }

 

@@ -655,6 +676,16 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

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

+        WriteApplication("to_int", node, options);

+        return true;

+      }

+

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

+        WriteApplication("to_real", node, options);

+        return true;

+      }

+

       private string ExtractDatatype(Function func) {

         if (func is DatatypeSelector) {

           DatatypeSelector selector = (DatatypeSelector) func;