Replaced all dictionaries that mapped to bool (i.e., were being used to implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.

2 files changed, 12 insertions, 13 deletions

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index f811461d..a78a6103 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -26,7 +26,7 @@ namespace Microsoft.Boogie.VCExprAST {
       GlobalNames = new Dictionary<Object, string>();

       LocalNames = TEHelperFuns.ToList(new Dictionary<Object/*!*/, string/*!*/>()

                                          as IDictionary<Object/*!*/, string/*!*/>);

-      UsedNames = new Dictionary<string, bool>();

+      UsedNames = new HashSet<string>();

       CurrentCounters = new Dictionary<string, int>();

       GlobalPlusLocalNames = new Dictionary<Object, string>();

     }

@@ -43,7 +43,7 @@ namespace Microsoft.Boogie.VCExprAST {
       foreach (IDictionary<Object/*!*/, string/*!*/>/*!*/ d in namer.LocalNames)

         localNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));

 

-      UsedNames = new Dictionary<string, bool>(namer.UsedNames);

+      UsedNames = new HashSet<string>(namer.UsedNames);

       CurrentCounters = new Dictionary<string, int>(namer.CurrentCounters);

       GlobalPlusLocalNames = new Dictionary<Object, string>(namer.GlobalPlusLocalNames);

     }

@@ -68,10 +68,10 @@ namespace Microsoft.Boogie.VCExprAST {
 

     // dictionary of all names that have already been used

     // (locally or globally)

-    private readonly IDictionary<string/*!*/, bool/*!*/>/*!*/ UsedNames;

+    private readonly HashSet<string/*!*/>/*!*/ UsedNames;

     [ContractInvariantMethod]

     void UsedNamesInvariantMethod() {

-      Contract.Invariant(UsedNames != null);

+      Contract.Invariant(cce.NonNull(UsedNames));

     }

     private readonly IDictionary<string/*!*/, int/*!*/>/*!*/ CurrentCounters;

     [ContractInvariantMethod]

@@ -111,13 +111,12 @@ namespace Microsoft.Boogie.VCExprAST {
         counter = 0;

       }

 

-      bool dummy;

-      while (UsedNames.TryGetValue(candidate, out dummy)) {

+      while (UsedNames.Contains(candidate)) {

         candidate = baseName + Spacer + counter;

         counter = counter + 1;

       }

 

-      UsedNames.Add(candidate, true);

+      UsedNames.Add(candidate);

       CurrentCounters[baseName] = counter;

       GlobalPlusLocalNames[thingie] = candidate;

       return candidate;

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 3d407150..1a29bbeb 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -1076,16 +1076,16 @@ namespace Microsoft.Boogie.VCExprAST {
     public IEnumerable<VCExprVar/*!*/>/*!*/ TermDomain {

       get {

         Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExprVar>>()));

-        Dictionary<VCExprVar/*!*/, bool>/*!*/ domain = new Dictionary<VCExprVar/*!*/, bool>();

+        HashSet<VCExprVar/*!*/>/*!*/ domain = new HashSet<VCExprVar/*!*/>();

         foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts) {

           Contract.Assert(dict != null);

           foreach (VCExprVar/*!*/ var in dict.Keys) {

             Contract.Assert(var != null);

             if (!var.Equals(this[var]))

-              domain.Add(var, true);

+              domain.Add(var);

           }

         }

-        return domain.Keys;

+        return domain;

       }

     }

 

@@ -1093,16 +1093,16 @@ namespace Microsoft.Boogie.VCExprAST {
     public IEnumerable<TypeVariable/*!*/>/*!*/ TypeDomain {

       get {

         Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<TypeVariable>>()));

-        Dictionary<TypeVariable/*!*/, bool>/*!*/ domain = new Dictionary<TypeVariable/*!*/, bool>();

+        HashSet<TypeVariable/*!*/>/*!*/ domain = new HashSet<TypeVariable/*!*/>();

         foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {

           Contract.Assert(dict != null);

           foreach (TypeVariable/*!*/ var in dict.Keys) {

             Contract.Assert(var != null);

             if (!var.Equals(this[var]))

-              domain.Add(var, true);

+              domain.Add(var);

           }

         }

-        return domain.Keys;

+        return domain;

       }

     }