summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SExpr.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/SExpr.cs')
-rw-r--r--Source/Provers/SMTLib/SExpr.cs526
1 files changed, 263 insertions, 263 deletions
diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs
index ac681b8a..3e9687e1 100644
--- a/Source/Provers/SMTLib/SExpr.cs
+++ b/Source/Provers/SMTLib/SExpr.cs
@@ -1,263 +1,263 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Linq;
-using System.Collections.Generic;
-using System.Collections.ObjectModel;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Globalization;
-
-namespace Microsoft.Boogie
-{
- public class SExpr
- {
- static readonly SExpr[] EmptyArgs = new SExpr[0];
- public readonly string Name;
- public SExpr[] Arguments
- {
- get
- {
- Contract.Ensures(Contract.Result<SExpr[]>() != null);
- Contract.Ensures(Contract.ForAll(Contract.Result<SExpr[]>(), expr => expr != null));
-
- return this.arguments;
- }
- }
-
- public SExpr this[int idx]
- {
- get
- {
- return Arguments[idx];
- }
- }
-
- public int ArgCount
- {
- get { return arguments.Length; }
- }
-
- public bool IsId
- {
- get { return Arguments.Length == 0; }
- }
-
- private readonly SExpr[] arguments;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(this.Name != null);
- Contract.Invariant(this.arguments != null);
- Contract.Invariant(Contract.ForAll(this.arguments, arg => arg != null));
- }
-
- public SExpr(string name, params SExpr[] args)
- : this(name, (IEnumerable<SExpr>)args)
- {
- Contract.Requires(name != null);
- Contract.Requires(args != null);
- Contract.Requires(Contract.ForAll(args, x => x != null));
- }
-
- public SExpr(string name, IEnumerable<SExpr> args)
- {
- Contract.Requires(name != null);
- Contract.Requires(args != null);
- // We don't want to evaluate args twice!
- // Contract.Requires(Contract.ForAll(args, x => x != null));
- Name = name;
- arguments = args.ToArray();
- }
-
- public SExpr(string name)
- : this(name, EmptyArgs)
- {
- Contract.Requires(name != null);
- }
-
- #region pretty-printing
- void WriteTo(StringBuilder sb)
- {
- Contract.Requires(sb != null);
-
- if (Arguments.Length > 0) sb.Append('(');
- if (Name.Any(Char.IsWhiteSpace))
- sb.Append("\"").Append(Name).Append("\"");
- else if (Name.Length == 0)
- sb.Append("()");
- else
- sb.Append(Name);
- foreach (var a in Arguments) {
- sb.Append(' ');
- a.WriteTo(sb);
- }
- if (Arguments.Length > 0) sb.Append(')');
- }
-
- public override string ToString()
- {
- var sb = new StringBuilder();
- this.WriteTo(sb);
- return sb.ToString();
- }
- #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
- }
-}
-
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.Collections.ObjectModel;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Globalization;
+
+namespace Microsoft.Boogie
+{
+ public class SExpr
+ {
+ static readonly SExpr[] EmptyArgs = new SExpr[0];
+ public readonly string Name;
+ public SExpr[] Arguments
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<SExpr[]>() != null);
+ Contract.Ensures(Contract.ForAll(Contract.Result<SExpr[]>(), expr => expr != null));
+
+ return this.arguments;
+ }
+ }
+
+ public SExpr this[int idx]
+ {
+ get
+ {
+ return Arguments[idx];
+ }
+ }
+
+ public int ArgCount
+ {
+ get { return arguments.Length; }
+ }
+
+ public bool IsId
+ {
+ get { return Arguments.Length == 0; }
+ }
+
+ private readonly SExpr[] arguments;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(this.Name != null);
+ Contract.Invariant(this.arguments != null);
+ Contract.Invariant(Contract.ForAll(this.arguments, arg => arg != null));
+ }
+
+ public SExpr(string name, params SExpr[] args)
+ : this(name, (IEnumerable<SExpr>)args)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(args != null);
+ Contract.Requires(Contract.ForAll(args, x => x != null));
+ }
+
+ public SExpr(string name, IEnumerable<SExpr> args)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(args != null);
+ // We don't want to evaluate args twice!
+ // Contract.Requires(Contract.ForAll(args, x => x != null));
+ Name = name;
+ arguments = args.ToArray();
+ }
+
+ public SExpr(string name)
+ : this(name, EmptyArgs)
+ {
+ Contract.Requires(name != null);
+ }
+
+ #region pretty-printing
+ void WriteTo(StringBuilder sb)
+ {
+ Contract.Requires(sb != null);
+
+ if (Arguments.Length > 0) sb.Append('(');
+ if (Name.Any(Char.IsWhiteSpace))
+ sb.Append("\"").Append(Name).Append("\"");
+ else if (Name.Length == 0)
+ sb.Append("()");
+ else
+ sb.Append(Name);
+ foreach (var a in Arguments) {
+ sb.Append(' ');
+ a.WriteTo(sb);
+ }
+ if (Arguments.Length > 0) sb.Append(')');
+ }
+
+ public override string ToString()
+ {
+ var sb = new StringBuilder();
+ this.WriteTo(sb);
+ return sb.ToString();
+ }
+ #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
+ }
+}
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 02:04:51 +0000