integrated the named float type to act as a real in boogie

3 files changed, 20 insertions, 2 deletions

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;

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 2326ba7a..4632b1e4 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1424,6 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return CastArguments(node, Type.Real, bindings, 0);

     }

+    public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)

+    {

+      Contract.Requires((bindings != null));

+      Contract.Requires((node != null));

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      return CastArguments(node, Type.Float, bindings, 0);

+    }

     public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));