Changed Has method of PureSequence to Contains to make refactoring easier.

10 files changed, 36 insertions, 36 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index e7c1fb77..6e131606 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3326,7 +3326,7 @@ namespace Microsoft.Boogie {
       for (int i = 0; i < s1.card; i++) {

         TypeVariable/*!*/ next = s1[i];

         Contract.Assert(next != null);

-        if (!this.Has(next))

+        if (!this.Contains(next))

           this.Add(next);

       }

     }

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 47f5505e..15a9fff7 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2176,7 +2176,7 @@ namespace Microsoft.Boogie {
         newBlockBody.Add(assign);

 

         // fra

-        if (!havocVarExprs.Has(f))

+        if (!havocVarExprs.Contains(f))

           havocVarExprs.Add(f);

       }

       #endregion

@@ -2200,7 +2200,7 @@ namespace Microsoft.Boogie {
         IdentifierExpr ie = new IdentifierExpr(cout.tok, cout);

         substMap.Add(param, ie);

 

-        if (!havocVarExprs.Has(ie))

+        if (!havocVarExprs.Contains(ie))

           havocVarExprs.Add(ie);

       }

       // add the where clauses, now that we have the entire substitution map

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 92f255f3..cca59323 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -197,7 +197,7 @@ namespace Microsoft.Boogie {
       TypeVariableSeq/*!*/ unmentionedParameters = new TypeVariableSeq();

       foreach (TypeVariable/*!*/ var in TypeParameters) {

         Contract.Assert(var != null);

-        if (!dummyParameters.Has(var))

+        if (!dummyParameters.Contains(var))

           unmentionedParameters.Add(var);

       }

       return unmentionedParameters;

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 81d44756..20ff8446 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -467,7 +467,7 @@ namespace Microsoft.Boogie {
         Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type);

         // if the type variables to be matched occur in the actual

         // argument types, something has gone very wrong

-        Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Has(typeParams[index])));

+        Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Contains(typeParams[index])));

 

         if (!formal.Unify(actual)) {

           Contract.Assume(tc != null);  // caller expected no errors

@@ -484,7 +484,7 @@ namespace Microsoft.Boogie {
           Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type);

           // if the type variables to be matched occur in the actual

           // argument types, something has gone very wrong

-          Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !actual.FreeVariables.Has(typeParams[var])));

+          Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !actual.FreeVariables.Contains(typeParams[var])));

 

           if (!formal.Unify(actual)) {

             Contract.Assume(tc != null);  // caller expected no errors

@@ -560,7 +560,7 @@ namespace Microsoft.Boogie {
         // in case we have been able to substitute all type parameters,

         // we can still return the result type and hope that the

         // type checking proceeds in a meaningful manner

-        if (Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Has(typeParams[index])))

+        if (Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Contains(typeParams[index])))

           return actualResults;

         else

           // otherwise there is no point in returning the result type,

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

       }

 

-      Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Has(typeParams[index])));

+      Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Contains(typeParams[index])));

       return actualResults;

     }

 

@@ -595,7 +595,7 @@ namespace Microsoft.Boogie {
       // all type parameters have to be substituted with concrete types

       TypeVariableSeq/*!*/ resFreeVars = res.FreeVariables;

       Contract.Assert(resFreeVars != null);

-      Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !resFreeVars.Has(typeParams[var])));

+      Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !resFreeVars.Contains(typeParams[var])));

       return res;

     }

 

@@ -656,7 +656,7 @@ namespace Microsoft.Boogie {
         Type actual = actualArgs[i];

         // if the type variables to be matched occur in the actual

         // argument types, something has gone very wrong

-        Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Has(typeParams[index])));

