summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@GHALIB.redmond.corp.microsoft.com>2011-09-06 13:56:36 -0700
committerGravatar Unknown <qadeer@GHALIB.redmond.corp.microsoft.com>2011-09-06 13:56:36 -0700
commita720bdea97d6646128d1d81b9f5cb61b71d06c79 (patch)
treec58788ca0f62dcd2c853d01760c2a14fea501908 /Source
parentde7fd8ce810d4d27168584e4e7270058cc8f9554 (diff)
check in support for generalized array theory
Diffstat (limited to 'Source')
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs15
1 files changed, 5 insertions, 10 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 2cda9d6a..36df38e3 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -667,7 +667,7 @@ 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);
@@ -686,10 +686,9 @@ namespace Microsoft.Boogie.SMTLib
private static string CheckMapApply(string name, VCExprNAry node) {
if (name == "MapConst") {
- StringBuilder sb = new StringBuilder();
Type type = node.Type;
- TypeToStringHelper(type, sb);
- return "(as const " + sb.ToString() + ")";
+ string s = TypeToString(type);
+ return "(as const " + s + ")";
}
else if (name == "MapAdd") {
return "(_ map (+ (Int Int) Int))";
@@ -708,9 +707,7 @@ namespace Microsoft.Boogie.SMTLib
}
else if (name == "MapEq") {
Type type = ResultType(node[0].Type);
- StringBuilder sb = new StringBuilder();
- TypeToStringHelper(type, sb);
- string s = sb.ToString();
+ string s = TypeToString(type);
return "(_ map (= (" + s + " " + s + ") Bool))";
}
else if (name == "MapIff") {
@@ -742,9 +739,7 @@ namespace Microsoft.Boogie.SMTLib
}
else if (name == "MapIte") {
Type type = ResultType(node.Type);
- StringBuilder sb = new StringBuilder();
- TypeToStringHelper(type, sb);
- string s = sb.ToString();
+ string s = TypeToString(type);
return "(_ map (ite (Bool " + s + " " + s + ") " + s + "))";
}
else {