From 5f05e3a1c194dcda48115d7b6a1c5777bd2d5287 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 27 Mar 2013 13:22:57 -0700
Subject: Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more
 useful in compiling assign-such-that statements Added run-time support for
 printing sets, multisets, maps, and sequences

---
 Binaries/DafnyRuntime.cs | 72 +++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 68 insertions(+), 4 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index ac688143..2d17af99 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -7,7 +7,6 @@ namespace Dafny
   public class Set<T>
   {
     Dictionary<T, bool> dict;
-    public Set() { }
     Set(Dictionary<T, bool> d) {
       dict = d;
     }
@@ -34,6 +33,35 @@ namespace Dafny
         return dict.Keys;
       }
     }
+    /// <summary>
+    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same
+    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").
+    /// </summary>
+    public IEnumerable<Set<T>> AllSubsets {
+      get {
+        // Start by putting all set elements into a list
+        var elmts = new List<T>();
+        elmts.AddRange(dict.Keys);
+        var n = elmts.Count;
+        var which = new bool[n];
+        var s = new Set<T>(new Dictionary<T, bool>(0));
+        while (true) {
+          yield return s;
+          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".
+          int i = 0;
+          for (; i < n && which[i]; i++) {
+            which[i] = false;
+            s.dict.Remove(elmts[i]);
+          }
+          if (i == n) {
+            // we have cycled through all the subsets
+            break;
+          }
+          which[i] = true;
+          s.dict.Add(elmts[i], true);
+        }
+      }
+    }
     public bool Equals(Set<T> other) {
       return dict.Count == other.dict.Count && IsSubsetOf(other);
     }
@@ -43,6 +71,15 @@ namespace Dafny
     public override int GetHashCode() {
       return dict.GetHashCode();
     }
+    public override string ToString() {
+      var s = "{";
+      var sep = "";
+      foreach (var t in dict.Keys) {
+        s += sep + t.ToString();
+        sep = ", ";
+      }
+      return s + "}";
+    }
     public bool IsProperSubsetOf(Set<T> other) {
       return dict.Count < other.dict.Count && IsSubsetOf(other);
     }
@@ -136,7 +173,6 @@ namespace Dafny
   public class MultiSet<T>
   {
     Dictionary<T, int> dict;
-    public MultiSet() { }
     MultiSet(Dictionary<T, int> d) {
       dict = d;
     }
@@ -195,6 +231,18 @@ namespace Dafny
     public override int GetHashCode() {
       return dict.GetHashCode();
     }
+    public override string ToString() {
+      var s = "multiset{";
+      var sep = "";
+      foreach (var kv in dict) {
+        var t = kv.Key.ToString();
+        for (int i = 0; i < kv.Value; i++) {
+          s += sep + t.ToString();
+          sep = ", ";
+        }
+      }
+      return s + "}";
+    }
     public bool IsProperSubsetOf(MultiSet<T> other) {
       return !Equals(other) && IsSubsetOf(other);
     }
@@ -293,7 +341,6 @@ namespace Dafny
   public class Map<U, V>
   {
     Dictionary<U, V> dict;
-    public Map() { }
     Map(Dictionary<U, V> d) {
       dict = d;
     }
@@ -342,6 +389,15 @@ namespace Dafny
     public override int GetHashCode() {
       return dict.GetHashCode();
     }
+    public override string ToString() {
+      var s = "map[";
+      var sep = "";
+      foreach (var kv in dict) {
+        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();
+        sep = ", ";
+      }
+      return s + "]";
+    }
     public bool IsDisjointFrom(Map<U, V> other) {
       foreach (U u in dict.Keys) {
         if (other.dict.ContainsKey(u))
@@ -373,7 +429,6 @@ namespace Dafny
   public class Sequence<T>
   {
     T[] elmts;
-    public Sequence() { }
     public Sequence(T[] ee) {
       elmts = ee;
     }
@@ -417,6 +472,15 @@ namespace Dafny
     public override int GetHashCode() {
       return elmts.GetHashCode();
     }
+    public override string ToString() {
+      var s = "[";
+      var sep = "";
+      foreach (var t in elmts) {
+        s += sep + t.ToString();
+        sep = ", ";
+      }
+      return s + "]";
+    }
     bool EqualUntil(Sequence<T> other, int n) {
       for (int i = 0; i < n; i++) {
         if (!elmts[i].Equals(other.elmts[i]))
-- 
cgit v1.2.3