naive SMTLIB2 Parser

1 files changed, 32 insertions, 300 deletions

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<Model> resModels = new List<Model>();

-      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<object> 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<object> newTuple = new List<object>();

-        Stack<int> wordStack = new Stack<int>();

-        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<object> ls = new List<object>();

-            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<object> 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<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];

-              if (elem == "(")

-              {

-                  List<object> ls = new List<object>();

-                  wordStack.Push(ls);

-              }

-              else if (elem == ")")

-              {

-                  List<object> 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<object> os = (List<object>)o;

-        List<Element> args = new List<Element>();

-        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<int, Model.Func>();

-        var storeFunctions = new Dictionary<int, Model.Func>();

-        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 == "<initial>")

-              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<Model> ParseModels(System.IO.TextReader rd)

-    {

-      var p = new Parser();

-      p.rd = rd;

-      p.Run();

-      return p.resModels;

-    }

+	public static List<Model> 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<Model> ParseModels(System.IO.TextReader rd)

+	{

+		ModelParser p = new ParserZ3_2();

+

+		p.rd = rd;

+		p.Run();

+

+		return p.resModels;

+	}

   }

 }