From b8b543484eba84d3aaf437333656017ad474b372 Mon Sep 17 00:00:00 2001 From: pantazis Date: Wed, 12 Jun 2013 16:36:07 +0100 Subject: simplified SMTLIB2 parser by merging some parsing methods for the CVC4 and Z3 sub-parsers --- Source/Model/ModelParser.cs | 731 ++++++++++++++++---------------------------- 1 file changed, 264 insertions(+), 467 deletions(-) (limited to 'Source/Model') 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 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 GetParsedTokens(string newLine) + List 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(); var storeFunctions = new Dictionary(); + 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])); + + i = 8; + + funName = (string) words[4]; + fn = null; + } - if (words[2] != "{") + 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,77 +559,231 @@ namespace Microsoft.Boogie } } - internal class ParserCVC4 : ParserSMT + internal class ParserZ3 : ParserSMT { - int arrayNum; - int arity; - - 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++; - } - } - /* protected override void ParseITE(ref int i) { - List args = new List(); - List results = new List(); - - FindArity(); - - output.Add("{"); - output.Add(" "); - for (; ; ) { - if (tokens[i] == ")") + if (tokens[i] == "ite") { - if ((tokens[i + 1] == ")" || tokens[i + 2] == ")") && - (tokens[i + 2] != "ite" || tokens[i + 3] != "ite") && - (tokens[i - 3] == "_" || tokens[i - 2] == "-")) - { - results.Add(GetValue(i - 1)); - break; - } - else - { - args.Add(GetValue(i - 1)); + i++; - if (tokens[i + 1] == "(" && tokens[i + 2] == "-") - { - results.Add(GetValue(i + 3)); - i += 5; - } - else if (tokens[i + 2] != "ite") - { - results.Add(GetValue(i + 1)); + for (; ; ) + { + if (tokens[i] == "(" && tokens[i + 1] == "and") i += 2; - } - else i++; - } - } - else i++; - } - int idx = 0; - for (int j = 0; j < results.Count - 1; j++) - { + 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 arity; + + 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++; + } + } + /* + protected override void ParseITE(ref int i) + { + List args = new List(); + List results = new List(); + + FindArity(); + + output.Add("{"); + output.Add(" "); + + for (; ; ) + { + if (tokens[i] == ")") + { + if ((tokens[i + 1] == ")" || tokens[i + 2] == ")") && + (tokens[i + 2] != "ite" || tokens[i + 3] != "ite") && + (tokens[i - 3] == "_" || tokens[i - 2] == "-")) + { + results.Add(GetValue(i - 1)); + break; + } + else + { + args.Add(GetValue(i - 1)); + + if (tokens[i + 1] == "(" && tokens[i + 2] == "-") + { + results.Add(GetValue(i + 3)); + i += 5; + } + else if (tokens[i + 2] != "ite") + { + results.Add(GetValue(i + 1)); + i += 2; + } + else i++; + } + } + else i++; + } + + int idx = 0; + for (int j = 0; j < results.Count - 1; j++) + { if (arity == 1) { output.Add(args[idx]); @@ -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) - { - 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() + protected override void ParseTokens() { - var selectFunctions = new Dictionary(); - var storeFunctions = new Dictionary(); - 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; } } } -- cgit v1.2.3