From 8205927a5e3d42700db73583aa1291d7543b23e5 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 16 Feb 2011 00:17:01 +0000
Subject: Fix printing of type-proxies

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 51 +++++++++++++++++++++++++------
 Source/Provers/SMTLib/SMTLibNamer.cs      |  2 +-
 2 files changed, 42 insertions(+), 11 deletions(-)

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 317a6eed..7df58b9e 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -89,7 +89,39 @@ namespace Microsoft.Boogie.SMTLib
 
     /////////////////////////////////////////////////////////////////////////////////////
 
-    internal static string TypeToString(Type t)
+    private static void TypeToStringHelper(Type t, StringBuilder sb)
+    {
+      Contract.Requires(t != null);
+
+      TypeSynonymAnnotation syn = t as TypeSynonymAnnotation;
+      if (syn != null) {
+        TypeToStringHelper(syn.ExpandedType, sb);
+      } else {
+        if (t.IsMap) {
+          MapType m = t.AsMap;
+          sb.Append('[');
+          for (int i = 0; i < m.MapArity; ++i) {
+            if (i != 0)
+              sb.Append(',');
+            TypeToStringHelper(m.Arguments[i], sb);
+          }
+          sb.Append(']');
+          TypeToStringHelper(m.Result, sb);
+        } else if (t.IsBool || t.IsInt || t.IsBv) {
+          sb.Append(TypeToString(t));
+        } else {
+          System.IO.StringWriter buffer = new System.IO.StringWriter();
+          using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+            t.Emit(stream);
+          }
+          sb.Append(buffer.ToString());
+        }
+      }
+
+    }
+
+
+    public static string TypeToString(Type t)
     {
       Contract.Requires(t != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -100,18 +132,17 @@ namespace Microsoft.Boogie.SMTLib
         return "Int";
       else if (t.IsBv) {
         Contract.Assert(false);
-        throw new cce.UnreachableException();
-      } // bitvectors are currently not handled for SMT-Lib solvers
-      else {
-        // at this point, only the types U, T should be left (except when /typeEncoding:m is used)
-        System.IO.StringWriter buffer = new System.IO.StringWriter();
-        using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
-          t.Emit(stream);
-        }
-        return SMTLibNamer.QuoteId("T@" + buffer.ToString());
+        return "$bv" + t.BvBits;
+      } else {
+        StringBuilder sb = new StringBuilder();
+        sb.Append("T@");
+        TypeToStringHelper(t, sb);
+        return SMTLibNamer.QuoteId(sb.ToString());
       }
     }
 
+
+
     /////////////////////////////////////////////////////////////////////////////////////
 
     public bool Visit(VCExprLiteral node, LineariserOptions options)
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 3de2e81d..2f8e86c8 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -104,7 +104,7 @@ namespace Microsoft.Boogie.SMTLib
 
     public SMTLibNamer()
     {
-      this.Spacer = "@@";
+      this.Spacer = "__";
       InitSymbolLists();
     }
   }
-- 
cgit v1.2.3