Skip to content

Commit

Permalink
named function to filter equality expressions
Browse files Browse the repository at this point in the history
  • Loading branch information
bkragl committed Sep 14, 2016
1 parent f786ee3 commit 7c9ac92
Showing 1 changed file with 8 additions and 3 deletions.
11 changes: 8 additions & 3 deletions Source/Concurrency/TransitionRelationComputation.cs
Original file line number Diff line number Diff line change
Expand Up @@ -258,10 +258,15 @@ private bool IsMapStoreExpr(Expr expr)
}
return naryExpr.Fun is MapStore;
}


private IEnumerable<NAryExpr> FilterEqualities(IEnumerable<Expr> exprs)
{
return exprs.OfType<NAryExpr>().Where(x => x.Fun.FunctionName == "==");
}

void InferSubstitution(HashSet<Variable> allExistsVars, Dictionary<Variable, Expr> existsSubstitutionMap, List<Expr> pathExprs, List<Expr> inferredSelectEqualities)
{
foreach (var eqExpr in pathExprs.OfType<NAryExpr>().Where(x => x.Fun.FunctionName == "=="))
foreach (var eqExpr in FilterEqualities(pathExprs))
{
Expr arg0 = eqExpr.Args[0];
Expr arg1 = eqExpr.Args[1];
Expand All @@ -276,7 +281,7 @@ void InferSubstitution(HashSet<Variable> allExistsVars, Dictionary<Variable, Exp
}

Dictionary<Variable, Expr> pendingMap = new Dictionary<Variable, Expr>();
foreach (var eqExpr in pathExprs.Union(inferredSelectEqualities).OfType<NAryExpr>().Where(x => x.Fun.FunctionName == "=="))
foreach (var eqExpr in FilterEqualities(pathExprs.Union(inferredSelectEqualities)))
{
Variable eVar = null;
Expr eVarSubstExpr = null;
Expand Down

0 comments on commit 7c9ac92

Please sign in to comment.