From e599209547cabdd5c9663938edec016117e14280 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 24 Sep 2014 12:24:52 +0100 Subject: Remove dead code Patch by Jeroen Ketema --- Source/Model/Model.cs | 14 +- Source/Model/ModelParser.cs | 460 -------------------------------------------- 2 files changed, 1 insertion(+), 473 deletions(-) diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 1f97125a..154297aa 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -697,21 +697,9 @@ namespace Microsoft.Boogie public static List ParseModels(System.IO.TextReader rd, string prover) { - ModelParser p; - - switch (prover) - { - case "SMTLIB2": - p = new ParserSMT(); - break; - default: - p = new ParserZ3(); - break; - } - + ModelParser p = new ParserZ3(); p.rd = rd; p.Run(); - return p.resModels; } } diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index ded145ed..e456cbcd 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -258,464 +258,4 @@ namespace Microsoft.Boogie } } - class ParserSMT : ModelParser - { - string[] tokens; - List output; - int arity; - int arrayNum; - int index; - - void FindArity () - { - arity = 0; - int p_count = 1; - int i = 4; - - while (p_count > 0) { - if (i == tokens.Length - 1) - break; - else if (tokens [i] == ")") - p_count--; - else if (tokens [i] == "(" && tokens [i + 1] != "ite") { - p_count++; - arity++; - } - - i++; - } - } - - string GetValue (int idx) - { - string value = tokens [idx]; - - if (tokens [idx - 1] == "-") { - value = "(- " + value + ")"; - } else if (tokens [idx - 2] == "_") { - value = tokens [idx - 1] + "[" + tokens [idx] + "]"; - } - - return value; - } - - List[] TrySplitExpr (List expr) - { - int splits = 1; - foreach (string tok in expr) - if (tok.Equals ("@SPLIT")) - splits++; - - List[] newExpr = new List[splits]; - - for (int s = 0; s < splits; s++) - newExpr [s] = new List (); - - int i = 0; - foreach (string tok in expr) { - if (tok.Equals ("@SPLIT")) { - i++; - continue; - } - - newExpr [i].Add (tok); - } - - return newExpr; - } - - void SplitArrayExpression () - { - output.Add ("as-array[k!" + arrayNum + "]"); - - if (output.Contains ("@SPLIT")) { - output.Add (" "); - output.Add ("}"); - } - - output.Add ("@SPLIT"); - output.Add ("k!" + arrayNum); - output.Add ("->"); - output.Add ("{"); - output.Add (" "); - - arrayNum++; - } - - void ParseArrayExpr () - { - while (tokens [index] != "as-array" && tokens [index] != "store" && tokens [index] != "__array_store_all__") - index++; - - if (tokens [index] == "store") { - SplitArrayExpression (); - - List args = new List (); - int p_count = 1; - index += 4; - - while (p_count > 0) { - if (tokens [index] == ")") - p_count--; - else if (tokens [index] == "(") - p_count++; - index++; - } - - if ((tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") || - (tokens [index] == "(" && tokens [index + 1] == "store")) { - SplitArrayExpression (); - } else { - while (args.Count < 3) { - if (tokens [index] == ")") - index++; - else if (tokens [index] == "(") { - while (tokens [index] != ")") - index++; - args.Add (GetValue (index - 1)); - } else { - args.Add (GetValue (index)); - } - - index++; - } - - output.Add (args [1]); - output.Add ("->"); - output.Add (args [2]); - output.Add (" "); - output.Add ("else"); - output.Add ("->"); - output.Add (args [0]); - } - } else if (tokens [index] == "__array_store_all__") { - SplitArrayExpression (); - - while (tokens[index] == "__array_store_all__") { - int p_count = 1; - index += 2; - - while (p_count > 0) { - if (tokens [index] == ")") - p_count--; - else if (tokens [index] == "(") - p_count++; - index++; - } - - if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") { - SplitArrayExpression (); - index++; - } else { - if (tokens [index] == ")") - index++; - else if (tokens [index] == "(") { - while (tokens [index] != ")") - index++; - output.Add (GetValue (index - 1)); - } else { - output.Add (GetValue (index)); - } - - index++; - } - } - } else if (tokens [index] == "as-array") { - output.Add ("as-array[" + tokens [index + 1] + "]"); - } - } - - void ParseIteExpr () - { - List args = new List (); - List results = new List (); - - FindArity (); - - for (; ;) { - index++; - - if (tokens [index] == "=") { - while (tokens[index] != ")") - index++; - args.Add (GetValue (index - 1)); - } - - if (args.Count > 0 && args.Count % arity == 0) { - while (tokens[index] == ")") - index++; - - if (tokens [index] == "(") { - while (tokens[index] != ")") - index++; - results.Add (GetValue (index - 1)); - } else { - results.Add (GetValue (index)); - } - - while (index < tokens.Length - 1 && tokens[index + 1] != "=") - index++; - - if (index == tokens.Length - 1) { - while (tokens[index] == ")") - index += -1; - results.Add (GetValue (index)); - break; - } - } - } - - int i = 0; - - for (int j = 0; j < results.Count - 1; j++) { - for (int r = 0; r < arity; r++) { - output.Add (args [i]); - i++; - } - - output.Add ("->"); - output.Add (results [j]); - output.Add (" "); - } - - output.Add ("else"); - output.Add ("->"); - output.Add (results [results.Count - 1]); - } - - void ParseEndOfExpr () - { - index++; - - if (index == tokens.Length && output.Count == 2) { - index += -2; - - if (tokens [index] == ")") { - index += -1; - output.Add (GetValue (index)); - } else { - output.Add (GetValue (index)); - } - } - - if (index == tokens.Length && output.Contains ("{")) { - output.Add (" "); - output.Add ("}"); - } - } - - List GetParsedTokens (string newLine) - { - if (newLine == null) - return null; - newLine = bv.Replace (newLine, "bv${1}"); - string line = newLine; - int openParenCounter = CountOpenParentheses (newLine, 0); - while (openParenCounter > 0) { - newLine = ReadLine (); - if (newLine == null) { - return null; - } - line += newLine; - openParenCounter = CountOpenParentheses (newLine, openParenCounter); - } - - line = line.Replace ("(", " ( "); - line = line.Replace (")", " ) "); - - tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries); - output = new List (); - - index = 0; - bool doneParsing = false; - - while (!doneParsing) { - switch (tokens [index]) { - case ")": - ParseEndOfExpr (); - break; - - case "define-fun": - output.Add (GetValue (index + 1)); - output.Add ("->"); - index += 2; - break; - - case "_ufmt_1": - case "x!1": - output.Add ("{"); - output.Add (" "); - if (Array.IndexOf (tokens, "ite") > -1) - ParseIteExpr (); - else - index++; - break; - - case "Array": - ParseArrayExpr (); - break; - - default: - index++; - break; - } - - if (index == tokens.Length) - doneParsing = true; - } - - return output; - } - - internal override void Run () - { - var selectFunctions = new Dictionary (); - var storeFunctions = new Dictionary (); - arrayNum = 0; - - for (; ;) { - var line = ReadLine (); - if (line == null) - break; // end of model, everything fine - if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") { - NewModel (); - continue; - } - if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:")) - continue; - if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL") - continue; - -// Console.WriteLine("\n\n# :: " + line); - - var words = GetParsedTokens (line); - if (words.Count == 0) - continue; - var exprs = TrySplitExpr (words); - - foreach (List expr in exprs) { -// Console.WriteLine (""); -// for (int i = 0; i < expr.Count; i++) { -// Console.Write (expr [i] + " "); -// } - - var lastToken = expr [expr.Count - 1]; - if (currModel == null) - BadModel ("model begin marker not found"); - - if (expr.Count > 3 && expr [1] == "->") { - var funName = (string)expr [0]; - Model.Func fn = null; - int i = 4; - - if (expr [2] != "{" && expr [6] != "{") - BadModel ("unidentified function definition 5"); - - fn = currModel.TryGetFunc (funName); - - for (; ;) { - if (expr [i] == "}") { - if (i == expr.Count - 1) { - if (fn == null) - fn = currModel.MkFunc (funName, 1); - break; - } else { - i++; - continue; - } - } - - for (; ;) { - if (expr [i] == " ") { - i++; - break; - } - - if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") { - if (fn.Else == null) - fn.Else = GetElt (expr [i]); - i++; - continue; - } - - if (expr [i] == "else") { - if (expr [i + 1] == "->") { - i += 2; - - if (expr [i] == "}") - BadModel ("unidentified function definition 1"); - - if (expr [i] == "{") { - i++; - continue; - } else { - if (fn != null && !(expr [i] == "#unspecified") && fn.Else == null) - fn.Else = GetElt (expr [i]); - i++; - continue; - } - } else - BadModel ("unidentified function definition 2"); - } - - int arity = 0; - for (; ;) { - arity++; - if (expr [arity + i] == " ") { - arity -= 2; - break; - } - } - - if (expr [i + arity] == "->") { - i += arity + 1; - - if (expr [i] == "}") - BadModel ("unidentified function definition 3"); - } else - BadModel ("unidentified function definition 4"); - - if (fn == null) { - if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) { - funName = string.Format ("[{0}]", arity); - - if (!selectFunctions.TryGetValue (arity, out fn)) { - fn = currModel.MkFunc (funName, arity); - selectFunctions.Add (arity, fn); - } - } else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) { - funName = string.Format ("[{0}:=]", arity); - - if (!storeFunctions.TryGetValue (arity, out fn)) { - fn = currModel.MkFunc (funName, arity); - storeFunctions.Add (arity, fn); - } - } else { - fn = currModel.MkFunc (funName, arity); - } - } - - var args = new Model.Element[fn.Arity]; - - for (var idx = 0; idx < fn.Arity; ++idx) - args [idx] = GetElt (expr [idx + i - arity - 1]); - - fn.AddApp (GetElt (expr [i]), args); - - i++; - break; - } - } - } else if (expr.Count == 3 && expr [1] == "->") { - var funName = (string)expr [0]; - Model.Func fn = null; - - fn = currModel.MkFunc (funName, 0); - fn.SetConstant (GetElt (lastToken)); - } else - BadModel ("unidentified line"); - } - } - } - } } -- cgit v1.2.3