diff options
| author |  MichalMoskal <unknown> | 2011-02-16 00:17:01 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-16 00:17:01 +0000 |
| commit | 8205927a5e3d42700db73583aa1291d7543b23e5 (patch) | |
| tree | be906befa580694de1b9eac28bdacbeee2901af5 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | 4ffa81d2c6df5570ae36b4bd01495e185bc15dac (diff) | |
Fix printing of type-proxies
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 51 |
1 files changed, 41 insertions, 10 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)
|