From d213a71b16a344dab7ac5d08507668abebffd21e Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 4 May 2015 03:46:22 -0600
Subject: integrated the named float type to act as a real in boogie

---
 Source/Provers/SMTLib/SMTLibLineariser.cs  | 13 ++++++++++++-
 Source/Provers/SMTLib/TypeDeclCollector.cs |  2 +-
 2 files changed, 13 insertions(+), 2 deletions(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 6accf79f..b834aa6b 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -116,7 +116,7 @@ namespace Microsoft.Boogie.SMTLib
           }
           sb.Append(']');
           TypeToStringHelper(m.Result, sb);
-        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) {
+        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv) {
           sb.Append(TypeToString(t));
         } else {
           System.IO.StringWriter buffer = new System.IO.StringWriter();
@@ -140,6 +140,8 @@ namespace Microsoft.Boogie.SMTLib
         return "Int";
       else if (t.IsReal)
         return "Real";
+      else if (t.IsFloat)
+        return "Real"; //TODO: Make to be a float
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
@@ -199,6 +201,15 @@ namespace Microsoft.Boogie.SMTLib
         else
           wr.Write(lit.ToDecimalString());
       }
+      else if (node is VCExprFloatLit)
+      {
+        BigFloat lit = ((VCExprFloatLit)node).Val;
+        if (lit.IsNegative)
+          // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
+          wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
+        else
+          wr.Write(lit.ToDecimalString());
+      }
       else {
         Contract.Assert(false);
         throw new cce.UnreachableException();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 30363102..2b053410 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -296,7 +296,7 @@ void ObjectInvariant()
         return;
       }
 
-      if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
+      if (type.IsBool || type.IsInt || type.IsReal || type.IsFloat || type.IsBv)
         return;
 
       CtorType ctorType = type as CtorType;
-- 
cgit v1.2.3