Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in code (as opposed to contracts).

8 files changed, 28 insertions, 22 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 22ba09be..0b92b1c3 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -6,6 +6,7 @@
 using System;

 using System.Text;

 using System.IO;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

@@ -36,7 +37,7 @@ namespace Microsoft.Boogie.VCExprAST {
       if (kinds.IndexOf(',') < 0) {

         return IsProverCommandSupported(kinds);

       } else {

-        return Contract.Exists(kinds.Split(',', ' '), k => IsProverCommandSupported(k));

+        return kinds.Split(',', ' ').Any(k => IsProverCommandSupported(k));

       }

     }

 

diff --git a/Source/VCExpr/Clustering.cs b/Source/VCExpr/Clustering.cs
index 1efc3606..1ab10107 100644
--- a/Source/VCExpr/Clustering.cs
+++ b/Source/VCExpr/Clustering.cs
@@ -6,6 +6,7 @@
 using System;

 using System.Text;

 using System.IO;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

@@ -398,12 +399,12 @@ namespace Microsoft.Boogie.Clustering {
 

     public bool RepresentationIsRenaming(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars) {

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

-      if (!Contract.ForAll(Representation, pair => pair.Key.Expr0 is VCExprVar && pair.Key.Expr1 is VCExprVar && !globalVars.ContainsKey(cce.NonNull((VCExprVar)pair.Key.Expr0)) && !globalVars.ContainsKey(cce.NonNull((VCExprVar/*!*/)pair.Key.Expr1))))

+      if (!Representation.Any(pair => pair.Key.Expr0 is VCExprVar && pair.Key.Expr1 is VCExprVar && !globalVars.ContainsKey(cce.NonNull((VCExprVar)pair.Key.Expr0)) && !globalVars.ContainsKey(cce.NonNull((VCExprVar/*!*/)pair.Key.Expr1))))

         return false;

       // check that all substituted variables are distinct

       // TODO: optimise

       return

-        Contract.ForAll(Representation, pair1 => Contract.ForAll(Representation, pair2 => pair1.Value.Equals(pair2.Value) || !pair1.Key.Expr0.Equals(pair2.Key.Expr0) && !pair1.Key.Expr1.Equals(pair2.Key.Expr1)));

+        Representation.All(pair1 => Representation.All(pair2 => pair1.Value.Equals(pair2.Value) || !pair1.Key.Expr0.Equals(pair2.Key.Expr0) && !pair1.Key.Expr1.Equals(pair2.Key.Expr1)));

     }

 

     public void RepresentationSize(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, out int expr0Size, out int expr1Size) {

diff --git a/Source/VCExpr/LetBindingSorter.cs b/Source/VCExpr/LetBindingSorter.cs
index 97d71e27..474770d0 100644
--- a/Source/VCExpr/LetBindingSorter.cs
+++ b/Source/VCExpr/LetBindingSorter.cs
@@ -6,6 +6,7 @@
 using System;

 using System.Text;

 using System.IO;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

@@ -87,7 +88,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
         }

       }

 

-      if (Contract.Exists(boundVars, pair=> pair.Value.InvOccurrencesNum > 0))

+      if (boundVars.Any(pair=> pair.Value.InvOccurrencesNum > 0))

         System.Diagnostics.Debug.Fail("Cyclic let-bindings");

 

       Contract.Assert(node.Length == sortedBindings.Count);

diff --git a/Source/VCExpr/TermFormulaFlattening.cs b/Source/VCExpr/TermFormulaFlattening.cs
index 7111939a..9198d753 100644
--- a/Source/VCExpr/TermFormulaFlattening.cs
+++ b/Source/VCExpr/TermFormulaFlattening.cs
@@ -6,6 +6,7 @@
 using System;

 using System.Text;

 using System.IO;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

@@ -99,8 +100,8 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()))
       foreach (KeyValuePair<VCExpr, VCExprVar> pair in Bindings) {

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

         coll.Collect(pair.Key);

-        if (Contract.Exists(boundVars, var => coll.FreeTermVars.ContainsKey(var)) ||

-            Contract.Exists(boundTypeVars, var => coll.FreeTypeVars.Contains(var)))

+        if (boundVars.Any(var => coll.FreeTermVars.ContainsKey(var)) ||

+            boundTypeVars.Any(var => coll.FreeTypeVars.Contains(var)))

           res.Add(Gen.LetBinding(pair.Value, pair.Key));

         coll.Reset();

       }

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index a25781af..9614f9f8 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -6,6 +6,7 @@
 using System;

 using System.Text;

 using System.IO;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

@@ -989,7 +990,7 @@ namespace Microsoft.Boogie.TypeErasure {
       if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))

         return rawType;

 

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

+      if (rawType.FreeVariables.All(var => !boundTypeParams.Contains(var))) {

         // Bingo!

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

         // replace it with a type variable

@@ -1361,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure {
       List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, newPolarity);

       Type/*!*/ oldType = node[0].Type;

       if (AxBuilder.UnchangedType(oldType) &&

-          Contract.ForAll(1, node.Arity, i => node[i].Type.Equals(oldType)))

+          node.All(e => e.Type.Equals(oldType)))

         return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));

       else

         return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));

