diff options
author | pantazis <pdeligia@me.com> | 2013-06-12 16:36:07 +0100 |
---|---|---|
committer | pantazis <pdeligia@me.com> | 2013-06-12 16:36:07 +0100 |
commit | b8b543484eba84d3aaf437333656017ad474b372 (patch) | |
tree | 5f306492595ab81384357d55c7df6286f2ab5bfe /Source/Model/ModelParser.cs | |
parent | 5370dfcf4f83048dc2b8ef8290677b6fa9fb0408 (diff) |
simplified SMTLIB2 parser by merging some parsing methods for the CVC4 and Z3 sub-parsers
Diffstat (limited to 'Source/Model/ModelParser.cs')
-rw-r--r-- | Source/Model/ModelParser.cs | 609 |
1 files changed, 203 insertions, 406 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index 723ccce5..49e403ff 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -281,6 +281,7 @@ namespace Microsoft.Boogie { protected string[] tokens; protected List<string> output; + protected int arrayNum; protected string GetValue(int idx) { @@ -298,28 +299,11 @@ namespace Microsoft.Boogie return value; } - abstract protected void ParseLeftParenthesis(ref int i); abstract protected void ParseITE(ref int i); abstract protected void ParseArray(ref int i); + abstract protected void ParseTokens(); - protected void ParseBitVector(ref int i) - { - i++; - - if (tokens[i] == "BitVec") - { - output.Add("->"); - i += 3; - } - - if (tokens[i].Contains("bv")) - { - output.Add(GetValue(i + 1)); - i += 2; - } - } - - void ParseDefineFun(ref int i) + protected void ParseDefineFun(ref int i) { i++; @@ -329,7 +313,7 @@ namespace Microsoft.Boogie i++; } - void ParseRightParenthesis(ref int i) + protected void ParseRightParenthesis(ref int i) { i++; @@ -355,42 +339,7 @@ namespace Microsoft.Boogie } } - void ParseTokens() - { - var i = 0; - bool doneParsing = false; - - while(!doneParsing) - { - switch (tokens[i]) - { - case ")": - ParseRightParenthesis(ref i); - break; - - case "(": - ParseLeftParenthesis(ref i); - break; - - case "declare-sort": - doneParsing = true; - break; - - case "define-fun": - ParseDefineFun(ref i); - break; - - default: - i++; - break; - } - - if (i == tokens.Length) - doneParsing = true; - } - } - - protected List<string> GetParsedTokens(string newLine) + List<string> GetParsedTokens(string newLine) { if (newLine == null) return null; @@ -420,155 +369,12 @@ namespace Microsoft.Boogie return output; } - } - - internal class ParserZ3 : ParserSMT - { - protected override void ParseITE(ref int i) - { - for (; ; ) - { - if (tokens[i] == "ite") - { - i++; - - for (; ; ) - { - if (tokens[i] == "(" && tokens[i + 1] == "and") - i += 2; - - if (tokens[i] == "(" && tokens[i + 1] == "=") - { - if (tokens[i + 3] == "(" && tokens[i + 4] == "-") - { - i += 7; - output.Add(GetValue(i - 2)); - } - if (tokens[i + 3] == "(" && tokens[i + 4] == "_") - { - i += 8; - output.Add(GetValue(i - 2)); - } - else - { - i += 4; - output.Add(GetValue(i - 1)); - } - - i++; - continue; - } - - output.Add("->"); - - if (tokens[i] == ")") i++; - - if (tokens[i] == "(" && tokens[i + 1] == "-") - { - i += 3; - output.Add(GetValue(i - 1)); - } - else if (tokens[i] == "(" && tokens[i + 1] == "_") - { - i += 4; - output.Add(GetValue(i - 1)); - } - else - { - i++; - output.Add(GetValue(i - 1)); - } - - output.Add(" "); - break; - } - } - - if (tokens[i] == "(" && tokens[i + 1] == "-") - { - i += 2; - output.Add("else"); - output.Add("->"); - output.Add(GetValue(i)); - break; - } - else if (tokens[i] == "(" && tokens[i + 1] == "_") - { - i += 3; - output.Add("else"); - output.Add("->"); - output.Add(GetValue(i)); - break; - } - else if (tokens[i] == ")" && tokens[i - 2] == "-") - { - i++; - continue; - } - else if (tokens[i] == ")" && tokens[i - 3] == "_") - { - i++; - continue; - } - else if (tokens[i] != "(") - { - output.Add("else"); - output.Add("->"); - output.Add(GetValue(i)); - break; - } - else i++; - } - } - - void ParseArgument(ref int i) - { - output.Add("{"); - output.Add(" "); - - i++; - } - - - protected override void ParseArray(ref int i) - { - while (tokens[i] != "as-array") - i++; - - output.Add("as-array[" + tokens[i + 1] + "]"); - } - - protected override void ParseLeftParenthesis(ref int i) - { - i++; - - switch (tokens[i]) - { - case "ite": - ParseITE(ref i); - break; - - case "Array": - ParseArray(ref i); - break; - - case "x!1": - ParseArgument(ref i); - break; - - case "_": - ParseBitVector(ref i); - break; - - default: - break; - } - } internal override void Run() { var selectFunctions = new Dictionary<int, Model.Func>(); var storeFunctions = new Dictionary<int, Model.Func>(); + arrayNum = 0; for (; ; ) { @@ -601,13 +407,26 @@ namespace Microsoft.Boogie { var funName = (string) words[0]; Model.Func fn = null; + int i = 4; + + if (words.Contains("@SPLIT")) + { + arrayNum++; + + fn = currModel.MkFunc(funName, 0); + fn.SetConstant(GetElt(words[2])); - if (words[2] != "{") + i = 8; + + funName = (string) words[4]; + fn = null; + } + + if (words[2] != "{" && words[6] != "{") BadModel("unidentified function definition 5"); fn = currModel.TryGetFunc(funName); - int i = 4; for (; ; ) { if (words[i] == "}") @@ -633,9 +452,7 @@ namespace Microsoft.Boogie break; } - if (i == 4 && words[3] == " " && words[5] == " ") { - if (fn == null) - fn = currModel.MkFunc(funName, 1); + if ((i == 4 || i == 8) && words[i - 1] == " " && words[i + 1] == " ") { if (fn.Else == null) fn.Else = GetElt(words[i]); i++; @@ -742,9 +559,163 @@ namespace Microsoft.Boogie } } + internal class ParserZ3 : ParserSMT + { + protected override void ParseITE(ref int i) + { + for (; ; ) + { + if (tokens[i] == "ite") + { + i++; + + for (; ; ) + { + if (tokens[i] == "(" && tokens[i + 1] == "and") + i += 2; + + if (tokens[i] == "(" && tokens[i + 1] == "=") + { + if (tokens[i + 3] == "(" && tokens[i + 4] == "-") + { + i += 7; + output.Add(GetValue(i - 2)); + } + else if (tokens[i + 3] == "(" && tokens[i + 4] == "_") + { + i += 8; + output.Add(GetValue(i - 2)); + } + else + { + i += 4; + output.Add(GetValue(i - 1)); + } + + i++; + continue; + } + + output.Add("->"); + + if (tokens[i] == ")") i++; + + if (tokens[i] == "(" && tokens[i + 1] == "-") + { + i += 3; + output.Add(GetValue(i - 1)); + } + else if (tokens[i] == "(" && tokens[i + 1] == "_") + { + i += 4; + output.Add(GetValue(i - 1)); + } + else + { + i++; + output.Add(GetValue(i - 1)); + } + + output.Add(" "); + break; + } + } + + if (tokens[i] == "(" && tokens[i + 1] == "-") + { + i += 2; + output.Add("else"); + output.Add("->"); + output.Add(GetValue(i)); + break; + } + else if (tokens[i] == "(" && tokens[i + 1] == "_") + { + i += 3; + output.Add("else"); + output.Add("->"); + output.Add(GetValue(i)); + break; + } + else if (tokens[i] == ")" && tokens[i - 2] == "-") + { + i++; + continue; + } + else if (tokens[i] == ")" && tokens[i - 3] == "_") + { + i++; + continue; + } + else if (tokens[i] != "(") + { + output.Add("else"); + output.Add("->"); + output.Add(GetValue(i)); + break; + } + else i++; + } + } + + void ParseArgument(ref int i) + { + output.Add("{"); + output.Add(" "); + + i++; + } + + protected override void ParseArray(ref int i) + { + while (tokens[i] != "as-array") + i++; + + output.Add("as-array[" + tokens[i + 1] + "]"); + } + + protected override void ParseTokens() + { + var i = 0; + bool doneParsing = false; + + while(!doneParsing) + { + switch (tokens[i]) + { + case ")": + ParseRightParenthesis(ref i); + break; + + case "define-fun": + ParseDefineFun(ref i); + break; + + case "Array": + ParseArray(ref i); + break; + + case "ite": + ParseITE(ref i); + break; + + case "x!1": + ParseArgument(ref i); + break; + + default: + i++; + break; + } + + if (i == tokens.Length) + doneParsing = true; + } + } + } + internal class ParserCVC4 : ParserSMT { - int arrayNum; int arity; void FindArity() @@ -944,221 +915,47 @@ namespace Microsoft.Boogie } else if (tokens[i] == ",") { - i += 2; - ParseBitVector(ref i); + //i += 2; + //ParseBitVector(ref i); + output.Add(GetValue(i + 4)); + i += 5; break; } } } - protected override void ParseLeftParenthesis(ref int i) + protected override void ParseTokens() { - i++; - - switch (tokens[i]) - { - case "ite": - ParseITE(ref i); - break; - - case "Array": - ParseArray(ref i); - break; - - case "_": - ParseBitVector(ref i); - break; - - default: - break; - } - } - - internal override void Run() - { - var selectFunctions = new Dictionary<int, Model.Func>(); - var storeFunctions = new Dictionary<int, Model.Func>(); - arrayNum = 0; + var i = 0; + bool doneParsing = false; - for (; ; ) + while(!doneParsing) { - 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; - - 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"); - - if (words.Count > 3 && words[1] == "->") + switch (tokens[i]) { - var funName = (string) words[0]; - Model.Func fn = null; - int i = 4; - - if (words.Contains("@SPLIT")) - { - arrayNum++; - - fn = currModel.MkFunc(funName, 0); - fn.SetConstant(GetElt(words[2])); - - i = 8; - - funName = (string) words[4]; - fn = null; - } - - if (words[2] != "{" && words[6] != "{") - BadModel("unidentified function definition 5"); - - fn = currModel.TryGetFunc(funName); - - for (; ; ) - { - if (words[i] == "}") - { - if (i == words.Count - 1) - { - if (fn == null) - fn = currModel.MkFunc(funName, 1); - break; - } - else - { - i++; - continue; - } - } - - for (; ; ) - { - if (words[i] == " ") - { - i++; - break; - } - - if ((i == 4 || i == 8) && words[i - 1] == " " && words[i + 1] == " ") { - if (fn.Else == null) - fn.Else = GetElt(words[i]); - i++; - continue; - } - - if (words[i] == "else") - { - if (words[i + 1] == "->") - { - i += 2; - - if (words[i] == "}") - BadModel("unidentified function definition 1"); - - if (words[i] == "{") - { - i++; - continue; - } - else - { - if (fn != null && !(words[i] == "#unspecified") && fn.Else == null) - fn.Else = GetElt(words[i]); - i++; - continue; - } - } - else - BadModel("unidentified function definition 2"); - } - - int arity = 0; - for (; ; ) - { - arity++; - if (words[arity + i] == " ") - { - arity -= 2; - break; - } - } - - if (words[i + arity] == "->") - { - i += arity + 1; - - 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); - } - } - 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); - } - } + case ")": + ParseRightParenthesis(ref i); + break; - var args = new Model.Element[fn.Arity]; + case "define-fun": + ParseDefineFun(ref i); + break; - for (var idx = 0; idx < fn.Arity; ++idx) - args[idx] = GetElt(words[idx + i - arity - 1]); + case "Array": + ParseArray(ref i); + break; - fn.AddApp(GetElt(words[i]), args); + case "ite": + ParseITE(ref i); + break; - i++; - break; - } - } + default: + i++; + break; } - 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"); + if (i == tokens.Length) + doneParsing = true; } } } |