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, 39 insertions, 8 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;

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 5629c0d6..101b07a0 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -22,8 +22,8 @@ namespace Microsoft.Boogie.SMTLib
       // Core theory:

       "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool",

       "=>", // implies (sic!)

-      // Integers

-      "Int", "*", "/", "-", "+", "<", "<=", ">", ">=",

+      // Integers and reals

+      "Int", "Real", "*", "/", "-", "+", "<", "<=", ">", ">=", "div", "mod",

       // Bitvectors

       "extract", "concat", 

       "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",

@@ -48,7 +48,7 @@ namespace Microsoft.Boogie.SMTLib
       "lblneg", "lblpos", "lbl-lit",

       "if", "&&", "||", "equals", "equiv", "bool",

       // Boogie-defined

-      "int_mod", "int_div", "UOrdering2", "UOrdering3", 

+      "real_pow", "UOrdering2", "UOrdering3", 

     };

 

     static HashSet<string> reservedSmtWords;

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index a4bdee51..bff949ea 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -255,7 +255,7 @@ void ObjectInvariant()
         return;

       }

 

-      if (type.IsBool || type.IsInt || type.IsBv)

+      if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)

         return;

 

       CtorType ctorType = type as CtorType;