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.

12 files changed, 153 insertions, 156 deletions

diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs
index 71462c07..31de9a70 100644
--- a/Source/CodeContractsExtender/cce.cs
+++ b/Source/CodeContractsExtender/cce.cs
@@ -57,6 +57,10 @@ public static class cce {
   public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) where T : class {

     return iEnumerator != null;

   }

+  [Pure]

+  public static bool NonNull<T>(HashSet<T> set) where T : class {

+    return set != null && !set.Contains(null);

+  }

   //[Pure]

   //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

   //  return cce.NonNullElements(graph.TopologicalSort());

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 6da85388..802fd390 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -671,7 +671,7 @@ namespace Microsoft.Boogie {
                                           new TypeVariableSeq(),

                                           new Variable[func.Args.Length]);

             int pos = 0;

-            Dictionary<Declaration, bool> parms = new Dictionary<Declaration, bool>();

+            HashSet<Declaration> parms = new HashSet<Declaration>();

             foreach (Expr/*!*/ e in func.Args) {

               Contract.Assert(e != null);

               IdentifierExpr id = e as IdentifierExpr;

@@ -680,11 +680,11 @@ namespace Microsoft.Boogie {
                 return;

               }

               exp.formals[pos++] = id.Decl;

-              if (parms.ContainsKey(id.Decl)) {

+              if (parms.Contains(id.Decl)) {

                 Error(all.tok, "an identifier was used more than once");

                 return;

               }

-              parms[id.Decl] = true;

+              parms.Add(id.Decl);

               if (!all.Dummies.Has(id.Decl)) {

                 Error(all.tok, "identifier was not quantified over");

                 return;

@@ -695,7 +695,7 @@ namespace Microsoft.Boogie {
               return;

             }

 

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

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

             foreach (TypeVariable/*!*/ v in cce.NonNull(func.TypeParameters).FormalTypeParams) {

               Contract.Assert(v != null);

               if (!func.TypeParameters[v].IsVariable) {

@@ -705,11 +705,11 @@ namespace Microsoft.Boogie {
               TypeVariable/*!*/ formal = func.TypeParameters[v].AsVariable;

               Contract.Assert(formal != null);

               exp.TypeParameters.Add(formal);

-              if (typeVars.ContainsKey(formal)) {

+              if (typeVars.Contains(formal)) {

                 Error(all.tok, "an identifier was used more than once");

                 return;

               }

-              typeVars[formal] = true;

+              typeVars.Add(formal);

               if (!all.TypeParameters.Has(formal)) {

                 Error(all.tok, "identifier was not quantified over");

                 return;

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 8c01d8db..9ad1ce22 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -184,7 +184,7 @@ namespace Graphing {
       int n = this.graph.Nodes.Count;

       this.postOrderNumberToNode = new Maybe<Node>[n + 1];

       this.nodeToPostOrderNumber = new Dictionary<Node, int>();

-      Dictionary<Node, bool> visited = new Dictionary<Node, bool>(n);

+      HashSet<Node> visited = new HashSet<Node>();

       int currentNumber = 1;

       Contract.Assume(this.source != null);

       this.PostOrderVisit(this.source, visited, ref currentNumber);

@@ -262,11 +262,11 @@ namespace Graphing {
       }

       return finger1;

     }

-    private void PostOrderVisit(Node/*!*/ n, Dictionary<Node, bool> visited, ref int currentNumber) {

+    private void PostOrderVisit(Node/*!*/ n, HashSet<Node> visited, ref int currentNumber) {

       Contract.Requires(n != null);

-      if (visited.ContainsKey(n))

+      if (visited.Contains(n))

         return;

-      visited[n] = true;

+      visited.Add(n);

       foreach (Node/*!*/ child in this.graph.Successors(n)) {

         Contract.Assert(child != null);

         PostOrderVisit(child, visited, ref currentNumber);

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 627d746c..6e59477b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -240,7 +240,7 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();

     }

 

-    private static Dictionary<string, bool> usedLogNames = new Dictionary<string, bool>();

+    private static HashSet<string> usedLogNames = new HashSet<string>();

 

     private TextWriter OpenOutputFile(string descriptiveName)

     {

@@ -253,10 +253,10 @@ namespace Microsoft.Boogie.SMTLib
 

       lock (usedLogNames) {

         int n = 1;

-        while (usedLogNames.ContainsKey(curFilename)) {

+        while (usedLogNames.Contains(curFilename)) {

           curFilename = filename + "." + n++;

         }

-        usedLogNames[curFilename] = true;

+        usedLogNames.Add(curFilename);

       }

 

       return new StreamWriter(curFilename, false);

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index e669e407..0793c614 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -42,7 +42,7 @@ namespace Microsoft.Boogie.SMTLib
       "int_mod", "int_div", "UOrdering2", "UOrdering3", 

     };

 

-    static Dictionary<string, bool> reservedSmtWords;

+    static HashSet<string> reservedSmtWords;

     static bool[] validIdChar;

     static bool symbolListsInitilized;

 

@@ -52,9 +52,9 @@ namespace Microsoft.Boogie.SMTLib
         // don't move out, c.f. http://en.wikipedia.org/wiki/Double-checked_locking

         if (symbolListsInitilized)

           return;

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

+        reservedSmtWords = new HashSet<string>();

         foreach (var w in reservedSmtWordsList)

-          reservedSmtWords.Add(w, true);

+          reservedSmtWords.Add(w);

         validIdChar = new bool[255];

         for (int i = 0; i < validIdChar.Length; ++i)

           validIdChar[i] = char.IsLetterOrDigit((char)i) || idCharacters.IndexOf((char)i) >= 0;

@@ -82,7 +82,7 @@ namespace Microsoft.Boogie.SMTLib
 

     static string NonKeyword(string s)

     {

-      if (reservedSmtWords.ContainsKey(s) || char.IsDigit(s[0]))

+      if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]))

         s = "q@" + s;

 

       // | and \ are illegal even in quoted identifiers

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 96f16366..c64dbf5e 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -47,14 +47,12 @@ void ObjectInvariant()
     private readonly List<string/*!>!*/> AllDecls = new List<string/*!*/> ();

     private readonly List<string/*!>!*/> IncDecls = new List<string/*!*/> ();

 

-    private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions =

-      new Dictionary<Function/*!*/, bool> ();

-    private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =

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

-

-    private readonly Dictionary<Type/*!*/, bool>/*!*/ KnownTypes = new Dictionary<Type, bool>();

-    private readonly Dictionary<string/*!*/, bool>/*!*/ KnownStoreFunctions = new Dictionary<string, bool>();

-    private readonly Dictionary<string/*!*/, bool>/*!*/ KnownSelectFunctions = new Dictionary<string, bool>();

+    private readonly HashSet<Function/*!*/>/*!*/ KnownFunctions = new HashSet<Function/*!*/>();

+    private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables = new HashSet<VCExprVar/*!*/>();

+

+    private readonly HashSet<Type/*!*/>/*!*/ KnownTypes = new HashSet<Type>();

+    private readonly HashSet<string/*!*/>/*!*/ KnownStoreFunctions = new HashSet<string>();

+    private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();

     private readonly HashSet<string> KnownLBL = new HashSet<string>();

 

 

@@ -107,7 +105,7 @@ void ObjectInvariant()
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);

       else {

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

-        if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

+        if (op != null && !KnownFunctions.Contains(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

           

@@ -121,7 +119,7 @@ void ObjectInvariant()
             string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

             AddDeclaration(decl);

           }

-          KnownFunctions.Add(f, true);

+          KnownFunctions.Add(f);

         } else {

           var lab = node.Op as VCExprLabelOp;

           if (lab != null && !KnownLBL.Contains(lab.label)) {

@@ -137,14 +135,14 @@ void ObjectInvariant()
 

     public override bool Visit(VCExprVar node, bool arg) {

       Contract.Requires(node != null);

-      if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {

+      if (!BoundTermVars.Contains(node) && !KnownVariables.Contains(node)) {

         string printedName = Namer.GetQuotedName(node, node.Name);

         Contract.Assert(printedName!=null);

         RegisterType(node.Type);

         string decl =

           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";

         AddDeclaration(decl);

-        KnownVariables.Add(node, true);

+        KnownVariables.Add(node);

       }

 

       return base.Visit(node, arg);

@@ -164,10 +162,10 @@ void ObjectInvariant()
     private void RegisterType(Type type)

     {

       Contract.Requires(type != null);

-      if (KnownTypes.ContainsKey(type)) return;

+      if (KnownTypes.Contains(type)) return;

 

       if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {

-        KnownTypes.Add(type, true);

+        KnownTypes.Add(type);

         MapType mapType = type.AsMap;

         Contract.Assert(mapType != null);

 

@@ -188,7 +186,7 @@ void ObjectInvariant()
 

       if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {

         AddDeclaration("(declare-sort " + TypeToString(type) + " 0)");

-        KnownTypes.Add(type, true);

+        KnownTypes.Add(type);

         return;

       }

     }

@@ -203,10 +201,10 @@ void ObjectInvariant()
       string name = SimplifyLikeExprLineariser.SelectOpName(node);

       name = Namer.GetQuotedName(name, name);

 

-      if (!KnownSelectFunctions.ContainsKey(name)) {

+      if (!KnownSelectFunctions.Contains(name)) {

         string decl = "(declare-fun " + name + " (" + node.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(node.Type) + ")";

         AddDeclaration(decl);

-        KnownSelectFunctions.Add(name, true);

+        KnownSelectFunctions.Add(name);

       }

     }

 

@@ -220,7 +218,7 @@ void ObjectInvariant()
       string name = SimplifyLikeExprLineariser.StoreOpName(node);

       name = Namer.GetQuotedName(name, name);

 

-      if (!KnownStoreFunctions.ContainsKey(name)) {

+      if (!KnownStoreFunctions.Contains(name)) {

         string decl = "(declare-fun " + name + " (" + node.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(node.Type) + ")";

         AddDeclaration(decl);

 

@@ -228,13 +226,13 @@ void ObjectInvariant()
           var sel = SimplifyLikeExprLineariser.SelectOpName(node);

           sel = Namer.GetQuotedName(sel, sel);

           

-          if (!KnownSelectFunctions.ContainsKey(sel)) {

+          if (!KnownSelectFunctions.Contains(sel)) {

             // need to declare it before reference

             var args = node.SkipEnd(1);

             var ret = node.Last();

             string seldecl = "(declare-fun " + sel + " (" + args.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(ret.Type) + ")";

             AddDeclaration(seldecl);

-            KnownSelectFunctions.Add(sel, true);

+            KnownSelectFunctions.Add(sel);

           }

 

           string ax1 = "(assert (forall (";

@@ -268,7 +266,7 @@ void ObjectInvariant()
           AddDeclaration(ax2);

         }

 

-        KnownStoreFunctions.Add(name, true);

+        KnownStoreFunctions.Add(name);

       }

       //

     }

diff --git a/Source/Provers/TPTP/TypeDeclCollector.cs b/Source/Provers/TPTP/TypeDeclCollector.cs
index beecf660..b7495659 100644
--- a/Source/Provers/TPTP/TypeDeclCollector.cs
+++ b/Source/Provers/TPTP/TypeDeclCollector.cs
@@ -17,19 +17,18 @@ namespace Microsoft.Boogie.TPTP
 

   public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

 

-    private readonly Dictionary<string/*!*/, bool>/*!*/ KnownStoreFunctions = new Dictionary<string, bool>();

-    private readonly Dictionary<string/*!*/, bool>/*!*/ KnownSelectFunctions = new Dictionary<string, bool>();

+    private readonly HashSet<string/*!*/>/*!*/ KnownStoreFunctions = new HashSet<string>();

+    private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();

 

     private readonly UniqueNamer Namer;

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(Namer!=null);

+    void ObjectInvariant() {

+      Contract.Invariant(Namer != null);

       Contract.Invariant(AllDecls != null);

       Contract.Invariant(IncDecls != null);

-      Contract.Invariant(KnownFunctions != null);

-      Contract.Invariant(KnownVariables != null);

-}

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

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

+    }

 

 

     public TypeDeclCollector(UniqueNamer namer) {

@@ -46,10 +45,8 @@ void ObjectInvariant()
     private readonly List<string/*!>!*/> AllDecls = new List<string/*!*/> ();

     private readonly List<string/*!>!*/> IncDecls = new List<string/*!*/> ();

 

-    private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions =

-      new Dictionary<Function/*!*/, bool> ();

-    private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =

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

+    private readonly HashSet<Function/*!*/>/*!*/ KnownFunctions = new HashSet<Function/*!*/>();

+    private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables = new HashSet<VCExprVar/*!*/>();

 

     public List<string/*!>!*/> AllDeclarations { get {

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));

@@ -86,7 +83,7 @@ void ObjectInvariant()
 

       if (node.Op is VCExprStoreOp) {

         string name = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));

-        if (!KnownStoreFunctions.ContainsKey(name)) {

+        if (!KnownStoreFunctions.Contains(name)) {

           var id = KnownStoreFunctions.Count;

 

           if (CommandLineOptions.Clo.MonomorphicArrays) {

@@ -122,7 +119,7 @@ void ObjectInvariant()
             AddDeclaration(ax2);

           }

 

-          KnownStoreFunctions.Add(name, true);

+          KnownStoreFunctions.Add(name);

         }

         //

       }

diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 638acdb0..c9bdfa31 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -18,17 +18,16 @@ using Microsoft.Boogie.VCExprAST;
 namespace Microsoft.Boogie.Z3

 {

   internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {

-    public Dictionary<string/*!*/,bool>/*!*/ Labels = new Dictionary<string/*!*/,bool>();

+    public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(Labels!=null&&cce.NonNullElements(Labels.Keys));

-}

+    void ObjectInvariant() {

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

+    }

 

 

-    public static Dictionary<string/*!*/,bool>/*!*/ FindLabels(VCExpr/*!*/ expr) {

+    public static HashSet<string/*!*/>/*!*/ FindLabels(VCExpr/*!*/ expr) {

       Contract.Requires(expr != null);

-      Contract.Ensures(Contract.Result<Dictionary<string/*!*/,bool>/*!*/>() != null&&cce.NonNullElements(Contract.Result<Dictionary<string/*!*/,bool>/*!*/>().Keys));

+      Contract.Ensures(cce.NonNull(Contract.Result<HashSet<string/*!*/>/*!*/>()));

 

       FindLabelsVisitor visitor = new FindLabelsVisitor();

       visitor.Traverse(expr, true);

@@ -41,7 +40,7 @@ void ObjectInvariant()
       if (nary != null) {

         VCExprLabelOp lab = nary.Op as VCExprLabelOp;

         if (lab != null) {

-          Labels[lab.label] = lab.pos;

+          Labels.Add(lab.label);

         }

       }

       return true;

@@ -94,11 +93,11 @@ void ObjectInvariant()
       Contract.Requires(descriptiveName != null);

       Contract.Requires(vc != null);

       Contract.Requires(handler != null);

-      Dictionary<string/*!*/,bool>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);

+      HashSet<string/*!*/>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);

       Contract.Assert(labels!=null);

       toInspector.WriteLine("PROBLEM " + descriptiveName);

       toInspector.WriteLine("TOKEN BEGIN");

-      foreach (string lab in labels.Keys) {

+      foreach (string lab in labels) {

         Contract.Assert(lab!=null);

         string no = lab.Substring(1);

         Absy absy = handler.Label2Absy(no);

diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index 303a0066..2e695215 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -29,12 +29,12 @@ void ObjectInvariant()
     Contract.Invariant(Namer!=null);

       Contract.Invariant(AllDecls != null);

       Contract.Invariant(IncDecls != null);

-      Contract.Invariant(KnownFunctions != null);

-      Contract.Invariant(KnownVariables != null);

-      Contract.Invariant(KnownTypes != null);

-      Contract.Invariant(KnownBvOps != null);

-      Contract.Invariant(KnownSelectFunctions != null);

-      Contract.Invariant(KnownStoreFunctions != null);

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

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

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

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

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

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

 }

 

 

@@ -46,13 +46,13 @@ void ObjectInvariant()
       this.NativeBv = nativeBv;

       AllDecls = new List<string/*!*/> ();

       IncDecls = new List<string/*!*/> ();

-      KnownFunctions = new Dictionary<Function/*!*/, bool> ();

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

-      KnownTypes = new Dictionary<Type/*!*/, bool> ();

-      KnownBvOps = new Dictionary<string/*!*/, bool> ();

-      

-      KnownStoreFunctions = new Dictionary<string/*!*/, bool>();

-      KnownSelectFunctions = new Dictionary<string/*!*/, bool>();

+      KnownFunctions = new HashSet<Function/*!*/>();

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

+      KnownTypes = new HashSet<Type/*!*/>();

+      KnownBvOps = new HashSet<string/*!*/>();

+

+      KnownStoreFunctions = new HashSet<string/*!*/>();

+      KnownSelectFunctions = new HashSet<string/*!*/>();

     }

 

     internal TypeDeclCollector(UniqueNamer namer, TypeDeclCollector coll) {

@@ -62,13 +62,13 @@ void ObjectInvariant()
       this.NativeBv = coll.NativeBv;

       AllDecls = new List<string/*!*/> (coll.AllDecls);

       IncDecls = new List<string/*!*/> (coll.IncDecls);

-      KnownFunctions = new Dictionary<Function/*!*/, bool> (coll.KnownFunctions);

-      KnownVariables = new Dictionary<VCExprVar/*!*/, bool> (coll.KnownVariables);

-      KnownTypes = new Dictionary<Type/*!*/, bool> (coll.KnownTypes);

-      KnownBvOps = new Dictionary<string/*!*/, bool> (coll.KnownBvOps);

-      

-      KnownStoreFunctions = new Dictionary<string/*!*/, bool> (coll.KnownStoreFunctions);

-      KnownSelectFunctions = new Dictionary<string/*!*/, bool> (coll.KnownSelectFunctions);

+      KnownFunctions = new HashSet<Function/*!*/>(coll.KnownFunctions);

+      KnownVariables = new HashSet<VCExprVar/*!*/>(coll.KnownVariables);

+      KnownTypes = new HashSet<Type/*!*/>(coll.KnownTypes);

+      KnownBvOps = new HashSet<string/*!*/>(coll.KnownBvOps);

+

+      KnownStoreFunctions = new HashSet<string/*!*/>(coll.KnownStoreFunctions);

+      KnownSelectFunctions = new HashSet<string/*!*/>(coll.KnownSelectFunctions);

     }

 

     // not used

@@ -80,17 +80,17 @@ void ObjectInvariant()
     private readonly List<string/*!>!*/> AllDecls;

     private readonly List<string/*!>!*/> IncDecls;

 

-    private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions;

-    private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables;

+    private readonly HashSet<Function/*!*/>/*!*/ KnownFunctions;

+    private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables;

 

     // bitvector types have to be registered as well

-    private readonly IDictionary<Type/*!*/, bool>/*!*/ KnownTypes;

+    private readonly HashSet<Type/*!*/>/*!*/ KnownTypes;

 

     // the names of registered BvConcatOps and BvExtractOps

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

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

 

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

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

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

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

 

     public List<string/*!>!*/> AllDeclarations { get {

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>()));

@@ -131,10 +131,10 @@ void ObjectInvariant()
     private void RegisterType(Type type)

     {

       Contract.Requires(type != null);

-      if (KnownTypes.ContainsKey(type)) return;

+      if (KnownTypes.Contains(type)) return;

 

       if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {

-        KnownTypes.Add(type, true);

+        KnownTypes.Add(type);

         string declString = "";

         MapType mapType = type.AsMap;

         Contract.Assert(mapType != null);

@@ -173,7 +173,7 @@ void ObjectInvariant()
         AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "

                        + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");

 

-        KnownTypes.Add(type, true);

+        KnownTypes.Add(type);

         return;

       }

 

@@ -182,7 +182,7 @@ void ObjectInvariant()
 

       if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {

         AddDeclaration("(DEFTYPE " + TypeToString(type) + ")");

-        KnownTypes.Add(type, true);

+        KnownTypes.Add(type);

         return;

       }

 

@@ -201,13 +201,13 @@ void ObjectInvariant()
           RegisterType(node.Type);

 

           string name = SimplifyLikeExprLineariser.BvConcatOpName(node);

-          if (!KnownBvOps.ContainsKey(name)) {

+          if (!KnownBvOps.Contains(name)) {

             AddDeclaration("(DEFOP " + name +

                            " " + TypeToString(node[0].Type) +

                            " " + TypeToString(node[1].Type) +

                            " " + TypeToString(node.Type) +

                            " :BUILTIN concat)");

-            KnownBvOps.Add(name, true);

+            KnownBvOps.Add(name);

           }

         }

         //

@@ -220,20 +220,20 @@ void ObjectInvariant()
           VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;

           Contract.Assert(op!=null);

           string name = SimplifyLikeExprLineariser.BvExtractOpName(node);

-          if (!KnownBvOps.ContainsKey(name)) {

+          if (!KnownBvOps.Contains(name)) {

             AddDeclaration("(DEFOP " + name +

                            " " + TypeToString(node[0].Type) +

                            " " + TypeToString(node.Type) + 

                            " :BUILTIN extract " +

                            (op.End - 1) + " " + op.Start + ")");

-            KnownBvOps.Add(name, true);

+            KnownBvOps.Add(name);

           }

         }

         //

       } else if (node.Op is VCExprStoreOp) {

         RegisterType(node.Type);        // this is the map type, registering it should register also the index and value types

         string name = SimplifyLikeExprLineariser.StoreOpName(node);

-        if (!KnownStoreFunctions.ContainsKey(name)) {

+        if (!KnownStoreFunctions.Contains(name)) {

           string decl = "(DEFOP " + name;

 

           foreach (VCExpr ch in node) {

@@ -249,14 +249,14 @@ void ObjectInvariant()
           if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {

             var sel = SimplifyLikeExprLineariser.SelectOpName(node);

 

-            if (!KnownSelectFunctions.ContainsKey(name)) {

+            if (!KnownSelectFunctions.Contains(name)) {

               // need to declare it before reference

               string seldecl = "(DEFOP " + sel;

               foreach (VCExpr ch in node) {

                 seldecl += " " + TypeToString(ch.Type);

               }

               AddDeclaration(seldecl + ")");

-              KnownSelectFunctions.Add(name, true);

+              KnownSelectFunctions.Add(name);

             }

 

             var eq = "EQ";

@@ -293,14 +293,14 @@ void ObjectInvariant()
             AddDeclaration(ax2);

           }

           

-          KnownStoreFunctions.Add(name, true);

+          KnownStoreFunctions.Add(name);

         }

         //

       } else if (node.Op is VCExprSelectOp) {

         //

         RegisterType(node[0].Type);

         string name = SimplifyLikeExprLineariser.SelectOpName(node);

-        if (!KnownSelectFunctions.ContainsKey(name)) {

+        if (!KnownSelectFunctions.Contains(name)) {

           string decl = "(DEFOP " + name;

 

           foreach (VCExpr ch in node) {

@@ -312,13 +312,13 @@ void ObjectInvariant()
             decl += " :BUILTIN select";

           decl += ")";

           AddDeclaration(decl);

-          KnownSelectFunctions.Add(name, true);

+          KnownSelectFunctions.Add(name);

         }

         //

       } else {

         //

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

-        if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

+        if (op != null && !KnownFunctions.Contains(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f!=null);

           string printedName = Namer.GetName(f, f.Name);

@@ -344,7 +344,7 @@ void ObjectInvariant()
           decl += ")";

         

           AddDeclaration(decl);

-          KnownFunctions.Add(f, true);

+          KnownFunctions.Add(f);

         }

         //

       }

@@ -366,7 +366,7 @@ void ObjectInvariant()
 

     public override bool Visit(VCExprVar node, bool arg) {

       Contract.Requires(node != null);

-      if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {

+      if (!BoundTermVars.Contains(node) && !KnownVariables.Contains(node)) {

         RegisterType(node.Type);

         string printedName = Namer.GetName(node, node.Name);

         Contract.Assert(printedName!=null);

@@ -374,7 +374,7 @@ void ObjectInvariant()
           "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)

           + " " + TypeToString(node.Type) + ")";

         AddDeclaration(decl);

-        KnownVariables.Add(node, true);

+        KnownVariables.Add(node);

       }

 

       return base.Visit(node, arg);

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;

       }

     }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 1062767c..8a9e13ff 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -284,7 +284,7 @@ namespace VC {
         Contract.Invariant(initial != null);

         Contract.Invariant(program != null);

         Contract.Invariant(cce.NonNullDictionaryAndValues(copies));

-        Contract.Invariant(visited != null);

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

         Contract.Invariant(callback != null);

       }

 

@@ -294,7 +294,7 @@ namespace VC {
       Program program;

       int id;

       Dictionary<Block, Block> copies = new Dictionary<Block, Block>();

-      Dictionary<Block, bool> visited = new Dictionary<Block, bool>();

+      HashSet<Block> visited = new HashSet<Block>();

       VerifierCallback callback;

 

       internal SmokeTester(VCGen par, Implementation i, Program prog, VerifierCallback callback) {

@@ -548,9 +548,9 @@ namespace VC {
       void DFS(Block cur) {

         Contract.Requires(cur != null);

         Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

-        if (visited.ContainsKey(cur))

+        if (visited.Contains(cur))

           return;

-        visited[cur] = true;

+        visited.Add(cur);

 

         CmdSeq seq = new CmdSeq();

         foreach (Cmd cmd_ in cur.Cmds) {

@@ -668,13 +668,13 @@ namespace VC {
         public double incomming_paths;

         public List<Block>/*!>!*/ virtual_successors = new List<Block>();

         public List<Block>/*!>!*/ virtual_predecesors = new List<Block>();

-        public Dictionary<Block, bool> reachable_blocks;

+        public HashSet<Block> reachable_blocks;

         public readonly Block block;

         [ContractInvariantMethod]

         void ObjectInvariant() {

           Contract.Invariant(cce.NonNullElements(virtual_successors));

           Contract.Invariant(cce.NonNullElements(virtual_predecesors));

-          Contract.Invariant(cce.NonNullElements(reachable_blocks.Keys));

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

           Contract.Invariant(block != null);

         }

 

@@ -696,8 +696,8 @@ namespace VC {
         Contract.Invariant(parent != null);

         Contract.Invariant(impl != null);

         Contract.Invariant(copies != null);

-        Contract.Invariant(protected_from_assert_to_assume != null);

-        Contract.Invariant(keep_at_all != null);

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

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

       }

 

 

@@ -724,8 +724,8 @@ namespace VC {
       double slice_initial_limit;

       double slice_limit;

       bool slice_pos;

-      Dictionary<Block/*!*/, bool>/*!*/ protected_from_assert_to_assume = new Dictionary<Block/*!*/, bool>();

-      Dictionary<Block/*!*/, bool>/*!*/ keep_at_all = new Dictionary<Block/*!*/, bool>();

+      HashSet<Block/*!*/>/*!*/ protected_from_assert_to_assume = new HashSet<Block/*!*/>();

+      HashSet<Block/*!*/>/*!*/ keep_at_all = new HashSet<Block/*!*/>();

 

       // async interface

       private Checker checker;

@@ -861,21 +861,21 @@ namespace VC {
         }

       }

 

-      Dictionary<Block/*!*/, bool>/*!*/ ComputeReachableNodes(Block/*!*/ b) {

+      HashSet<Block/*!*/>/*!*/ ComputeReachableNodes(Block/*!*/ b) {

         Contract.Requires(b != null);

-        Contract.Ensures(Contract.Result<Dictionary<Block, bool>>() != null);

+        Contract.Ensures(cce.NonNull(Contract.Result<HashSet<Block/*!*/>>()));

         BlockStats s = GetBlockStats(b);

         if (s.reachable_blocks != null) {

           return s.reachable_blocks;

         }

-        Dictionary<Block/*!*/, bool> blocks = new Dictionary<Block/*!*/, bool>();

+        HashSet<Block/*!*/> blocks = new HashSet<Block/*!*/>();

         s.reachable_blocks = blocks;

-        blocks[b] = true;

+        blocks.Add(b);

         foreach (Block/*!*/ succ in Exits(b)) {

           Contract.Assert(succ != null);

-          foreach (Block r in ComputeReachableNodes(succ).Keys) {

+          foreach (Block r in ComputeReachableNodes(succ)) {

             Contract.Assert(r != null);

-            blocks[r] = true;

+            blocks.Add(r);

           }

         }

         return blocks;

@@ -979,7 +979,7 @@ namespace VC {
         if (s.incomming_paths < 0.0) {

           int count = 0;

           s.incomming_paths = 0.0;

-          if (!keep_at_all.ContainsKey(s.block))

+          if (!keep_at_all.Contains(s.block))

             return;

           foreach (Block b in s.virtual_predecesors) {

             Contract.Assert(b != null);

@@ -999,9 +999,9 @@ namespace VC {
 

       void ComputeBlockSetsHelper(Block b, bool allow_small) {

         Contract.Requires(b != null);

-        if (keep_at_all.ContainsKey(b))

+        if (keep_at_all.Contains(b))

           return;

-        keep_at_all[b] = true;

+        keep_at_all.Add(b);

 

         if (allow_small) {

           foreach (Block ch in Exits(b)) {

@@ -1030,18 +1030,18 @@ namespace VC {
         if (assert_to_assume) {

           foreach (Block b in allow_small ? blocks : big_blocks) {

             Contract.Assert(b != null);

-            if (ComputeReachableNodes(b).ContainsKey(cce.NonNull(split_block))) {

-              keep_at_all[b] = true;

+            if (ComputeReachableNodes(b).Contains(cce.NonNull(split_block))) {

+              keep_at_all.Add(b);

             }

           }

 

           foreach (Block b in assumized_branches) {

             Contract.Assert(b != null);

-            foreach (Block r in ComputeReachableNodes(b).Keys) {

+            foreach (Block r in ComputeReachableNodes(b)) {

               Contract.Assert(r != null);

               if (allow_small || GetBlockStats(r).big_block) {

-                keep_at_all[r] = true;

-                protected_from_assert_to_assume[r] = true;

+                keep_at_all.Add(r);

+                protected_from_assert_to_assume.Add(r);

               }

             }

           }

@@ -1052,7 +1052,7 @@ namespace VC {
 

       bool ShouldAssumize(Block b) {

         Contract.Requires(b != null);

-        return assert_to_assume && !protected_from_assert_to_assume.ContainsKey(b);

+        return assert_to_assume && !protected_from_assert_to_assume.Contains(b);

       }

 

       double DoComputeScore(bool aa) {

@@ -1069,7 +1069,7 @@ namespace VC {
         double cost = 0.0;

         foreach (Block b in big_blocks) {

           Contract.Assert(b != null);

-          if (keep_at_all.ContainsKey(b)) {

+          if (keep_at_all.Contains(b)) {

             BlockStats s = GetBlockStats(b);

             UpdateIncommingPaths(s);

             double local = s.assertion_cost;

@@ -1140,10 +1140,10 @@ namespace VC {
           foreach (Block ch in cce.NonNull(gt.labelTargets)) {

             Contract.Assert(ch != null);

             Contract.Assert(doing_slice ||

-                   (assert_to_assume || (keep_at_all.ContainsKey(ch) || assumized_branches.Contains(ch))));

+                   (assert_to_assume || (keep_at_all.Contains(ch) || assumized_branches.Contains(ch))));

             if (doing_slice ||

                 ((b != split_block || assumized_branches.Contains(ch) == assert_to_assume) &&

-                 keep_at_all.ContainsKey(ch))) {

+                 keep_at_all.Contains(ch))) {

               newGoto.AddTarget(CloneBlock(ch));

             }

             pos++;

@@ -1304,7 +1304,7 @@ namespace VC {
             ss.Add(s0.blocks[0]);

             ss.Add(s1.blocks[0]);

             try {

-              best.SoundnessCheck(new Dictionary<PureCollections.Tuple, bool>(), best.blocks[0], ss);

+              best.SoundnessCheck(new HashSet<PureCollections.Tuple>(), best.blocks[0], ss);

             } catch (System.Exception e) {

               Console.WriteLine(e);

               best.DumpDot(-1);

@@ -1461,8 +1461,8 @@ namespace VC {
         checker.BeginCheck(desc, vc, reporter);

       }

 

-      private void SoundnessCheck(Dictionary<PureCollections.Tuple/*!*/, bool>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {

-        Contract.Requires(cache != null);

+      private void SoundnessCheck(HashSet<PureCollections.Tuple/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {

+        Contract.Requires(cce.NonNull(cache));

         Contract.Requires(orig != null);

         Contract.Requires(copies != null);

         {

@@ -1473,10 +1473,10 @@ namespace VC {
             Contract.Assert(b != null);

             t[i++] = b;

           }

-          if (cache.ContainsKey(t)) {

+          if (cache.Contains(t)) {

             return;

           }

-          cache[t] = true;

+          cache.Add(t);

         }

 

         for (int i = 0; i < orig.Cmds.Length; ++i) {

@@ -3997,7 +3997,7 @@ namespace VC {
 

         // recursively call this method on each successor

         // merge result into a *set* of blocks

-        Dictionary<Block,bool> mergedSuccessors = new Dictionary<Block,bool>();

+        HashSet<Block> mergedSuccessors = new HashSet<Block>();

         int m = 0;  // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null

         foreach (Block dest in gtc.labelTargets){Contract.Assert(dest != null);

           Block renameInfo;

@@ -4009,15 +4009,15 @@ namespace VC {
             renameInfoForStartBlock = null;

           }

           foreach (Block successor in ys){

-            if (!mergedSuccessors.ContainsKey(successor))

-              mergedSuccessors.Add(successor,true);

+            if (!mergedSuccessors.Contains(successor))

+              mergedSuccessors.Add(successor);

           }

           m++;

         }

         b.TraversingStatus = Block.VisitState.AlreadyVisited;

 

         BlockSeq setOfSuccessors = new BlockSeq();

-        foreach (Block d in mergedSuccessors.Keys)

+        foreach (Block d in mergedSuccessors)

           setOfSuccessors.Add(d);

         if (b.Cmds.Length == 0 && !startNode) {

           // b is about to become extinct