From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001
From: boehmes <unknown>
Date: Thu, 27 Sep 2012 17:13:45 +0200
Subject: 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)

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 39 +++++++++++++++++++++++++++----
 1 file changed, 35 insertions(+), 4 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

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;
-- 
cgit v1.2.3