diff options
| author |  MichalMoskal <unknown> | 2011-02-17 18:58:14 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-17 18:58:14 +0000 |
| commit | 6ecb825daaf77f2e783106509c6b33e76e2f9e11 (patch) | |
| tree | b21627d5933991eee6489cce67376061de51c2dc /Source/Provers/SMTLib/SExpr.cs | |
| parent | f79fc4e0abd823571d5705106a4192d61b801b84 (diff) | |
Start implementation of pipe communication in SMTLIB backend
Diffstat (limited to 'Source/Provers/SMTLib/SExpr.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SExpr.cs | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs new file mode 100644 index 00000000..2d143830 --- /dev/null +++ b/Source/Provers/SMTLib/SExpr.cs @@ -0,0 +1,105 @@ +//-----------------------------------------------------------------------------
+//
+// 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 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
+ 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
+
+ }
+}
|