summaryrefslogtreecommitdiff
path: root/Source/VCExpr
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr')
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs3
-rw-r--r--Source/VCExpr/Clustering.cs5
-rw-r--r--Source/VCExpr/LetBindingSorter.cs3
-rw-r--r--Source/VCExpr/TermFormulaFlattening.cs5
-rw-r--r--Source/VCExpr/TypeErasure.cs7
-rw-r--r--Source/VCExpr/TypeErasureArguments.cs3
-rw-r--r--Source/VCExpr/TypeErasurePremisses.cs12
-rw-r--r--Source/VCExpr/VCExprASTVisitors.cs12
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 03:12:59 +0000