diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-09-03 14:43:05 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-09-03 14:43:05 -0700 |
| commit | 982548560d971b07dcaefb39f186833186724570 (patch) | |
| tree | 83b393aaad44e856e6ef1941c9e7f019752fed27 /Source/Provers/SMTLib | |
| parent | 36d78b7b41cd10fd026c948718c33f758b3a15d8 (diff) | |
further fixes; temporarily commented out
Diffstat (limited to 'Source/Provers/SMTLib')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 7eafbdfb..34a8502a 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -668,19 +668,28 @@ namespace Microsoft.Boogie.SMTLib printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
Contract.Assert(printedName != null);
- printedName = CheckMapApply(printedName, node);
+ //printedName = CheckMapApply(printedName, node);
WriteApplication(printedName, node, options);
return true;
}
+ private static Type ResultType(Type type) {
+ MapType mapType = type as MapType;
+ if (mapType != null) {
+ return ResultType(mapType.Result);
+ }
+ else {
+ return type;
+ }
+ }
+
private static string CheckMapApply(string name, VCExprNAry node) {
- MapType mapType = node.Type as MapType;
- Contract.Assume(mapType != null);
if (name == "MapConst") {
StringBuilder sb = new StringBuilder();
- TypeToStringHelper(node.Type, sb);
+ Type type = node.Type;
+ TypeToStringHelper(type, sb);
return "(as const " + sb.ToString() + ")";
}
else if (name == "MapAdd") {
@@ -698,14 +707,16 @@ namespace Microsoft.Boogie.SMTLib else if (name == "MapMod") {
return "(_ map (mod (Int Int) Int))";
}
- else if (name == "MapEq" || name == "MapIff") {
- MapType argType = node[0].Type as MapType;
- Contract.Assume(argType != null);
+ else if (name == "MapEq") {
+ Type type = ResultType(node[0].Type);
StringBuilder sb = new StringBuilder();
- TypeToStringHelper(argType.Result, sb);
+ TypeToStringHelper(type, sb);
string s = sb.ToString();
return "(_ map (= (" + s + " " + s + ") Bool))";
}
+ else if (name == "MapIff") {
+ return "(_ map (= (Bool Bool) Bool))";
+ }
else if (name == "MapGt") {
return "(_ map (> (Int Int) Int))";
}
@@ -731,8 +742,9 @@ namespace Microsoft.Boogie.SMTLib return "(_ map =>)";
}
else if (name == "MapIte") {
+ Type type = ResultType(node.Type);
StringBuilder sb = new StringBuilder();
- TypeToStringHelper(mapType.Result, sb);
+ TypeToStringHelper(type, sb);
string s = sb.ToString();
return "(_ map (ite (Bool " + s + " " + s + ") " + s + "))";
}
|