+        Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Contains(typeParams[index])));

 

         if (!formal.Unify(actual)) {

           Contract.Assume(false);  // caller expected no errors

@@ -699,7 +699,7 @@ namespace Microsoft.Boogie {
       TypeVariableSeq sortedTypeParams = new TypeVariableSeq();

       foreach (TypeVariable/*!*/ var in freeVarsInUse) {

         Contract.Assert(var != null);

-        if (typeParams.Has(var)) {

+        if (typeParams.Contains(var)) {

           sortedTypeParams.Add(var);

         }

       }

@@ -734,9 +734,9 @@ namespace Microsoft.Boogie {
         Contract.Assert(var != null);

         if (rc.LookUpTypeBinder(var.Name) == var)  // avoid to complain twice about variables that are bound multiple times

         {

-          if (freeVarsInArgs.Has(var)) {

+          if (freeVarsInArgs.Contains(var)) {

             // cool

-          } else if (moFreeVarsInArgs != null && moFreeVarsInArgs.Has(var)) {

+          } else if (moFreeVarsInArgs != null && moFreeVarsInArgs.Contains(var)) {

             someTypeParamsAppearOnlyAmongMo = true;

           } else {

             rc.Error(resolutionSubject,

@@ -802,7 +802,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(that != null);

       Contract.Requires(unifiableVariables != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(unifier));

-      Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Has(key)));

+      Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Contains(key)));

       Contract.Requires(IsIdempotent(unifier));

       throw new NotImplementedException();

     }

@@ -1484,7 +1484,7 @@ Contract.Requires(that != null);
       if (this.Equals(that))

         return true;

 

-      if (unifiableVariables.Has(this)) {

+      if (unifiableVariables.Contains(this)) {

         Type previousSubst;

         unifier.TryGetValue(this, out previousSubst);

         if (previousSubst == null) {

@@ -1501,7 +1501,7 @@ Contract.Requires(that != null);
       TypeVariable tv = that as TypeVariable;

 

       return tv != null &&

-             unifiableVariables.Has(tv) &&

+             unifiableVariables.Contains(tv) &&

              that.Unify(this, unifiableVariables, unifier);

     }

 

@@ -1520,7 +1520,7 @@ Contract.Requires(that != null);
       Type/*!*/ substSubst = newSubst.Substitute(oldSolution);

       Contract.Assert(substSubst != null);

       // occurs check

-      if (substSubst.FreeVariables.Has(this))

+      if (substSubst.FreeVariables.Contains(this))

         return false;

       newMapping.Add(this, substSubst);

 

@@ -2141,7 +2141,7 @@ Contract.Requires(that != null);
 

       TypeVariable tv = that as TypeVariable;

 

-      if (tv != null && unifiableVariables.Has(tv))

+      if (tv != null && unifiableVariables.Contains(tv))

         return that.Unify(this, unifiableVariables, result);

 

       if (object.ReferenceEquals(this, that)) {

@@ -2219,7 +2219,7 @@ Contract.Requires(that != null);
         // of the substituted variables (otherwise, we are in big trouble)

         Contract.Assert(Contract.ForAll(constraints, c =>

                Contract.ForAll(subst.Keys, var =>

-                      !c.T0.FreeVariables.Has(var) && !c.T1.FreeVariables.Has(var))));

+                      !c.T0.FreeVariables.Contains(var) && !c.T1.FreeVariables.Contains(var))));

       }

       return base.Substitute(subst);

     }

@@ -2455,7 +2455,7 @@ Contract.Requires(that != null);
 

       TypeVariable tv = that as TypeVariable;

 

-      if (tv != null && unifiableVariables.Has(tv))

+      if (tv != null && unifiableVariables.Contains(tv))

         return that.Unify(this, unifiableVariables, result);

 

       if (object.ReferenceEquals(this, that)) {

@@ -2500,8 +2500,8 @@ Contract.Requires(that != null);
         // of the substituted variables (otherwise, we are in big trouble)

         Contract.Assert(Contract.ForAll(constraints, c =>

                Contract.ForAll(subst.Keys, var =>

-               Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Has(var)) &&

-                     !c.Result.FreeVariables.Has(var))));

+               Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Contains(var)) &&

+                     !c.Result.FreeVariables.Contains(var))));

       }

       return base.Substitute(subst);

     }

@@ -3096,7 +3096,7 @@ Contract.Requires(that != null);
         new Dictionary<TypeVariable/*!*/, TypeVariable/*!*/>();

       foreach (KeyValuePair<TypeVariable/*!*/, TypeVariable/*!*/> p in varMap) {

         Contract.Assert(cce.NonNullElements(p));

-        if (!TypeParameters.Has(p.Key))

+        if (!TypeParameters.Contains(p.Key))

           newVarMap.Add(p);

       }

 

@@ -3231,12 +3231,12 @@ Contract.Requires(that != null);
         // non-substituted types ...

         TypeVariableSeq freeVars = this.FreeVariables;

         foreach (TypeVariable fr in freshies)

