Fixing "key not found" error when using set as key (#754)

* Fixing "set key not found in map" error

* [PSym] Add todo for fixing key error when using set as map key

---------

Co-authored-by: Christine Zhou <[email protected]>
Co-authored-by: Aman Goel <[email protected]>

Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs

@@ -37,6 +37,19 @@ private bool IsDirty
             }
         }
 
+        public override int GetHashCode()
+        {
+            if (!IsDirty)
+            {
+                return hashCode;
+            }
+
+            hashCode = ComputeHashCode();
+            IsDirty = false;
+
+            return hashCode;
+        }
+
         public IEnumerator<IPrtValue> GetEnumerator()
         {
             return set.GetEnumerator();

Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java

@@ -68,6 +68,9 @@ private static void setRunArgs() {
   }
 
   private static void createExcludeList() {
+    // TODO: fix key not found error when using set as key
+    excluded.add("../../../Tst/RegressionTests/Integration/Correct/TestMapSet");
+
     // TODO Unsupported: too many choices to throw error if choices more than 10000
     excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq");
     excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet");

Tst/RegressionTests/Integration/Correct/TestMapSet/TestMapSet.p

@@ -0,0 +1,25 @@
+  // Recreating set in map error
+
+machine Main
+{
+  start state Init {
+    entry {
+      ReplicateMapSet();
+    }
+  }
+}
+
+fun ReplicateMapSet()
+{
+  var seqmap: map[seq[int], int]; // Creating example for comparison
+  var mapmap: map[map[int, int], int];
+  var setmap: map[set[int], int]; 
+
+  seqmap[default(seq[int])] = 0;
+  mapmap[default(map[int,int])] = 1;
+  setmap[default(set[int])] = 2;
+
+  print format("seqmap: {0}", seqmap[default(seq[int])]);
+  print format("mapmap: {0}", mapmap[default(map[int,int])]);
+  print format("setmap: {0}", setmap[default(set[int])]);
+}