From cfb9f6a3c00d4943a3bc7248a873b643746e0d24 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 16 Apr 2015 11:09:24 -0700
Subject: Change GetHashCode for Set, MultiSet and Map

---
 Binaries/DafnyRuntime.cs     | 20 +++++++++++++++++---
 Test/dafny4/Bug68.dfy        | 34 ++++++++++++++++++++++++++++++++--
 Test/dafny4/Bug68.dfy.expect |  7 +++++--
 3 files changed, 54 insertions(+), 7 deletions(-)

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index a682422a..2a553c81 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -75,7 +75,11 @@ namespace Dafny
       return other is Set<T> && Equals((Set<T>)other);
     }
     public override int GetHashCode() {
-      return dict.GetHashCode();
+      var hashCode = 0;
+      foreach (var t in dict.Keys) {
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ t.GetHashCode();
+      }
+      return hashCode;
     }
     public override string ToString() {
       var s = "{";
@@ -228,7 +232,12 @@ namespace Dafny
       return other is MultiSet<T> && Equals((MultiSet<T>)other);
     }
     public override int GetHashCode() {
-      return dict.GetHashCode();
+      var hashCode = 0;
+      foreach (var kv in dict) {
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Key.GetHashCode();
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Value.GetHashCode();
+      }
+      return hashCode;
     }
     public override string ToString() {
       var s = "multiset{";
@@ -392,7 +401,12 @@ namespace Dafny
       return other is Map<U, V> && Equals((Map<U, V>)other);
     }
     public override int GetHashCode() {
-      return dict.GetHashCode();
+      var hashCode = 0;
+      foreach (var kv in dict) {
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Key.GetHashCode();
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Value.GetHashCode();
+      }
+      return hashCode;
     }
     public override string ToString() {
       var s = "map[";
diff --git a/Test/dafny4/Bug68.dfy b/Test/dafny4/Bug68.dfy
index 2736246d..bfd8c4ad 100644
--- a/Test/dafny4/Bug68.dfy
+++ b/Test/dafny4/Bug68.dfy
@@ -1,9 +1,39 @@
 // RUN: %dafny /compile:3  "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method Main()
+method M1()
+{
+  var m := map [{10, 20} := 33];
+  assert {10, 20} in m; // succeeds 
+  print {10, 20} in m, "\n"; // prints False
+}
+
+method M2()
+{
+  var m := map [(map [1 := 10, 2 := 20]) := 33];
+  assert (map [1 := 10, 2 := 20]) in m; // succeeds 
+  print (map [1 := 10, 2 := 20]) in m, "\n"; // prints False
+}
+
+method M3()
+{
+  var m := map [(multiset{10, 20}) := 33];
+  assert (multiset{10, 20}) in m; // succeeds 
+  print (multiset{10, 20}) in m, "\n"; // prints False
+}
+
+
+method M4()
 {
   var m := map [[10, 20] := 33];
   assert [10, 20] in m; // succeeds 
-  print [10, 20] in m; // prints False
+  print [10, 20] in m, "\n"; // prints False
+}
+
+method Main()
+{
+  M1();
+  M2();
+  M3();
+  M4();
 }
\ No newline at end of file
diff --git a/Test/dafny4/Bug68.dfy.expect b/Test/dafny4/Bug68.dfy.expect
index 4fcef38e..22cf7e4d 100644
--- a/Test/dafny4/Bug68.dfy.expect
+++ b/Test/dafny4/Bug68.dfy.expect
@@ -1,6 +1,9 @@
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
 Program compiled successfully
 Running...
 
-True
\ No newline at end of file
+True
+True
+True
+True
-- 
cgit v1.2.3