From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Source/Basetypes/Set.cs | 570 ++++++++++++++++++++++++------------------------
 1 file changed, 285 insertions(+), 285 deletions(-)

(limited to 'Source/Basetypes/Set.cs')

diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs
index dfd65b4b..0cc1d103 100644
--- a/Source/Basetypes/Set.cs
+++ b/Source/Basetypes/Set.cs
@@ -1,286 +1,286 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.Boogie {
-  using System;
-  using System.IO;
-  using System.Collections;
-  using System.Collections.Generic;
-  using System.Diagnostics.Contracts;
-
-  /// <summary>
-  /// A class representing a mathematical set.
-  /// </summary>
-  public class GSet<T> : ICloneable, IEnumerable, IEnumerable<T> {
-    /*[Own]*/
-    Dictionary<T, int> ht;
-    List<T> arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic
-
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(ht != null);
-      Contract.Invariant(arr != null);
-      Contract.Invariant(ht.Count == arr.Count);
-    }
-
-
-    public GSet() {
-      ht = new Dictionary<T, int>();
-      arr = new List<T>();
-      //:base();
-    }
-
-    private GSet(Dictionary<T,int>/*!*/ ht, List<T> arr) {
-      Contract.Requires(ht != null);
-      Contract.Requires(arr != null);
-      this.ht = ht;
-      this.arr = arr;
-      //:base();
-    }
-
-    public GSet(int capacity) {
-      ht = new Dictionary<T, int>(capacity);
-      arr = new List<T>(capacity);
-      //:base();
-    }
-
-
-    public readonly static GSet<T>/*!*/ Empty = new GSet<T>();
-
-    public void Clear() {
-      ht.Clear();
-      arr.Clear();
-    }
-
-    /// <summary>
-    /// This method idempotently adds "o" to the set.
-    /// In notation:
-    ///   this.SetElements =  this.SetElements_old \union {o};
-    /// </summary>
-    public void Add(T o) {
-      if (!ht.ContainsKey(o)) {
-        ht[o] = arr.Count;
-        arr.Add(o);
-      }
-    }
-
-    /// <summary>
-    /// this.SetElements =  this.SetElements_old \union s.GSet<T>Elements;
-    /// </summary>
-    public void AddRange(IEnumerable<T> s) {
-      foreach (T o in s) {
-        Add(o);
-      }
-    }
-
-    /// <summary>
-    /// this.SetElements =  this.SetElements_old \setminus {o};
-    /// </summary>
-    public void Remove(T o) {
-      int idx;
-      if (ht.TryGetValue(o, out idx)) {
-        var last = arr[arr.Count - 1];
-        arr.RemoveAt(arr.Count - 1);
-        if (idx != arr.Count) {
-          arr[idx] = last;
-          ht[last] = idx;
-        }
-        ht.Remove(o);
-      }
-    }
-
-    /// <summary>
-    /// this.SetElements =  this.SetElements_old \setminus s.SetElements;
-    /// </summary>
-    public void RemoveRange(IEnumerable<T> s) {
-      Contract.Requires(s != null);
-      if (s == this) {
-        ht.Clear();
-        arr.Clear();
-      } else {
-        foreach (T o in s) {
-          Remove(o);
-        }
-      }
-    }
-
-    /// <summary>
-    /// Returns an arbitrary element from the set.
-    /// </summary>
-    public T Choose() {
-      Contract.Requires((Count > 0));
-      foreach(var e in this) 
-        return e;
-      return default(T);
-    }
-
-    /// <summary>
-    /// Picks an arbitrary element from the set, removes it, and returns it.
-    /// </summary>
-    public T Take() {
-      Contract.Requires((Count > 0));
-      Contract.Ensures(Count == Contract.OldValue(Count) - 1);
-      T r = Choose();
-      Remove(r);
-      return r;
-    }
-
-    public void Intersect(GSet<T>/*!*/ s) {
-      Contract.Requires(s != null);
-      if (s == this) return;
-      ht.Clear();
-      var newArr = new List<T>();
-      foreach (T key in arr) {
-        if (s.ht.ContainsKey(key)) {
-          ht[key] = newArr.Count;
-          newArr.Add(key);
-        }
-      }
-      arr = newArr;
-    }
-
-    /// <summary>
-    /// The getter returns true iff "o" is in the set.
-    /// The setter adds the value "o" (for "true") or removes "o" (for "false")
-    /// </summary>
-    public bool this[T o] {
-      get {
-        return ht.ContainsKey(o);
-      }
-      set {
-        if (value) {
-          Add(o);
-        } else {
-          Remove(o);
-        }
-      }
-    }
-
-    /// <summary>
-    /// Returns true iff "o" is an element of "this".
-    /// </summary>
-    /// <param name="o"></param>
-    /// <returns></returns>
-    [Pure]
-    public bool Contains(T o) {
-      return this.ht.ContainsKey(o);
-    }
-
-    /// <summary>
-    /// Returns true iff every element of "s" is an element of "this", that is, if
-    /// "s" is a subset of "this".
-    /// </summary>
-    /// <param name="s"></param>
-    /// <returns></returns>
-    public bool ContainsRange(IEnumerable<T> s) {
-      Contract.Requires(s != null);
-      if (s != this) {
-        foreach (T key in s) {
-          if (!this.ht.ContainsKey(key)) {
-            return false;
-          }
-        }
-      }
-      return true;
-    }
-
-    public object/*!*/ Clone() {
-      Contract.Ensures(Contract.Result<object>() != null);
-      return new GSet<T>(new Dictionary<T,int>(ht), new List<T>(arr));
-    }
-
-    public virtual int Count {
-      get {
-        return ht.Count;
-      }
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      string s = null;
-      foreach (object/*!*/ key in ht.Keys) {
-        Contract.Assert(key != null);
-        if (s == null) {
-          s = "{";
-        } else {
-          s += ", ";
-        }
-        s += key.ToString();
-      }
-      if (s == null) {
-        return "{}";
-      } else {
-        return s + "}";
-      }
-    }
-
-    //----------------------------- Static Methods ---------------------------------
-
-    // Functional Intersect
-    public static GSet<T>/*!*/ Intersect(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
-      Contract.Requires(b != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<GSet<T>>() != null);
-      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
-      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
-      res.Intersect(b);
-      return res;
-    }
-    // Functional Union
-    public static GSet<T>/*!*/ Union(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
-      Contract.Requires(a != null);
-      Contract.Requires(b != null);
-      Contract.Ensures(Contract.Result<GSet<T>>() != null);
-      //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
-      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
-      res.AddRange(b);
-      return res;
-    }
-
-    public delegate bool SetFilter(object/*!*/ obj);
-
-    public static GSet<T>/*!*/ Filter(GSet<T>/*!*/ a, Func<T,bool> filter) {
-      Contract.Requires(filter != null);
-      Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<GSet<T>>() != null);
-      GSet<T> inter = new GSet<T>();
-
-      foreach (T elem in a) {
-        Contract.Assert(elem != null);
-        if (filter(elem)) {
-          inter.Add(elem);
-        }
-      }
-      return inter;
-    }
-
-    public IEnumerator<T> GetEnumerator()
-    {
-      return arr.GetEnumerator();
-    }
-
-    IEnumerator IEnumerable.GetEnumerator()
-    {
-      return ((IEnumerable)arr).GetEnumerator();
-    }
-
-    public bool AddAll(IEnumerable s)
-    {
-      foreach (T e in s) Add(e);
-      return true;
-    }
-  }
-
-
-  public interface IWorkList : ICollection {
-    bool Add(object o);
-    bool AddAll(IEnumerable objs);
-    bool IsEmpty();
-    object Pull();
-  }
-
-
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie {
+  using System;
+  using System.IO;
+  using System.Collections;
+  using System.Collections.Generic;
+  using System.Diagnostics.Contracts;
+
+  /// <summary>
+  /// A class representing a mathematical set.
+  /// </summary>
+  public class GSet<T> : ICloneable, IEnumerable, IEnumerable<T> {
+    /*[Own]*/
+    Dictionary<T, int> ht;
+    List<T> arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic
+
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(ht != null);
+      Contract.Invariant(arr != null);
+      Contract.Invariant(ht.Count == arr.Count);
+    }
+
+
+    public GSet() {
+      ht = new Dictionary<T, int>();
+      arr = new List<T>();
+      //:base();
+    }
+
+    private GSet(Dictionary<T,int>/*!*/ ht, List<T> arr) {
+      Contract.Requires(ht != null);
+      Contract.Requires(arr != null);
+      this.ht = ht;
+      this.arr = arr;
+      //:base();
+    }
+
+    public GSet(int capacity) {
+      ht = new Dictionary<T, int>(capacity);
+      arr = new List<T>(capacity);
+      //:base();
+    }
+
+
+    public readonly static GSet<T>/*!*/ Empty = new GSet<T>();
+
+    public void Clear() {
+      ht.Clear();
+      arr.Clear();
+    }
+
+    /// <summary>
+    /// This method idempotently adds "o" to the set.
+    /// In notation:
+    ///   this.SetElements =  this.SetElements_old \union {o};
+    /// </summary>
+    public void Add(T o) {
+      if (!ht.ContainsKey(o)) {
+        ht[o] = arr.Count;
+        arr.Add(o);
+      }
+    }
+
+    /// <summary>
+    /// this.SetElements =  this.SetElements_old \union s.GSet<T>Elements;
+    /// </summary>
+    public void AddRange(IEnumerable<T> s) {
+      foreach (T o in s) {
+        Add(o);
+      }
+    }
+
+    /// <summary>
+    /// this.SetElements =  this.SetElements_old \setminus {o};
+    /// </summary>
+    public void Remove(T o) {
+      int idx;
+      if (ht.TryGetValue(o, out idx)) {
+        var last = arr[arr.Count - 1];
+        arr.RemoveAt(arr.Count - 1);
+        if (idx != arr.Count) {
+          arr[idx] = last;
+          ht[last] = idx;
+        }
+        ht.Remove(o);
+      }
+    }
+
+    /// <summary>
+    /// this.SetElements =  this.SetElements_old \setminus s.SetElements;
+    /// </summary>
+    public void RemoveRange(IEnumerable<T> s) {
+      Contract.Requires(s != null);
+      if (s == this) {
+        ht.Clear();
+        arr.Clear();
+      } else {
+        foreach (T o in s) {
+          Remove(o);
+        }
+      }
+    }
+
+    /// <summary>
+    /// Returns an arbitrary element from the set.
+    /// </summary>
+    public T Choose() {
+      Contract.Requires((Count > 0));
+      foreach(var e in this) 
+        return e;
+      return default(T);
+    }
+
+    /// <summary>
+    /// Picks an arbitrary element from the set, removes it, and returns it.
+    /// </summary>
+    public T Take() {
+      Contract.Requires((Count > 0));
+      Contract.Ensures(Count == Contract.OldValue(Count) - 1);
+      T r = Choose();
+      Remove(r);
+      return r;
+    }
+
+    public void Intersect(GSet<T>/*!*/ s) {
+      Contract.Requires(s != null);
+      if (s == this) return;
+      ht.Clear();
+      var newArr = new List<T>();
+      foreach (T key in arr) {
+        if (s.ht.ContainsKey(key)) {
+          ht[key] = newArr.Count;
+          newArr.Add(key);
+        }
+      }
+      arr = newArr;
+    }
+
+    /// <summary>
+    /// The getter returns true iff "o" is in the set.
+    /// The setter adds the value "o" (for "true") or removes "o" (for "false")
+    /// </summary>
+    public bool this[T o] {
+      get {
+        return ht.ContainsKey(o);
+      }
+      set {
+        if (value) {
+          Add(o);
+        } else {
+          Remove(o);
+        }
+      }
+    }
+
+    /// <summary>
+    /// Returns true iff "o" is an element of "this".
+    /// </summary>
+    /// <param name="o"></param>
+    /// <returns></returns>
+    [Pure]
+    public bool Contains(T o) {
+      return this.ht.ContainsKey(o);
+    }
+
+    /// <summary>
+    /// Returns true iff every element of "s" is an element of "this", that is, if
+    /// "s" is a subset of "this".
+    /// </summary>
+    /// <param name="s"></param>
+    /// <returns></returns>
+    public bool ContainsRange(IEnumerable<T> s) {
+      Contract.Requires(s != null);
+      if (s != this) {
+        foreach (T key in s) {
+          if (!this.ht.ContainsKey(key)) {
+            return false;
+          }
+        }
+      }
+      return true;
+    }
+
+    public object/*!*/ Clone() {
+      Contract.Ensures(Contract.Result<object>() != null);
+      return new GSet<T>(new Dictionary<T,int>(ht), new List<T>(arr));
+    }
+
+    public virtual int Count {
+      get {
+        return ht.Count;
+      }
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      string s = null;
+      foreach (object/*!*/ key in ht.Keys) {
+        Contract.Assert(key != null);
+        if (s == null) {
+          s = "{";
+        } else {
+          s += ", ";
+        }
+        s += key.ToString();
+      }
+      if (s == null) {
+        return "{}";
+      } else {
+        return s + "}";
+      }
+    }
+
+    //----------------------------- Static Methods ---------------------------------
+
+    // Functional Intersect
+    public static GSet<T>/*!*/ Intersect(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
+      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
+      res.Intersect(b);
+      return res;
+    }
+    // Functional Union
+    public static GSet<T>/*!*/ Union(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
+      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
+      res.AddRange(b);
+      return res;
+    }
+
+    public delegate bool SetFilter(object/*!*/ obj);
+
+    public static GSet<T>/*!*/ Filter(GSet<T>/*!*/ a, Func<T,bool> filter) {
+      Contract.Requires(filter != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      GSet<T> inter = new GSet<T>();
+
+      foreach (T elem in a) {
+        Contract.Assert(elem != null);
+        if (filter(elem)) {
+          inter.Add(elem);
+        }
+      }
+      return inter;
+    }
+
+    public IEnumerator<T> GetEnumerator()
+    {
+      return arr.GetEnumerator();
+    }
+
+    IEnumerator IEnumerable.GetEnumerator()
+    {
+      return ((IEnumerable)arr).GetEnumerator();
+    }
+
+    public bool AddAll(IEnumerable s)
+    {
+      foreach (T e in s) Add(e);
+      return true;
+    }
+  }
+
+
+  public interface IWorkList : ICollection {
+    bool Add(object o);
+    bool AddAll(IEnumerable objs);
+    bool IsEmpty();
+    object Pull();
+  }
+
+
 }
\ No newline at end of file
-- 
cgit v1.2.3