diff options
| author |  qunyanm <unknown> | 2015-04-16 11:09:24 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-16 11:09:24 -0700 |
| commit | cfb9f6a3c00d4943a3bc7248a873b643746e0d24 (patch) | |
| tree | 3cbb25ca94f8678c35d6a916c3647ee7e8beefcf | |
| parent | d95b2c8dd46bb52c6c84f2b764d3e6211b403346 (diff) | |
Change GetHashCode for Set, MultiSet and Map
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 20 | ||||
| -rw-r--r-- | Test/dafny4/Bug68.dfy | 34 | ||||
| -rw-r--r-- | 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 |