From ca8dbdd3d3b0821b494f3202796456e3fffb3635 Mon Sep 17 00:00:00 2001 From: pantazis Date: Wed, 12 Jun 2013 03:23:15 +0100 Subject: naive SMTLIB2 Parser --- Source/Model/Model.cs | 332 +++++--------------------------------------------- 1 file changed, 32 insertions(+), 300 deletions(-) (limited to 'Source/Model') diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 16dec8b0..34d39863 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -695,305 +695,37 @@ namespace Microsoft.Boogie foreach (var f in functions) f.Substitute(mapping); } - class Parser - { - internal System.IO.TextReader rd; - string lastLine = ""; - int lineNo; - internal List resModels = new List(); - Model currModel; - - void BadModel(string msg) - { - throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine)); - } - - static char[] seps = new char[] { ' ' }; - - int CountOpenParentheses(string s, int n) { - int f = n; - foreach (char c in s) { - if (c == '(') - f++; - else if (c == ')') - f--; - } - if (f < 0) BadModel("mismatched parentheses in datatype term"); - return f; - } - - static Regex bv = new Regex(@"\(_ BitVec (\d+)\)"); - - /* - List GetFunctionTuple(string newLine) { - if (newLine == null) - return null; - 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) { - return null; - } - line += newLine; - openParenCounter = CountOpenParentheses(newLine, openParenCounter); - } - } - - line = line.Replace("(", " ( "); - 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 == "(") { - wordStack.Push(newTuple.Count - 1); - } - else if (elem == ")") { - int openParenIndex = wordStack.Pop(); - List ls = new List(); - for (int j = openParenIndex; j < newTuple.Count; j++) - { - ls.Add(newTuple[j]); - } - newTuple.RemoveRange(openParenIndex, newTuple.Count - openParenIndex); - newTuple.Add(ls); - } - else { - newTuple.Add(elem); - } - } - return newTuple; - } - */ - - List GetFunctionTuple(string newLine) - { - if (newLine == null) - return null; - 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) - { - return null; - } - line += newLine; - 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); - } - } - else if (wordStack.Count > 0) - { - wordStack.Peek().Add(elem); - } - else - { - newTuple.Add(elem); - } - } - return newTuple; - } - - string[] GetWords(string line) - { - if (line == null) - return null; - var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries); - return words; - } - - string ReadLine() - { - var l = rd.ReadLine(); - if (l != null) { - lineNo++; - lastLine = l; - } - return l; - } - - Element GetElt(object o) { - string s = o as string; - if (s != null) - return GetElt(s); - List os = (List)o; - List args = new List(); - for (int i = 1; i < os.Count; i++) { - args.Add(GetElt(os[i])); - } - return new DatatypeValue(currModel, (string)os[0], args); - } - - Element GetElt(string name) { - Element ret = currModel.TryMkElement(name); - if (ret == null) - BadModel("invalid element name " + name); - return ret; - } - - void NewModel() - { - lastLine = ""; - currModel = new Model(); - resModels.Add(currModel); - } - - internal void Run() - { - 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 == "Z3 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 = GetFunctionTuple(line); - if (words.Count == 0) continue; - var lastWord = words[words.Count - 1]; - - if (currModel == null) - BadModel("model begin marker not found"); - - if (line.StartsWith("*** STATE ")) { - var name = line.Substring(10); - CapturedState cs; - if (name == "") - cs = currModel.InitialState; - else - cs = currModel.MkState(name); - for (; ; ) { - var tmpline = ReadLine(); - if (tmpline == "*** END_STATE") break; - var tuple = GetFunctionTuple(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]; - Func fn = null; - - if (lastWord is string && ((string) lastWord) == "{") { - fn = currModel.TryGetFunc(funName); - for ( ; ; ) { - var tuple = GetFunctionTuple(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; - if (fn.Else == null) - 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]; - if (tuple0 == "else") { - if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) { - 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); - } - } 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 Element[fn.Arity]; - for (int i = 0; i < fn.Arity; ++i) - args[i] = GetElt(tuple[i]); - fn.AddApp(GetElt(resultName), args); - } - } else { - fn = currModel.MkFunc(funName, 0); - fn.SetConstant(GetElt(lastWord)); - } - } else { - BadModel("unidentified line"); - } - } - } - } - - public static List ParseModels(System.IO.TextReader rd) - { - var p = new Parser(); - p.rd = rd; - p.Run(); - return p.resModels; - } + public static List ParseModels(System.IO.TextReader rd, string modelType) + { + ModelParser p; + + switch (modelType) + { + case "Z3": + p = new ParserZ3(); + break; + case "CVC4": + p = new ParserCVC4(); + break; + default: + p = new ParserZ3_2(); + break; + } + + p.rd = rd; + p.Run(); + + return p.resModels; + } + + public static List ParseModels(System.IO.TextReader rd) + { + ModelParser p = new ParserZ3_2(); + + p.rd = rd; + p.Run(); + + return p.resModels; + } } } -- cgit v1.2.3