-          if (freeVars.Has(fr)) {

+          if (freeVars.Contains(fr)) {

             return false;

           }  // fresh variable escaped

         freeVars = thatMapType.FreeVariables;

         foreach (TypeVariable fr in freshies)

-          if (freeVars.Has(fr)) {

+          if (freeVars.Contains(fr)) {

             return false;

           }  // fresh variable escaped

 

@@ -3245,7 +3245,7 @@ Contract.Requires(that != null);
           Contract.Assert(cce.NonNullElements(pair));

           freeVars = pair.Value.FreeVariables;

           foreach (TypeVariable fr in freshies)

-            if (freeVars.Has(fr)) {

+            if (freeVars.Contains(fr)) {

               return false;

             }  // fresh variable escaped          

         }

@@ -3317,7 +3317,7 @@ Contract.Assert(var != null);
     private bool collisionsPossible(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {

       Contract.Requires(cce.NonNullDictionaryAndValues(subst));

       // PR: could be written more efficiently

-      return Contract.Exists(0, TypeParameters.Length, i => subst.ContainsKey(TypeParameters[i]) || Contract.Exists(subst.Values, t => t.FreeVariables.Has(TypeParameters[i])));

+      return Contract.Exists(0, TypeParameters.Length, i => subst.ContainsKey(TypeParameters[i]) || Contract.Exists(subst.Values, t => t.FreeVariables.Contains(TypeParameters[i])));

     }

 

     public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 26d57f68..47cf25d3 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -376,7 +376,7 @@ namespace Microsoft.Boogie {
         substMapOld.Add(mVar, ie);

         // FIXME why are we doing this? the modifies list should already include them.

         // add the modified variable to the modifies list of the procedure

-        if (!newModifies.Has(mie)) {

+        if (!newModifies.Contains(mie)) {

           newModifies.Add(mie);

         }

       }

diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs
index f984ecd4..58b6e9c0 100644
--- a/Source/Core/PureCollections.cs
+++ b/Source/Core/PureCollections.cs
@@ -794,7 +794,7 @@ namespace PureCollections {
 

     //pure---------------------------------------------------------------

     [Pure]

-    public bool Has(object x) {         // WS translate to tailrecursion 

+    public bool Contains(object x) {         // WS translate to tailrecursion 

       if (x == null)

         throw new MissingCase();

       Contract.Assert(this.elems != null);

diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs
index e65a570a..d97d56d0 100644
--- a/Source/Doomed/DoomedLoopUnrolling.cs
+++ b/Source/Doomed/DoomedLoopUnrolling.cs
@@ -114,7 +114,7 @@ namespace VC
             {

                 Contract.Assert(v != null);

                 IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-                if (!havocExprs.Has(ie))

+                if (!havocExprs.Contains(ie))

                     havocExprs.Add(ie);

             }

             // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index c4a54300..77e54945 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1000,12 +1000,12 @@ namespace Microsoft.Boogie.TypeErasure {
       if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))

         return rawType;

 

-      if (Contract.ForAll(0, rawType.FreeVariables.Length, var => !boundTypeParams.Has(rawType.FreeVariables[var]))) {

+      if (Contract.ForAll(0, rawType.FreeVariables.Length, var => !boundTypeParams.Contains(rawType.FreeVariables[var]))) {

         // Bingo!

         // if the type does not contain any bound variables, we can simply

         // replace it with a type variable

         TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Count);

-        Contract.Assume(!boundTypeParams.Has(abstractionVar));

+        Contract.Assume(!boundTypeParams.Contains(abstractionVar));

         instantiations.Add(rawType);

         return abstractionVar;

       }

@@ -1014,7 +1014,7 @@ namespace Microsoft.Boogie.TypeErasure {
         //

         // then the variable has to be bound, we cannot do anything

         TypeVariable/*!*/ rawVar = rawType.AsVariable;

-        Contract.Assume(boundTypeParams.Has(rawVar));

+        Contract.Assume(boundTypeParams.Contains(rawVar));

         return rawVar;

         //

       } else if (rawType.IsMap) {

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 44eb7dbb..12f8d7e3 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -355,7 +355,7 @@ namespace Microsoft.Boogie.TypeErasure
 

       foreach (TypeVariable/*!*/ var in allTypeParams) {

         Contract.Assert(var != null);

-        if (varsInInParamTypes.Has(var))

+        if (varsInInParamTypes.Contains(var))

           implicitParams.Add(var);

         else

           explicitParams.Add(var);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 09874382..055a79ad 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1830,7 +1830,7 @@ namespace VC {
         foreach (AssertCmd a in assertNodes) {

           // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)

           foreach (Block b in traceNodes) {

-            if (b.Cmds.Has(a)) {

+            if (b.Cmds.Contains(a)) {

               BlockSeq trace = new BlockSeq();

               trace.Add(b);

               Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, model, MvInfo, context);

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

           Contract.Assert(v != null);

           IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-          if(!havocExprs.Has(ie))

+          if(!havocExprs.Contains(ie))

             havocExprs.Add(ie);

         }

         // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct