From f2800362628674094694b1d95bc0ba093745b0d8 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Wed, 7 Dec 2011 10:38:22 -0800
Subject: Make set iteration order deterministic Make the set class generic

---
 Source/Basetypes/Set.cs | 140 +++++++++++++++++++++++++-----------------------
 1 file changed, 73 insertions(+), 67 deletions(-)

(limited to 'Source/Basetypes')

diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs
index e31e5399..b11bf9c4 100644
--- a/Source/Basetypes/Set.cs
+++ b/Source/Basetypes/Set.cs
@@ -7,41 +7,50 @@ 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 Set : ICloneable, IEnumerable {
+  public class GSet<T> : ICloneable, IEnumerable, IEnumerable<T> {
     /*[Own]*/
-    Hashtable ht;
+    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);
     }
 
 
-    public Set() {
-      ht = new Hashtable();
+    public GSet() {
+      ht = new Dictionary<T, int>();
+      arr = new List<T>();
       //:base();
     }
 
-    private Set(Hashtable/*!*/ ht) {
+    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 Set(int capacity) {
-      ht = new Hashtable(capacity);
+    public GSet(int capacity) {
+      ht = new Dictionary<T, int>(capacity);
+      arr = new List<T>(capacity);
       //:base();
     }
 
 
-    public readonly static Set/*!*/ Empty = new Set();
+    public readonly static GSet<T>/*!*/ Empty = new GSet<T>();
 
     public void Clear() {
       ht.Clear();
+      arr.Clear();
     }
 
     /// <summary>
@@ -49,18 +58,18 @@ namespace Microsoft.Boogie {
     /// In notation:
     ///   this.SetElements =  this.SetElements_old \union {o};
     /// </summary>
-    public void Add(object/*!*/ o) {
-      Contract.Requires(o != null);
-      ht[o] = o;
+    public void Add(T o) {
+      if (!ht.ContainsKey(o)) {
+        ht[o] = arr.Count;
+        arr.Add(o);
+      }
     }
 
     /// <summary>
-    /// this.SetElements =  this.SetElements_old \union s.SetElements;
+    /// this.SetElements =  this.SetElements_old \union s.GSet<T>Elements;
     /// </summary>
-    public void AddRange(Set/*!*/ s) {
-      Contract.Requires(s != null);
-      foreach (object/*!*/ o in s) {
-        Contract.Assert(o != null);
+    public void AddRange(IEnumerable<T> s) {
+      foreach (T o in s) {
         Add(o);
       }
     }
@@ -68,21 +77,19 @@ namespace Microsoft.Boogie {
     /// <summary>
     /// this.SetElements =  this.SetElements_old \setminus {o};
     /// </summary>
-    public void Remove(object/*!*/ o) {
-      Contract.Requires(o != null);
+    public void Remove(T o) {
       ht.Remove(o);
     }
 
     /// <summary>
-    /// this.SetElements =  this.SetElements_old \setminus s.SetElements;
+    /// this.GSet<T>Elements =  this.GSet<T>Elements_old \setminus s.GSet<T>Elements;
     /// </summary>
-    public void RemoveRange(Set/*!*/ s) {
+    public void RemoveRange(IEnumerable<T> s) {
       Contract.Requires(s != null);
       if (s == this) {
         ht.Clear();
       } else {
-        foreach (object/*!*/ o in s) {
-          Contract.Assert(o != null);
+        foreach (T o in s) {
           ht.Remove(o);
         }
       }
@@ -91,45 +98,44 @@ namespace Microsoft.Boogie {
     /// <summary>
     /// Returns an arbitrary element from the set.
     /// </summary>
-    public object/*!*/ Choose() {
+    public T Choose() {
       Contract.Requires((Count > 0));
-      Contract.Ensures(Contract.Result<object>() != null);
-      IEnumerator iter = GetEnumerator();
-      iter.MoveNext();
-      return cce.NonNull(iter.Current);
+      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 object/*!*/ Take() {
+    public T Take() {
       Contract.Requires((Count > 0));
       Contract.Ensures(Contract.Result<object>() != null);
       Contract.Ensures(Count == Contract.OldValue(Count) - 1);
-      object r = Choose();
+      T r = Choose();
       Remove(r);
       return r;
     }
 
-    public void Intersect(Set/*!*/ s) {
+    public void Intersect(GSet<T>/*!*/ s) {
       Contract.Requires(s != null);
-      Hashtable h = new Hashtable(ht.Count);
-      foreach (object/*!*/ key in ht.Keys) {
-        Contract.Assert(key != null);
+      ht.Clear();
+      var newArr = new List<T>();
+      foreach (T key in this) {
         if (s.ht.ContainsKey(key)) {
-          h.Add(key, key);
+          ht[key] = newArr.Count;
+          newArr.Add(key);
         }
       }
-      ht = h;
+      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[object/*!*/ o] {
+    public bool this[T o] {
       get {
-        Contract.Requires(o != null);
         return ht.ContainsKey(o);
       }
       set {
@@ -147,8 +153,7 @@ namespace Microsoft.Boogie {
     /// <param name="o"></param>
     /// <returns></returns>
     [Pure]
-    public bool Contains(object/*!*/ o) {
-      Contract.Requires(o != null);
+    public bool Contains(T o) {
       if (!this.ht.ContainsKey(o)) {
         return false;
       }
@@ -161,11 +166,10 @@ namespace Microsoft.Boogie {
     /// </summary>
     /// <param name="s"></param>
     /// <returns></returns>
-    public bool ContainsRange(Set/*!*/ s) {
+    public bool ContainsRange(IEnumerable<T> s) {
       Contract.Requires(s != null);
       if (s != this) {
-        foreach (object/*!*/ key in s.ht.Keys) {
-          Contract.Assert(key != null);
+        foreach (T key in s) {
           if (!this.ht.ContainsKey(key)) {
             return false;
           }
@@ -176,7 +180,7 @@ namespace Microsoft.Boogie {
 
     public object/*!*/ Clone() {
       Contract.Ensures(Contract.Result<object>() != null);
-      return new Set((Hashtable/*!*/)cce.NonNull(ht.Clone()));
+      return new GSet<T>(new Dictionary<T,int>(ht), new List<T>(arr));
     }
 
     public virtual int Count {
@@ -185,12 +189,6 @@ namespace Microsoft.Boogie {
       }
     }
 
-    [Pure]
-    public IEnumerator/*!*/ GetEnumerator() {
-      Contract.Ensures(Contract.Result<IEnumerator>() != null);
-      return ht.Keys.GetEnumerator();
-    }
-
     [Pure]
     public override string/*!*/ ToString() {
       Contract.Ensures(Contract.Result<string>() != null);
@@ -211,46 +209,38 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public bool AddAll(IEnumerable/*!*/ objs) {
-      Contract.Requires(objs != null);
-      foreach (object/*!*/ o in objs) {
-        Contract.Assert(o != null);
-        this.Add(o);
-      }
-      return true;
-    }
     //----------------------------- Static Methods ---------------------------------
 
     // Functional Intersect
-    public static Set/*!*/ Intersect(Set/*!*/ a, Set/*!*/ b) {
+    public static GSet<T>/*!*/ Intersect(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
       Contract.Requires(b != null);
       Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<Set>() != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
       //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
-      Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());
+      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
       res.Intersect(b);
       return res;
     }
     // Functional Union
-    public static Set/*!*/ Union(Set/*!*/ a, Set/*!*/ b) {
+    public static GSet<T>/*!*/ Union(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
       Contract.Requires(a != null);
       Contract.Requires(b != null);
-      Contract.Ensures(Contract.Result<Set>() != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
       //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
-      Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());
+      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
       res.AddRange(b);
       return res;
     }
 
     public delegate bool SetFilter(object/*!*/ obj);
 
-    public static Set/*!*/ Filter(Set/*!*/ a, SetFilter/*!*/ filter) {
+    public static GSet<T>/*!*/ Filter(GSet<T>/*!*/ a, Func<T,bool> filter) {
       Contract.Requires(filter != null);
       Contract.Requires(a != null);
-      Contract.Ensures(Contract.Result<Set>() != null);
-      Set inter = new Set();
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      GSet<T> inter = new GSet<T>();
 
-      foreach (object/*!*/ elem in a) {
+      foreach (T elem in a) {
         Contract.Assert(elem != null);
         if (filter(elem)) {
           inter.Add(elem);
@@ -259,8 +249,24 @@ namespace Microsoft.Boogie {
       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);
-- 
cgit v1.2.3