From a720bdea97d6646128d1d81b9f5cb61b71d06c79 Mon Sep 17 00:00:00 2001 From: Unknown Date: Tue, 6 Sep 2011 13:56:36 -0700 Subject: check in support for generalized array theory --- Source/Provers/SMTLib/SMTLibLineariser.cs | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs') 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 { -- cgit v1.2.3