From 0f9de25932ded17ef7b1f52e8385274b058d901e Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Wed, 10 Jul 2013 15:59:57 +0100 Subject: the cvc4 parser can now parse nested array expressions --- Source/Model/ModelParser.cs | 928 ++++++++++++++++++++++---------------------- 1 file changed, 471 insertions(+), 457 deletions(-) (limited to 'Source/Model') diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index 9a455662..5de903ab 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -3,7 +3,6 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- - using System; using System.Linq; using System.Collections.Generic; @@ -17,28 +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; @@ -46,34 +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 ret = currModel.TryMkElement(name); + Model.Element GetElt (string 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) { @@ -82,182 +82,175 @@ namespace Microsoft.Boogie else if (c == ')') f--; } - if (f < 0) BadModel("mismatched parentheses in datatype term"); + if (f < 0) + 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("}")) - { - while (openParenCounter > 0) - { - newLine = ReadLine(); - if (newLine == null) - { + int openParenCounter = CountOpenParentheses (newLine, 0); + if (!newLine.Contains ("}")) { + while (openParenCounter > 0) { + 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); - - List newTuple = new List(); - Stack> wordStack = new Stack>(); - for (int i = 0; i < tuple.Length; i++) - { - string elem = tuple[i]; - if (elem == "(") - { - List ls = new List(); - wordStack.Push(ls); - } - else if (elem == ")") - { - List ls = wordStack.Pop(); - if (wordStack.Count > 0) - { - wordStack.Peek().Add(ls); - } - else - { - newTuple.Add(ls); + line = line.Replace ("(", " ( "); + line = line.Replace (")", " ) "); + var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries); + + List newTuple = new List (); + Stack> wordStack = new Stack> (); + for (int i = 0; i < tuple.Length; i++) { + string elem = tuple [i]; + if (elem == "(") { + List ls = new List (); + wordStack.Push (ls); + } else if (elem == ")") { + List ls = wordStack.Pop (); + if (wordStack.Count > 0) { + wordStack.Peek ().Add (ls); + } else { + newTuple.Add (ls); } - } - else if (wordStack.Count > 0) - { - wordStack.Peek().Add(elem); - } - else - { - newTuple.Add(elem); + } else if (wordStack.Count > 0) { + wordStack.Peek ().Add (elem); + } else { + newTuple.Add (elem); } } return newTuple; } - internal override void Run() + internal override void Run () { - var selectFunctions = new Dictionary(); - var storeFunctions = new Dictionary(); - for (; ; ) { - var line = ReadLine(); - if (line == null) break; // end of model, everything fine + var selectFunctions = new Dictionary (); + var storeFunctions = new Dictionary (); + for (; ;) { + 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); - if (words.Count == 0) continue; - var lastWord = words[words.Count - 1]; + var words = GetFunctionTokens (line); + if (words.Count == 0) + continue; + 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); - for (; ; ) { - var tmpline = ReadLine(); - if (tmpline == "*** END_STATE") break; - var tuple = GetFunctionTokens(tmpline); - if (tuple == null) 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])); - } - else - { - BadModel("invalid state tuple definition"); + cs = currModel.MkState (name); + for (; ;) { + var tmpline = ReadLine (); + if (tmpline == "*** END_STATE") + break; + var tuple = GetFunctionTokens (tmpline); + if (tuple == null) + 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])); + } else { + 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); - for ( ; ; ) { - var tuple = GetFunctionTokens(ReadLine()); - if (tuple == null) BadModel("EOF in function table"); - if (tuple.Count == 0) continue; - string tuple0 = tuple[0] as string; + if (lastWord is string && ((string)lastWord) == "{") { + fn = currModel.TryGetFunc (funName); + for (; ;) { + var tuple = GetFunctionTokens (ReadLine ()); + if (tuple == null) + BadModel ("EOF in function table"); + if (tuple.Count == 0) + continue; + string tuple0 = tuple [0] as string; if (tuple.Count == 1) { if (fn == null) - fn = currModel.MkFunc(funName, 1); - if (tuple0 == "}") break; + 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; - if (tuplePenultimate != "->") BadModel("invalid function tuple definition"); - var resultName = tuple[tuple.Count - 1]; + string tuplePenultimate = tuple [tuple.Count - 2] as string; + if (tuplePenultimate != "->") + 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"); } } } @@ -270,23 +263,22 @@ namespace Microsoft.Boogie protected int arity; protected int arrayNum; - abstract protected void ParseArray(ref int i); - abstract protected void ParseITE(ref int i); + abstract protected void ParseArray (ref int i); - protected void FindArity() + abstract protected void ParseITE (ref int i); + + protected void FindArity () { arity = 0; int p_count = 1; int i = 4; - while (p_count > 0) - { + 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++; } @@ -295,108 +287,96 @@ namespace Microsoft.Boogie } } - protected string GetValue(int idx) + protected 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 ParseEndOfExpression(ref int i) + void ParseEndOfExpression (ref int i) { i++; - if (i == tokens.Length && output.Count == 2) - { + if (i == tokens.Length && output.Count == 2) { i += -2; - if (tokens[i] == ")") - { + if (tokens [i] == ")") { i += -1; - output.Add(GetValue(i)); - } - else - { - output.Add(GetValue(i)); + output.Add (GetValue (i)); + } else { + output.Add (GetValue (i)); } } - if (i == tokens.Length && output.Contains("{")) - { - output.Add(" "); - output.Add("}"); + if (i == tokens.Length && output.Contains ("{")) { + output.Add (" "); + output.Add ("}"); } } - 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(); - if (newLine == null) - { + while (openParenCounter > 0) { + 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 (); var i = 0; bool doneParsing = false; - while(!doneParsing) - { - switch (tokens[i]) - { - case ")": - ParseEndOfExpression(ref i); + while (!doneParsing) { + switch (tokens [i]) { + case ")": + ParseEndOfExpression (ref i); break; - case "define-fun": - output.Add(GetValue(i+1)); - output.Add("->"); + case "define-fun": + output.Add (GetValue (i + 1)); + output.Add ("->"); i += 2; break; - case "Array": - ParseArray(ref i); + case "Array": + ParseArray (ref i); break; - case "ite": - ParseITE(ref i); + case "ite": + ParseITE (ref i); break; - case "_ufmt_1": - case "x!1": - output.Add("{"); - output.Add(" "); + case "_ufmt_1": + case "x!1": + output.Add ("{"); + output.Add (" "); i++; break; - default: + default: i++; break; } @@ -408,290 +388,348 @@ namespace Microsoft.Boogie return output; } - internal override void Run() + List[] TrySplitExpr (List expr) { - 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; + int splits = 1; + foreach (string tok in expr) + if (tok.Equals ("@SPLIT")) + splits++; - var words = GetParsedTokens(line); - /* - Console.WriteLine(""); - for (int i = 0; i < words.Count; i++) - { - Console.Write(words[i] + " "); - } -*/ - if (words.Count == 0) continue; - var lastToken = words[words.Count - 1]; - if (currModel == null) - BadModel("model begin marker not found"); + List[] newExpr = new List[splits]; - if (words.Count > 3 && words[1] == "->") - { - var funName = (string) words[0]; - Model.Func fn = null; - int i = 4; + for (int s = 0; s < splits; s++) + newExpr [s] = new List (); - if (words.Contains("@SPLIT")) - { - arrayNum++; + int i = 0; + foreach (string tok in expr) { + if (tok.Equals ("@SPLIT")) { + i++; + continue; + } - fn = currModel.MkFunc(funName, 0); - fn.SetConstant(GetElt(words[2])); + newExpr [i].Add (tok); + } - i = 8; + return newExpr; + } - funName = (string) words[4]; - fn = null; - } + internal override void Run () + { + var selectFunctions = new Dictionary (); + var storeFunctions = new Dictionary (); + arrayNum = 0; - if (words[2] != "{" && words[6] != "{") - BadModel("unidentified function definition 5"); + 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; - fn = currModel.TryGetFunc(funName); + var words = GetParsedTokens (line); + if (words.Count == 0) + continue; + var exprs = TrySplitExpr (words); - for (; ; ) - { - if (words[i] == "}") - { - if (i == words.Count - 1) - { - if (fn == null) - fn = currModel.MkFunc(funName, 1); - break; - } - else - { - i++; - continue; - } - } + foreach (List expr in exprs) { + /*Console.WriteLine (""); + for (int i = 0; i < expr.Count; i++) { + Console.Write (expr [i] + " "); + }*/ - for (; ; ) - { - if (words[i] == " ") - { - i++; - break; - } + var lastToken = expr [expr.Count - 1]; + if (currModel == null) + BadModel ("model begin marker not found"); - if ((i == 4 || i == 8) && words[i - 1] == " " && words[i + 1] == " ") { - if (fn.Else == null) - fn.Else = GetElt(words[i]); - i++; - continue; - } + if (expr.Count > 3 && expr [1] == "->") { + var funName = (string)expr [0]; + Model.Func fn = null; + int i = 4; - if (words[i] == "else") - { - if (words[i + 1] == "->") - { - i += 2; + if (expr [2] != "{" && expr [6] != "{") + BadModel ("unidentified function definition 5"); - if (words[i] == "}") - BadModel("unidentified function definition 1"); + fn = currModel.TryGetFunc (funName); - if (words[i] == "{") - { - i++; - continue; - } - else - { - if (fn != null && !(words[i] == "#unspecified") && fn.Else == null) - fn.Else = GetElt(words[i]); - i++; - continue; - } + for (; ;) { + if (expr [i] == "}") { + if (i == expr.Count - 1) { + if (fn == null) + fn = currModel.MkFunc (funName, 1); + break; + } else { + i++; + continue; } - else - BadModel("unidentified function definition 2"); } - int arity = 0; - for (; ; ) - { - arity++; - if (words[arity + i] == " ") - { - arity -= 2; + for (; ;) { + if (expr [i] == " ") { + i++; break; } - } - if (words[i + arity] == "->") - { - i += arity + 1; + if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") { + if (fn.Else == null) + fn.Else = GetElt (expr [i]); + i++; + continue; + } - if (words[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); - } + 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"); } - 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); + int arity = 0; + for (; ;) { + arity++; + if (expr [arity + i] == " ") { + arity -= 2; + break; } } - else - { - fn = currModel.MkFunc(funName, arity); + + 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]; + var args = new Model.Element[fn.Arity]; - for (var idx = 0; idx < fn.Arity; ++idx) - args[idx] = GetElt(words[idx + i - arity - 1]); + for (var idx = 0; idx < fn.Arity; ++idx) + args [idx] = GetElt (expr [idx + i - arity - 1]); - fn.AddApp(GetElt(words[i]), args); + fn.AddApp (GetElt (expr [i]), args); - i++; - break; + 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"); } - else if (words.Count == 3 && words[1] == "->") - { - var funName = (string) words[0]; - Model.Func fn = null; - - fn = currModel.MkFunc(funName, 0); - fn.SetConstant(GetElt(lastToken)); - } - else - BadModel("unidentified line"); } } } internal class ParserZ3_SMTLIB2 : ParserSMT { - protected override void ParseArray(ref int i) + protected override void ParseArray (ref int i) { while (tokens[i] != "as-array") i++; - output.Add("as-array[" + tokens[i + 1] + "]"); + output.Add ("as-array[" + tokens [i + 1] + "]"); } - protected override void ParseITE(ref int i) + protected override void ParseITE (ref int i) { - List args = new List(); - List results = new List(); + List args = new List (); + List results = new List (); - FindArity(); + FindArity (); - for (; ; ) - { + for (; ;) { i++; - if (tokens[i] == "=") - { - if (tokens[i + 2] == "(" && tokens[i + 3] == "_") - { - args.Add(GetValue(i + 5)); + if (tokens [i] == "=") { + if (tokens [i + 2] == "(" && tokens [i + 3] == "_") { + args.Add (GetValue (i + 5)); i += 6; - } - else if (tokens[i + 2] == "(" && tokens[i + 3] == "-") - { - args.Add(GetValue(i + 4)); + } else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") { + args.Add (GetValue (i + 4)); i += 5; - } - else - { - args.Add(GetValue(i + 2)); + } else { + args.Add (GetValue (i + 2)); i += 3; } } - if (args.Count > 0 && args.Count % arity == 0) - { - if (tokens[i + 2] == "(" && tokens[i + 3] == "_") - { - results.Add(GetValue(i + 5)); + if (args.Count > 0 && args.Count % arity == 0) { + if (tokens [i + 2] == "(" && tokens [i + 3] == "_") { + results.Add (GetValue (i + 5)); i += 6; - } - else if (tokens[i + 2] == "(" && tokens[i + 3] == "-") - { - results.Add(GetValue(i + 4)); + } else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") { + results.Add (GetValue (i + 4)); i += 5; - } - else - { - results.Add(GetValue(i + 2)); + } else { + results.Add (GetValue (i + 2)); i += 3; } - while (i < tokens.Length - 1 && tokens[i + 1] != "=") - { + while (i < tokens.Length - 1 && tokens[i + 1] != "=") { i++; } - if (i == tokens.Length - 1) - { + if (i == tokens.Length - 1) { while (tokens[i] == ")") i += -1; - results.Add(GetValue(i)); + results.Add (GetValue (i)); break; } } } int idx = 0; - for (int j = 0; j < results.Count - 1; j++) - { - for (int r = 0; r < arity; r++) - { - output.Add(args[idx]); + for (int j = 0; j < results.Count - 1; j++) { + for (int r = 0; r < arity; r++) { + output.Add (args [idx]); idx++; } - 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]); } } internal class ParserCVC4 : ParserSMT { + void SplitArrayExpression () + { + if (output.Contains ("@SPLIT")) { + output.Add (" "); + output.Add ("}"); + } + + output.Add ("@SPLIT"); + output.Add ("k!" + arrayNum); + output.Add ("->"); + output.Add ("{"); + output.Add (" "); + + arrayNum++; + } + + protected override void ParseArray (ref int i) + { + output.Add ("as-array[k!" + arrayNum + "]"); + SplitArrayExpression (); + + while (tokens[i] != "store" && tokens[i] != "__array_store_all__") + i++; + + if (tokens [i] == "store") { + List args = new List (); + int p_count = 1; + i += 4; + + while (p_count > 0) { + if (tokens [i] == ")") + p_count--; + else if (tokens [i] == "(") + p_count++; + i++; + } + + if (tokens [i] == "(" && tokens [i + 1] == "__array_store_all__") { + output.Add ("as-array[k!" + arrayNum + "]"); + SplitArrayExpression (); + } else { + while (args.Count < 3) { + if (tokens [i] == ")") + i++; + else if (tokens [i] == "(" && tokens [i + 1] == "_") { + args.Add (GetValue (i + 3)); + i += 5; + } else if (tokens [i + 1] == "(" && tokens [i + 1] == "-") { + args.Add (GetValue (i + 2)); + i += 4; + } else { + args.Add (GetValue (i)); + i++; + } + } + + output.Add (args [1]); + output.Add ("->"); + output.Add (args [2]); + output.Add (" "); + output.Add ("else"); + output.Add ("->"); + output.Add (args [0]); + } + } else if (tokens [i] == "__array_store_all__") { + int p_count = 1; + i += 2; + + while (p_count > 0) { + if (tokens [i] == ")") + p_count--; + else if (tokens [i] == "(") + p_count++; + i++; + } + + if (tokens [i] == "(" && tokens [i + 1] == "_") { + output.Add (GetValue (i + 3)); + i += 5; + } else if (tokens [i] == "(" && tokens [i + 1] == "-") { + output.Add (GetValue (i + 2)); + i += 4; + } else { + output.Add (GetValue (i)); + i++; + } + } + } + /* protected override void ParseArray(ref int i) { output.Add("as-array[k!" + arrayNum + "]"); @@ -779,73 +817,58 @@ namespace Microsoft.Boogie } } } - - protected override void ParseITE(ref int i) + */ + protected override void ParseITE (ref int i) { - List args = new List(); - List results = new List(); + List args = new List (); + List results = new List (); - FindArity(); + FindArity (); int occurrences = 0; - foreach (string tok in tokens) - { - if (tok == "_ufmt_1") occurrences++; + foreach (string tok in tokens) { + if (tok == "_ufmt_1") + occurrences++; } - for (; ; ) - { + for (; ;) { i++; - if (tokens[i] == "=") - { - if (tokens[i + 2] == "(" && tokens[i + 3] == "_") - { - args.Add(GetValue(i + 5)); + if (tokens [i] == "=") { + if (tokens [i + 2] == "(" && tokens [i + 3] == "_") { + args.Add (GetValue (i + 5)); i += 6; - } - else if (tokens[i + 2] == "(" && tokens[i + 3] == "-") - { - args.Add(GetValue(i + 4)); + } else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") { + args.Add (GetValue (i + 4)); i += 5; - } - else - { - args.Add(GetValue(i + 2)); + } else { + args.Add (GetValue (i + 2)); i += 2; } } if ((args.Count > 0 && args.Count % arity == 0) || - (results.Count > 0 && occurrences <= 2)) - { - if (tokens[i + 2] == "(" && tokens[i + 3] == "_") - { - results.Add(GetValue(i + 5)); + (results.Count > 0 && occurrences <= 2)) { + if (tokens [i + 2] == "(" && tokens [i + 3] == "_") { + results.Add (GetValue (i + 5)); i += 6; - } - else if (tokens[i + 2] == "(" && tokens[i + 3] == "-") - { - results.Add(GetValue(i + 4)); + } else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") { + results.Add (GetValue (i + 4)); i += 5; - } - else - { - results.Add(GetValue(i + 2)); + } else { + results.Add (GetValue (i + 2)); i += 2; } - while (i < tokens.Length - 1 && tokens[i + 1] != "=") - { + while (i < tokens.Length - 1 && tokens[i + 1] != "=") { i++; } - if (i == tokens.Length - 1) - { + if (i == tokens.Length - 1) { while (tokens[i] == ")") i += -1; - results.Add(GetValue(i)); + results.Add (GetValue (i)); break; } } @@ -853,43 +876,34 @@ namespace Microsoft.Boogie int idx = 0; - for (int j = 0; j < results.Count - 1; j++) - { - if (occurrences > 2) - { - for (int r = 0; r < arity; r++) - { - output.Add(args[idx]); + for (int j = 0; j < results.Count - 1; j++) { + if (occurrences > 2) { + for (int r = 0; r < arity; r++) { + output.Add (args [idx]); idx++; } - } - else - { - if (arity == 1) - { - output.Add(args[idx]); + } else { + if (arity == 1) { + output.Add (args [idx]); idx++; - } - else - { - output.Add(args[0]); + } else { + output.Add (args [0]); - for (int r = 1; r < arity; r++) - { + for (int r = 1; r < arity; r++) { idx++; - output.Add(args[idx]); + output.Add (args [idx]); } } } - 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]); } } } -- cgit v1.2.3