diff options
| author |  MichalMoskal <unknown> | 2011-02-18 22:05:07 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-18 22:05:07 +0000 |
| commit | 6cd02de973f4160bfb5dc22ad0ddaa7b5600eda9 (patch) | |
| tree | d4940d70ad22c2f8ea7cdaeaea340d79f17c42d3 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | 192f8e8429c32ae6501c01c1f37033f4a893dd48 (diff) | |
Handle /useArrayTheory
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index f7a682ad..3c6c611c 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -97,7 +97,15 @@ namespace Microsoft.Boogie.SMTLib if (syn != null) {
TypeToStringHelper(syn.ExpandedType, sb);
} else {
- if (t.IsMap) {
+ if (t.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
+ MapType m = t.AsMap;
+ Contract.Assert(m.MapArity == 1);
+ sb.Append("(Array ");
+ TypeToStringHelper(m.Arguments[0], sb);
+ sb.Append(" ");
+ TypeToStringHelper(m.Result, sb);
+ sb.Append(")");
+ } else if (t.IsMap) {
MapType m = t.AsMap;
sb.Append('[');
for (int i = 0; i < m.MapArity; ++i) {
@@ -132,10 +140,13 @@ namespace Microsoft.Boogie.SMTLib else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
- StringBuilder sb = new StringBuilder();
- sb.Append("T@");
+ StringBuilder sb = new StringBuilder();
TypeToStringHelper(t, sb);
- return SMTLibNamer.QuoteId(sb.ToString());
+ var s = sb.ToString();
+ if (s[0] == '(')
+ return s;
+ else
+ return SMTLibNamer.QuoteId("T@" + s);
}
}
|