From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Source/Basetypes/Set.ssc | 282 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 282 insertions(+)
 create mode 100644 Source/Basetypes/Set.ssc

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

diff --git a/Source/Basetypes/Set.ssc b/Source/Basetypes/Set.ssc
new file mode 100644
index 00000000..221a9ad4
--- /dev/null
+++ b/Source/Basetypes/Set.ssc
@@ -0,0 +1,282 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie
+{
+    using System;
+    using System.IO;
+    using System.Collections;
+    using Microsoft.Contracts;
+
+    /// <summary>
+    /// A class representing a mathematical set.
+    /// </summary>
+    public class Set : ICloneable, IEnumerable 
+    {
+        /*[Own]*/ Hashtable! ht;
+
+        public Set() 
+        {
+            ht = new Hashtable();
+            base();
+        }
+
+        private Set(Hashtable! ht) 
+        {
+            this.ht = ht;
+            base();
+        }
+
+        public Set(int capacity) 
+        {
+            ht = new Hashtable(capacity);
+            base();
+        }
+        
+        
+        public readonly static Set! Empty = new Set();
+
+        public void Clear() 
+        {
+            ht.Clear();
+        }
+
+        /// <summary>
+        /// This method idempotently adds "o" to the set.
+        /// In notation:
+        ///   this.SetElements =  this.SetElements_old \union {o};
+        /// </summary>
+        public void Add(object! o) 
+        {
+            ht[o] = o;
+        }
+
+        /// <summary>
+        /// this.SetElements =  this.SetElements_old \union s.SetElements;
+        /// </summary>
+        public void AddRange(Set! s) 
+        {
+            foreach (object! o in s) 
+            {
+                Add(o);
+            }
+        }
+
+        /// <summary>
+        /// this.SetElements =  this.SetElements_old \setminus {o};
+        /// </summary>
+        public void Remove(object! o) 
+        {
+            ht.Remove(o);
+        }
+
+        /// <summary>
+        /// this.SetElements =  this.SetElements_old \setminus s.SetElements;
+        /// </summary>
+        public void RemoveRange(Set! s) 
+        {
+            if (s == this) 
+            {
+                ht.Clear();
+            } 
+            else 
+            {
+                foreach (object! o in s) 
+                {
+                    ht.Remove(o);
+                }
+            }
+        }
+        
+        /// <summary>
+        /// Returns an arbitrary element from the set.
+        /// </summary>
+        public object! Choose()
+          requires Count > 0;
+        {
+            IEnumerator iter = GetEnumerator();
+            iter.MoveNext();
+            return (!)iter.Current;
+        }
+        
+        /// <summary>
+        /// Picks an arbitrary element from the set, removes it, and returns it.
+        /// </summary>
+        public object! Take()
+          requires Count > 0;
+          ensures Count == old(Count) - 1;
+        {
+            object r = Choose();
+            Remove(r);
+            return r;
+        }
+
+        public void Intersect(Set! s) 
+        {
+            Hashtable h = new Hashtable(ht.Count);
+            foreach (object! key in ht.Keys) 
+            {
+                if (s.ht.ContainsKey(key)) 
+                {
+                    h.Add(key, key);
+                }
+            }
+            ht = h;
+        }
+        
+        /// <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] 
+        {
+            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(object! o) 
+        {
+          if (!this.ht.ContainsKey(o)) 
+          {
+            return false;
+          }            
+          return true;
+        }
+
+        /// <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(Set! s) 
+        {
+            if (s != this) 
+            {
+                foreach (object! key in s.ht.Keys) 
+                {
+                    if (!this.ht.ContainsKey(key)) 
+                    {
+                        return false;
+                    }
+                }
+            }
+            return true;
+        }
+
+        public object! Clone() 
+        {
+            return new Set((Hashtable!)ht.Clone());
+        }
+
+        public virtual int Count 
+        {
+            [Pure][Reads(ReadsAttribute.Reads.Owned)] get 
+            {
+                return ht.Count;
+            }
+        }
+
+        [Pure]
+        public IEnumerator! GetEnumerator() 
+        {
+            return ht.Keys.GetEnumerator();
+        }
+
+        [Pure][Reads(ReadsAttribute.Reads.Owned)]
+        public override string! ToString() 
+        {
+            string s = null;
+            foreach (object! key in ht.Keys) 
+            {
+                if (s == null) 
+                {
+                    s = "{";
+                } 
+                else 
+                {
+                    s += ", ";
+                }
+                s += key.ToString();
+            }
+            if (s == null) 
+            {
+                return "{}";
+            } 
+            else 
+            {
+                return s + "}";
+            }
+        }
+        
+         public bool AddAll(IEnumerable! objs){
+          foreach (object! o in objs){
+            this.Add(o);
+          }
+          return true;
+        }
+       //----------------------------- Static Methods ---------------------------------
+        
+        // Functional Intersect
+        public static Set! Intersect(Set! a, Set! b) 
+        //  ensures Forall{ object x in result; a[x] && b[x] };
+        {
+            Set! res = (Set!) a.Clone();
+            res.Intersect(b);
+            return res;
+        }
+        // Functional Union
+        public static Set! Union(Set! a, Set! b) 
+        //  ensures Forall{ object x in result; a[x] || b[x] };
+        {
+            Set! res = (Set!) a.Clone();
+            res.AddRange(b);
+            return res;
+        }
+ 
+       public delegate bool SetFilter(object! obj);
+
+       public static Set! Filter(Set! a, SetFilter! filter) 
+       {
+         Set inter = new Set();
+
+         foreach(object! elem in a) 
+         {
+           if (filter(elem))
+           {
+             inter.Add(elem);
+           }
+         }	
+         return inter;
+       }
+
+  }
+ 
+   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