1 files changed, 150 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs
index 461e1ee8..ba07ec27 100644
--- a/Source/Provers/SMTLib/SExpr.cs
+++ b/Source/Provers/SMTLib/SExpr.cs
@@ -106,6 +106,156 @@ namespace Microsoft.Boogie
     }
     #endregion
 
+    #region parsing
+
+    public abstract class Parser
+    {
+        System.IO.StreamReader sr;
+        int linePos = 0;
+        string currLine = null;
+
+        public Parser(System.IO.StreamReader _sr)
+        {
+            sr = _sr;
+        }
+        string Read()
+        {
+            return sr.ReadLine();
+        }
+        char SkipWs()
+        {
+            while (true)
+            {
+                if (currLine == null)
+                {
+                    currLine = Read();
+                    if (currLine == null)
+                        return '\0';
+                }
+
+                while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))
+                    linePos++;
+
+                if (linePos < currLine.Length)
+                    return currLine[linePos];
+                else
+                {
+                    currLine = null;
+                    linePos = 0;
+                }
+            }
+        }
+
+        void Shift()
+        {
+            linePos++;
+        }
+
+        string ParseId()
+        {
+            var sb = new StringBuilder();
+
+            var beg = SkipWs();
+
+            var quoted = beg == '"' || beg == '|';
+            if (quoted)
+                Shift();
+            while (true)
+            {
+                if (linePos >= currLine.Length)
+                {
+                    if (quoted)
+                    {
+                        sb.Append("\n");
+                        currLine = Read();
+                        linePos = 0;
+                        if (currLine == null)
+                            break;
+                    }
+                    else break;
+                }
+
+                var c = currLine[linePos++];
+                if (quoted && c == beg)
+                    break;
+                if (!quoted && (char.IsWhiteSpace(c) || c == '(' || c == ')'))
+                {
+                    linePos--;
+                    break;
+                }
+                if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"')
+                {
+                    sb.Append('"');
+                    linePos++;
+                    continue;
+                }
+                sb.Append(c);
+            }
+
+            return sb.ToString();
+        }
+
+        public abstract void ParseError(string msg);
+
+        public IEnumerable<SExpr> ParseSExprs(bool top)
+        {
+            while (true)
+            {
+                var c = SkipWs();
+                if (c == '\0')
+                    break;
+
+                if (c == ')')
+                {
+                    if (top)
+                        ParseError("stray ')'");
+                    break;
+                }
+
+                string id;
+
+                if (c == '(')
+                {
+                    Shift();
+                    c = SkipWs();
+                    if (c == '\0')
+                    {
+                        ParseError("expecting something after '('");
+                        break;
+                    }
+                    else if (c == '(')
+                    {
+                        id = "";
+                    }
+                    else
+                    {
+                        id = ParseId();
+                    }
+
+                    var args = ParseSExprs(false).ToArray();
+
+                    c = SkipWs();
+                    if (c == ')')
+                    {
+                        Shift();
+                    }
+                    else
+                    {
+                        ParseError("unclosed '(" + id + "'");
+                    }
+                    yield return new SExpr(id, args);
+                }
+                else
+                {
+                    id = ParseId();
+                    yield return new SExpr(id);
+                }
+
+                if (top) break;
+            }
+        }
+    }
+    #endregion
   }
 }