From 2c4fff7b78774a98525e475e8a4e078ecf94583d Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Fri, 19 Jul 2013 11:03:54 +0100 Subject: refactoring and fixes in the SMTLIB2 parser --- Source/Model/ModelParser.cs | 582 +++++++++++++++++++++----------------------- 1 file changed, 273 insertions(+), 309 deletions(-) (limited to 'Source/Model') diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index 40fd3c9a..ed9ea2f4 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -16,27 +16,27 @@ namespace Microsoft.Boogie { protected Model currModel; int lineNo; - internal List resModels = new List (); + internal List resModels = new List(); internal System.IO.TextReader rd; string lastLine = ""; protected static char[] seps = new char[] { ' ' }; - protected static Regex bv = new Regex (@"\(_ BitVec (\d+)\)"); + protected static Regex bv = new Regex(@"\(_ BitVec (\d+)\)"); - protected void NewModel () + protected void NewModel() { lastLine = ""; - currModel = new Model (); - resModels.Add (currModel); + currModel = new Model(); + resModels.Add(currModel); } - protected void BadModel (string msg) + protected void BadModel(string msg) { - throw new ArgumentException (string.Format ("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine)); + throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine)); } - protected string ReadLine () + protected string ReadLine() { - var l = rd.ReadLine (); + var l = rd.ReadLine(); if (l != null) { lineNo++; lastLine = l; @@ -44,36 +44,36 @@ namespace Microsoft.Boogie return l; } - string[] GetWords (string line) + string[] GetWords(string line) { if (line == null) return null; - var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries); + var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries); return words; } - Model.Element GetElt (string name) + Model.Element GetElt(string name) { - Model.Element ret = currModel.TryMkElement (name); + Model.Element ret = currModel.TryMkElement(name); if (ret == null) - BadModel ("invalid element name " + name); + BadModel("invalid element name " + name); return ret; } - protected Model.Element GetElt (object o) + protected Model.Element GetElt(object o) { string s = o as string; if (s != null) - return GetElt (s); + return GetElt(s); List os = (List)o; - List args = new List (); + List args = new List(); for (int i = 1; i < os.Count; i++) { - args.Add (GetElt (os [i])); + args.Add(GetElt(os[i])); } - return new Model.DatatypeValue (currModel, (string)os [0], args); + return new Model.DatatypeValue(currModel, (string)os[0], args); } - protected int CountOpenParentheses (string s, int n) + protected int CountOpenParentheses(string s, int n) { int f = n; foreach (char c in s) { @@ -83,174 +83,174 @@ namespace Microsoft.Boogie f--; } if (f < 0) - BadModel ("mismatched parentheses in datatype term"); + BadModel("mismatched parentheses in datatype term"); return f; } - abstract internal void Run (); + abstract internal void Run(); } class ParserZ3 : ModelParser { - List GetFunctionTokens (string newLine) + List GetFunctionTokens(string newLine) { if (newLine == null) return null; - newLine = bv.Replace (newLine, "bv${1}"); + newLine = bv.Replace(newLine, "bv${1}"); string line = newLine; - int openParenCounter = CountOpenParentheses (newLine, 0); - if (!newLine.Contains ("}")) { + int openParenCounter = CountOpenParentheses(newLine, 0); + if (!newLine.Contains("}")) { while (openParenCounter > 0) { - newLine = ReadLine (); + newLine = ReadLine(); if (newLine == null) { return null; } line += newLine; - openParenCounter = CountOpenParentheses (newLine, openParenCounter); + openParenCounter = CountOpenParentheses(newLine, openParenCounter); } } - line = line.Replace ("(", " ( "); - line = line.Replace (")", " ) "); - var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries); + line = line.Replace("(", " ( "); + line = line.Replace(")", " ) "); + var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries); - List newTuple = new List (); - Stack> wordStack = new Stack> (); + List newTuple = new List(); + Stack> wordStack = new Stack>(); for (int i = 0; i < tuple.Length; i++) { - string elem = tuple [i]; + string elem = tuple[i]; if (elem == "(") { - List ls = new List (); - wordStack.Push (ls); + List ls = new List(); + wordStack.Push(ls); } else if (elem == ")") { - List ls = wordStack.Pop (); + List ls = wordStack.Pop(); if (wordStack.Count > 0) { - wordStack.Peek ().Add (ls); + wordStack.Peek().Add(ls); } else { - newTuple.Add (ls); + newTuple.Add(ls); } } else if (wordStack.Count > 0) { - wordStack.Peek ().Add (elem); + wordStack.Peek().Add(elem); } else { - newTuple.Add (elem); + newTuple.Add(elem); } } return newTuple; } - internal override void Run () + internal override void Run() { - var selectFunctions = new Dictionary (); - var storeFunctions = new Dictionary (); + var selectFunctions = new Dictionary(); + var storeFunctions = new Dictionary(); for (; ;) { - var line = ReadLine (); + var line = ReadLine(); if (line == null) break; // end of model, everything fine if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") { - NewModel (); + NewModel(); continue; } - if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:")) + if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.") || line.StartsWith("labels:")) continue; if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL") continue; - var words = GetFunctionTokens (line); + var words = GetFunctionTokens(line); if (words.Count == 0) continue; - var lastWord = words [words.Count - 1]; + var lastWord = words[words.Count - 1]; if (currModel == null) - BadModel ("model begin marker not found"); + BadModel("model begin marker not found"); - if (line.StartsWith ("*** STATE ")) { - var name = line.Substring (10); + if (line.StartsWith("*** STATE ")) { + var name = line.Substring(10); Model.CapturedState cs; if (name == "") cs = currModel.InitialState; else - cs = currModel.MkState (name); + cs = currModel.MkState(name); for (; ;) { - var tmpline = ReadLine (); + var tmpline = ReadLine(); if (tmpline == "*** END_STATE") break; - var tuple = GetFunctionTokens (tmpline); + var tuple = GetFunctionTokens(tmpline); if (tuple == null) - BadModel ("EOF in state table"); + BadModel("EOF in state table"); if (tuple.Count == 0) continue; - if (tuple.Count == 3 && tuple [0] is string && tuple [1] is string && ((string)tuple [1]) == "->") { - cs.AddBinding ((string)tuple [0], GetElt (tuple [2])); + if (tuple.Count == 3 && tuple[0] is string && tuple[1] is string && ((string)tuple[1]) == "->") { + cs.AddBinding((string)tuple[0], GetElt(tuple[2])); } else { - BadModel ("invalid state tuple definition"); + BadModel("invalid state tuple definition"); } } continue; } - if (words.Count == 3 && words [1] is string && ((string)words [1]) == "->") { - var funName = (string)words [0]; + if (words.Count == 3 && words[1] is string && ((string)words[1]) == "->") { + var funName = (string)words[0]; Model.Func fn = null; if (lastWord is string && ((string)lastWord) == "{") { - fn = currModel.TryGetFunc (funName); + fn = currModel.TryGetFunc(funName); for (; ;) { - var tuple = GetFunctionTokens (ReadLine ()); + var tuple = GetFunctionTokens(ReadLine()); if (tuple == null) - BadModel ("EOF in function table"); + BadModel("EOF in function table"); if (tuple.Count == 0) continue; - string tuple0 = tuple [0] as string; + string tuple0 = tuple[0] as string; if (tuple.Count == 1) { if (fn == null) - fn = currModel.MkFunc (funName, 1); + fn = currModel.MkFunc(funName, 1); if (tuple0 == "}") break; if (fn.Else == null) - fn.Else = GetElt (tuple [0]); + fn.Else = GetElt(tuple[0]); continue; } - string tuplePenultimate = tuple [tuple.Count - 2] as string; + string tuplePenultimate = tuple[tuple.Count - 2] as string; if (tuplePenultimate != "->") - BadModel ("invalid function tuple definition"); - var resultName = tuple [tuple.Count - 1]; + BadModel("invalid function tuple definition"); + var resultName = tuple[tuple.Count - 1]; if (tuple0 == "else") { if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) { - fn.Else = GetElt (resultName); + fn.Else = GetElt(resultName); } continue; } if (fn == null) { var arity = tuple.Count - 2; - 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); + 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 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); + fn = currModel.MkFunc(funName, arity); } } var args = new Model.Element[fn.Arity]; for (int i = 0; i < fn.Arity; ++i) - args [i] = GetElt (tuple [i]); - fn.AddApp (GetElt (resultName), args); + args[i] = GetElt(tuple[i]); + fn.AddApp(GetElt(resultName), args); } } else { - fn = currModel.MkFunc (funName, 0); - fn.SetConstant (GetElt (lastWord)); + fn = currModel.MkFunc(funName, 0); + fn.SetConstant(GetElt(lastWord)); } } else { - BadModel ("unidentified line"); + BadModel("unidentified line"); } } } @@ -264,7 +264,7 @@ namespace Microsoft.Boogie int arrayNum; int index; - void FindArity () + void FindArity() { arity = 0; int p_count = 1; @@ -273,9 +273,9 @@ namespace Microsoft.Boogie while (p_count > 0) { if (i == tokens.Length - 1) break; - else if (tokens [i] == ")") + else if (tokens[i] == ")") p_count--; - else if (tokens [i] == "(" && tokens [i + 1] != "ite") { + else if (tokens[i] == "(" && tokens[i + 1] != "ite") { p_count++; arity++; } @@ -284,159 +284,171 @@ namespace Microsoft.Boogie } } - string GetValue (int idx) + string GetValue(int idx) { - string value = tokens [idx]; + string value = tokens[idx]; - if (tokens [idx - 1] == "-") { + if (tokens[idx - 1] == "-") { value = "(- " + value + ")"; - } else if (tokens [idx - 2] == "_") { - value = tokens [idx - 1] + "[" + tokens [idx] + "]"; + } else if (tokens[idx - 2] == "_") { + value = tokens[idx - 1] + "[" + tokens[idx] + "]"; } return value; } - void SplitArrayExpression () + List[] TrySplitExpr(List expr) { - output.Add ("as-array[k!" + arrayNum + "]"); + int splits = 1; + foreach (string tok in expr) + if (tok.Equals("@SPLIT")) + splits++; + + List[] newExpr = new List[splits]; - if (output.Contains ("@SPLIT")) { - output.Add (" "); - output.Add ("}"); + 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); } - output.Add ("@SPLIT"); - output.Add ("k!" + arrayNum); - output.Add ("->"); - output.Add ("{"); - output.Add (" "); + 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 () + void ParseArrayExpr() { while (tokens [index] != "as-array" && tokens [index] != "store" && tokens [index] != "__array_store_all__") index++; - if (tokens [index] == "store") { - SplitArrayExpression (); + if (tokens[index] == "store") { + SplitArrayExpression(); - List args = new List (); + List args = new List(); int p_count = 1; index += 4; while (p_count > 0) { - if (tokens [index] == ")") + if (tokens[index] == ")") p_count--; - else if (tokens [index] == "(") + else if (tokens[index] == "(") p_count++; index++; } - if ((tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") || - (tokens [index] == "(" && tokens [index + 1] == "store")) { - SplitArrayExpression (); + if ((tokens[index] == "(" && tokens[index + 1] == "__array_store_all__") || + (tokens[index] == "(" && tokens[index + 1] == "store")) { + SplitArrayExpression(); } else { while (args.Count < 3) { - if (tokens [index] == ")") + if (tokens[index] == ")") index++; - else if (tokens [index] == "(") { + else if (tokens[index] == "(") { while (tokens [index] != ")") index++; - args.Add (GetValue (index - 1)); + args.Add(GetValue(index - 1)); } else { - args.Add (GetValue (index)); + 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]); + 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 (); + } 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] == ")") + if (tokens[index] == ")") p_count--; - else if (tokens [index] == "(") + else if (tokens[index] == "(") p_count++; index++; } - if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") { - SplitArrayExpression (); + if (tokens[index] == "(" && tokens[index + 1] == "__array_store_all__") { + SplitArrayExpression(); index++; } else { - if (tokens [index] == ")") + if (tokens[index] == ")") index++; - else if (tokens [index] == "(") { + else if (tokens[index] == "(") { while (tokens [index] != ")") index++; - output.Add (GetValue (index - 1)); + output.Add(GetValue(index - 1)); } else { - output.Add (GetValue (index)); + output.Add(GetValue(index)); } index++; } } - } else if (tokens [index] == "as-array") { - output.Add ("as-array[" + tokens [index + 1] + "]"); + } else if (tokens[index] == "as-array") { + output.Add("as-array[" + tokens[index + 1] + "]"); } } - void ParseIteExpr () + void ParseIteExpr() { - List args = new List (); - List results = new List (); - - FindArity (); + List args = new List(); + List results = new List(); - int occurrences = 0; - - foreach (string tok in tokens) { - if (tok == "_ufmt_1") - occurrences++; - } + FindArity(); for (; ;) { index++; - if (tokens [index] == "=") { - index += 2; - - if (tokens [index] == "(") { - while (tokens [index] != ")") - index++; - args.Add (GetValue (index - 1)); - } else { - args.Add (GetValue (index)); - } + if (tokens[index] == "=") { + while (tokens[index] != ")") + index++; + args.Add(GetValue(index - 1)); } - if ((args.Count > 0 && args.Count % arity == 0) || - (results.Count > 0 && occurrences <= 2 && occurrences > 0)) { - index += 2; + if (args.Count > 0 && args.Count % arity == 0) { + while (tokens[index] == ")") + index++; - if (tokens [index] == "(") { - while (tokens [index] != ")") + if (tokens[index] == "(") { + while (tokens[index] != ")") index++; - results.Add (GetValue (index - 1)); + results.Add(GetValue(index - 1)); } else { - results.Add (GetValue (index)); + results.Add(GetValue(index)); } while (index < tokens.Length - 1 && tokens[index + 1] != "=") @@ -445,7 +457,7 @@ namespace Microsoft.Boogie if (index == tokens.Length - 1) { while (tokens[index] == ")") index += -1; - results.Add (GetValue (index)); + results.Add(GetValue(index)); break; } } @@ -454,139 +466,91 @@ namespace Microsoft.Boogie int i = 0; for (int j = 0; j < results.Count - 1; j++) { - if (occurrences > 2) { - for (int r = 0; r < arity; r++) { - output.Add (args [i]); - i++; - } - } else if (occurrences > 0) { - if (arity == 1) { - output.Add (args [i]); - i++; - } else { - output.Add (args [0]); - - for (int r = 1; r < arity; r++) { - i++; - output.Add (args [i]); - } - } - } else { - for (int r = 0; r < arity; r++) { - output.Add (args [i]); - i++; - } + for (int r = 0; r < arity; r++) { + output.Add(args[i]); + i++; } - output.Add ("->"); - output.Add (results [j]); - output.Add (" "); + output.Add("->"); + output.Add(results[j]); + output.Add(" "); } - output.Add ("else"); - output.Add ("->"); - output.Add (results [results.Count - 1]); + output.Add("else"); + output.Add("->"); + output.Add(results[results.Count - 1]); } - void ParseEndOfExpr () + void ParseEndOfExpr() { index++; if (index == tokens.Length && output.Count == 2) { index += -2; - if (tokens [index] == ")") { + if (tokens[index] == ")") { index += -1; - output.Add (GetValue (index)); + output.Add(GetValue(index)); } else { - output.Add (GetValue (index)); + output.Add(GetValue(index)); } } - if (index == tokens.Length && output.Contains ("{")) { - output.Add (" "); - output.Add ("}"); - } - } - - 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); + if (index == tokens.Length && output.Contains("{")) { + output.Add(" "); + output.Add("}"); } - - return newExpr; } - List GetParsedTokens (string newLine) + List GetParsedTokens(string newLine) { if (newLine == null) return null; - - newLine = bv.Replace (newLine, "bv${1}"); - + newLine = bv.Replace(newLine, "bv${1}"); string line = newLine; - int openParenCounter = CountOpenParentheses (newLine, 0); - + int openParenCounter = CountOpenParentheses(newLine, 0); while (openParenCounter > 0) { - newLine = ReadLine (); + newLine = ReadLine(); if (newLine == null) { return null; } line += newLine; - openParenCounter = CountOpenParentheses (newLine, openParenCounter); + openParenCounter = CountOpenParentheses(newLine, openParenCounter); } - line = line.Replace ("(", " ( "); - line = line.Replace (")", " ) "); + line = line.Replace("(", " ( "); + line = line.Replace(")", " ) "); - tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries); - output = new List (); + tokens = line.Split(seps, StringSplitOptions.RemoveEmptyEntries); + output = new List(); index = 0; bool doneParsing = false; while (!doneParsing) { - switch (tokens [index]) { + switch (tokens[index]) { case ")": - ParseEndOfExpr (); + ParseEndOfExpr(); break; case "define-fun": - output.Add (GetValue (index + 1)); - output.Add ("->"); + output.Add(GetValue(index + 1)); + output.Add("->"); index += 2; break; - case "Array": - ParseArrayExpr (); - break; - - case "ite": - ParseIteExpr (); - break; - case "_ufmt_1": case "x!1": - output.Add ("{"); - output.Add (" "); - index++; + output.Add("{"); + output.Add(" "); + if (Array.IndexOf(tokens, "ite") > -1) + ParseIteExpr(); + else + index++; + break; + + case "Array": + ParseArrayExpr(); break; default: @@ -601,57 +565,57 @@ namespace Microsoft.Boogie return output; } - internal override void Run () + internal override void Run() { - var selectFunctions = new Dictionary (); - var storeFunctions = new Dictionary (); + var selectFunctions = new Dictionary(); + var storeFunctions = new Dictionary(); arrayNum = 0; for (; ;) { - var line = ReadLine (); + var line = ReadLine(); if (line == null) break; // end of model, everything fine if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") { - NewModel (); + NewModel(); continue; } - if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:")) + 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); +// Console.WriteLine("\n\n# :: " + line); - var words = GetParsedTokens (line); + var words = GetParsedTokens(line); if (words.Count == 0) continue; - var exprs = TrySplitExpr (words); + var exprs = TrySplitExpr(words); foreach (List expr in exprs) { - /*Console.WriteLine (""); - for (int i = 0; i < expr.Count; i++) { - Console.Write (expr [i] + " "); - }*/ +// Console.WriteLine (""); +// for (int i = 0; i < expr.Count; i++) { +// Console.Write (expr [i] + " "); +// } - var lastToken = expr [expr.Count - 1]; + var lastToken = expr[expr.Count - 1]; if (currModel == null) - BadModel ("model begin marker not found"); + BadModel("model begin marker not found"); - if (expr.Count > 3 && expr [1] == "->") { - var funName = (string)expr [0]; + 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"); + if (expr[2] != "{" && expr[6] != "{") + BadModel("unidentified function definition 5"); - fn = currModel.TryGetFunc (funName); + fn = currModel.TryGetFunc(funName); for (; ;) { - if (expr [i] == "}") { + if (expr[i] == "}") { if (i == expr.Count - 1) { if (fn == null) - fn = currModel.MkFunc (funName, 1); + fn = currModel.MkFunc(funName, 1); break; } else { i++; @@ -660,94 +624,94 @@ namespace Microsoft.Boogie } for (; ;) { - if (expr [i] == " ") { + if (expr[i] == " ") { i++; break; } - if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") { + if ((i == 4 || i == 8) && expr[i - 1] == " " && expr[i + 1] == " ") { if (fn.Else == null) - fn.Else = GetElt (expr [i]); + fn.Else = GetElt(expr[i]); i++; continue; } - if (expr [i] == "else") { - if (expr [i + 1] == "->") { + if (expr[i] == "else") { + if (expr[i + 1] == "->") { i += 2; - if (expr [i] == "}") - BadModel ("unidentified function definition 1"); + if (expr[i] == "}") + BadModel("unidentified function definition 1"); - if (expr [i] == "{") { + if (expr[i] == "{") { i++; continue; } else { - if (fn != null && !(expr [i] == "#unspecified") && fn.Else == null) - fn.Else = GetElt (expr [i]); + if (fn != null && !(expr[i] == "#unspecified") && fn.Else == null) + fn.Else = GetElt(expr[i]); i++; continue; } } else - BadModel ("unidentified function definition 2"); + BadModel("unidentified function definition 2"); } int arity = 0; for (; ;) { arity++; - if (expr [arity + i] == " ") { + if (expr[arity + i] == " ") { arity -= 2; break; } } - if (expr [i + arity] == "->") { + if (expr[i + arity] == "->") { i += arity + 1; - if (expr [i] == "}") - BadModel ("unidentified function definition 3"); + if (expr[i] == "}") + BadModel("unidentified function definition 3"); } else - BadModel ("unidentified function definition 4"); + BadModel("unidentified function definition 4"); if (fn == null) { - if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) { - funName = string.Format ("[{0}]", arity); + 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); + 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); + } 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); + if (!storeFunctions.TryGetValue(arity, out fn)) { + fn = currModel.MkFunc(funName, arity); + storeFunctions.Add(arity, fn); } } else { - fn = currModel.MkFunc (funName, arity); + 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]); + args[idx] = GetElt(expr[idx + i - arity - 1]); - fn.AddApp (GetElt (expr [i]), args); + fn.AddApp(GetElt(expr[i]), args); i++; break; } } - } else if (expr.Count == 3 && expr [1] == "->") { - var funName = (string)expr [0]; + } 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)); + fn = currModel.MkFunc(funName, 0); + fn.SetConstant(GetElt(lastToken)); } else - BadModel ("unidentified line"); + BadModel("unidentified line"); } } } -- cgit v1.2.3