summaryrefslogtreecommitdiff
path: root/Source/Model/ModelParser.cs
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-22 14:17:05 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-22 14:17:05 +0100
commitcc6ae16068e2b49a980e337b4e101cf87d37b900 (patch)
tree83c65c1ab38ae615b50c11458123a26a0d8ebae0 /Source/Model/ModelParser.cs
parent9ba2ad319e142834d83a0b48e94ef378c870bcdb (diff)
refactoring
Diffstat (limited to 'Source/Model/ModelParser.cs')
-rw-r--r--Source/Model/ModelParser.cs470
1 files changed, 235 insertions, 235 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index ed9ea2f4..dc6e06b5 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<Model> resModels = new List<Model>();
+ internal List<Model> resModels = new List<Model> ();
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<object> os = (List<object>)o;
- List<Model.Element> args = new List<Model.Element>();
+ List<Model.Element> args = new List<Model.Element> ();
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<object> GetFunctionTokens(string newLine)
+ List<object> 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<object> newTuple = new List<object>();
- Stack<List<object>> wordStack = new Stack<List<object>>();
+ List<object> newTuple = new List<object> ();
+ Stack<List<object>> wordStack = new Stack<List<object>> ();
for (int i = 0; i < tuple.Length; i++) {
- string elem = tuple[i];
+ string elem = tuple [i];
if (elem == "(") {
- List<object> ls = new List<object>();
- wordStack.Push(ls);
+ List<object> ls = new List<object> ();
+ wordStack.Push (ls);
} else if (elem == ")") {
- List<object> ls = wordStack.Pop();
+ List<object> 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<int, Model.Func>();
- var storeFunctions = new Dictionary<int, Model.Func>();
+ var selectFunctions = new Dictionary<int, Model.Func> ();
+ var storeFunctions = new Dictionary<int, Model.Func> ();
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 == "<initial>")
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,171 +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;
}
- List<string>[] TrySplitExpr(List<string> expr)
+ List<string>[] TrySplitExpr (List<string> expr)
{
int splits = 1;
foreach (string tok in expr)
- if (tok.Equals("@SPLIT"))
+ if (tok.Equals ("@SPLIT"))
splits++;
List<string>[] newExpr = new List<string>[splits];
for (int s = 0; s < splits; s++)
- newExpr[s] = new List<string>();
+ newExpr [s] = new List<string> ();
int i = 0;
foreach (string tok in expr) {
- if (tok.Equals("@SPLIT")) {
+ if (tok.Equals ("@SPLIT")) {
i++;
continue;
}
- newExpr[i].Add(tok);
+ newExpr [i].Add (tok);
}
return newExpr;
}
- void SplitArrayExpression()
+ void SplitArrayExpression ()
{
- output.Add("as-array[k!" + arrayNum + "]");
+ output.Add ("as-array[k!" + arrayNum + "]");
- if (output.Contains("@SPLIT")) {
- output.Add(" ");
- output.Add("}");
+ if (output.Contains ("@SPLIT")) {
+ output.Add (" ");
+ output.Add ("}");
}
- output.Add("@SPLIT");
- output.Add("k!" + arrayNum);
- output.Add("->");
- 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<string> args = new List<string>();
+ List<string> args = new List<string> ();
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<string> args = new List<string>();
- List<string> results = new List<string>();
+ List<string> args = new List<string> ();
+ List<string> results = new List<string> ();
- FindArity();
+ FindArity ();
for (; ;) {
index++;
- if (tokens[index] == "=") {
+ if (tokens [index] == "=") {
while (tokens[index] != ")")
index++;
- args.Add(GetValue(index - 1));
+ args.Add (GetValue (index - 1));
}
if (args.Count > 0 && args.Count % arity == 0) {
while (tokens[index] == ")")
index++;
- if (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] != "=")
@@ -457,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;
}
}
@@ -467,90 +467,90 @@ namespace Microsoft.Boogie
for (int j = 0; j < results.Count - 1; j++) {
for (int r = 0; r < arity; r++) {
- output.Add(args[i]);
+ 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("}");
+ if (index == tokens.Length && output.Contains ("{")) {
+ output.Add (" ");
+ output.Add ("}");
}
}
- List<string> GetParsedTokens(string newLine)
+ List<string> 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<string>();
+ tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+ output = new List<string> ();
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 "_ufmt_1":
case "x!1":
- output.Add("{");
- output.Add(" ");
- if (Array.IndexOf(tokens, "ite") > -1)
- ParseIteExpr();
+ output.Add ("{");
+ output.Add (" ");
+ if (Array.IndexOf (tokens, "ite") > -1)
+ ParseIteExpr ();
else
index++;
break;
case "Array":
- ParseArrayExpr();
+ ParseArrayExpr ();
break;
default:
@@ -565,31 +565,31 @@ namespace Microsoft.Boogie
return output;
}
- internal override void Run()
+ internal override void Run ()
{
- var selectFunctions = new Dictionary<int, Model.Func>();
- var storeFunctions = new Dictionary<int, Model.Func>();
+ var selectFunctions = new Dictionary<int, Model.Func> ();
+ var storeFunctions = new Dictionary<int, Model.Func> ();
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);
- var words = GetParsedTokens(line);
+ var words = GetParsedTokens (line);
if (words.Count == 0)
continue;
- var exprs = TrySplitExpr(words);
+ var exprs = TrySplitExpr (words);
foreach (List<string> expr in exprs) {
// Console.WriteLine ("");
@@ -597,25 +597,25 @@ namespace Microsoft.Boogie
// 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++;
@@ -624,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");
}
}
}