@@ -1568,7 +1569,7 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

       VariableCastCollector/*!*/ collector = new VariableCastCollector(axBuilder);

       Contract.Assert(collector != null);

-      if (Contract.Exists(newNode.Triggers, trigger => trigger.Pos)) {

+      if (newNode.Triggers.Any(trigger => trigger.Pos)) {

         // look in the given triggers

         foreach (VCTrigger/*!*/ trigger in newNode.Triggers) {

           Contract.Assert(trigger != null);

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 00259ecd..8885cbc7 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -6,6 +6,7 @@
 using System;

 using System.Text;

 using System.IO;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

@@ -108,7 +109,7 @@ namespace Microsoft.Boogie.TypeErasure {
 

         // if all of the parameters are int or bool, the function does

         // not have to be changed

-        if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

+        if (fun.InParams.All(param => UnchangedType(cce.NonNull(param).TypedIdent.Type)) &&

             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type)) {

           res = fun;

         } else {

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index c6b5eee6..fc3d1214 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -374,7 +374,7 @@ namespace Microsoft.Boogie.TypeErasure
 

         // if all of the parameters are int or bool, the function does

         // not have to be changed

-        if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

+        if (fun.InParams.All(param => UnchangedType(cce.NonNull(param).TypedIdent.Type)) &&

             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&

             fun.TypeParameters.Count == 0) {

           res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());

@@ -641,9 +641,9 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Ensures(Contract.ValueAtReturn(out mapTypeSynonym) != null);

       Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out typeParams)));

       Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out originalIndexTypes)));

-      typeParams = new List<TypeVariable/*!*/>(abstractedType.TypeParameters.Count + abstractedType.FreeVariables.Count);

-      typeParams.AddRange(abstractedType.TypeParameters.ToList());

-      typeParams.AddRange(abstractedType.FreeVariables.ToList());

+      typeParams = new List<TypeVariable/*!*/>();

+      typeParams.AddRange(abstractedType.TypeParameters);

+      typeParams.AddRange(abstractedType.FreeVariables);

 

       originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);

       List<Type>/*!*/ mapTypeParams = new List<Type>();

@@ -1115,7 +1115,7 @@ namespace Microsoft.Boogie.TypeErasure
       if (typeVarBindings.Count < node.TypeParameters.Count) {

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

           Contract.Assert(var != null);

-          if (!Contract.Exists(typeVarBindings, b => b.V.Equals(var)))

+          if (typeVarBindings.All(b => b.V.Equals(var)))

             newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]);

         }

       }

@@ -1196,7 +1196,7 @@ namespace Microsoft.Boogie.TypeErasure
           Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =

                       FreeVariableCollector.FreeTermVariables(e);

           Contract.Assert(freeVars != null && cce.NonNullElements(freeVars.Keys));

-          if (Contract.Exists(typeVarBindings, b => freeVars.ContainsKey(b.V))) {

+          if (typeVarBindings.Any(b => freeVars.ContainsKey(b.V))) {

             exprsWithLets.Add(Gen.Let(typeVarBindings, e));

             changed = true;

           } else {

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 67280bea..10c06abf 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -1072,13 +1072,13 @@ namespace Microsoft.Boogie.VCExprAST {
 

     public bool TermSubstIsEmpty {

       get {

-        return Contract.ForAll(TermSubsts, dict => dict.Count == 0);

+        return TermSubsts.All(dict => dict.Count == 0);

       }

     }

 

     public bool TypeSubstIsEmpty {

       get {

-        return Contract.ForAll(TypeSubsts, dict => dict.Count == 0);

+        return TypeSubsts.All(dict => dict.Count == 0); ;

       }

     }

 

@@ -1173,15 +1173,15 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Requires(cce.NonNullElements(boundVars));

       Contract.Requires(substitution != null);

       // variables can be shadowed by a binder

-      if (Contract.Exists(typeParams, var => substitution.ContainsKey(var)) ||

-          Contract.Exists(boundVars, var => substitution.ContainsKey(var)))

+      if (typeParams.Any(var => substitution.ContainsKey(var)) ||

+          boundVars.Any(var => substitution.ContainsKey(var)))

         return true;

       // compute the codomain of the substitution

       FreeVariableCollector coll = substitution.Codomains;

       Contract.Assert(coll != null);

       // variables could be captured when applying the substitution

-      return Contract.Exists(typeParams, var => coll.FreeTypeVars.Contains(var)) ||

-             Contract.Exists(boundVars, var => coll.FreeTermVars.ContainsKey(var));

+      return typeParams.Any(var => coll.FreeTypeVars.Contains(var)) ||

+             boundVars.Any(var => coll.FreeTermVars.ContainsKey(var));

     }

 

     // can be overwritten if names of bound variables are to be changed