Implement self-loop detection

Implementing loop detection between multiple triggers is much harder, as it
seems to require walking an exponentially sized graph. Self-loop detection is
still a net gain compared to the current situation: we used to not detect loops
in large quantifiers; not we break these apart, suppress the loops where we can
in the smaller parts, and report the ones that we can't suppress. It could be
that the broken-up quantifiers are mutually recursive, but these cases would
have already led to a loop in the past.

6 files changed, 275 insertions, 153 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b5d89abd..14fca463 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13107,8 +13107,10 @@ namespace Microsoft.Dafny {
       return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));

     }

 

+    Triggers.TriggersCollector triggersCollector = new Triggers.TriggersCollector();

+

     private bool CanSafelySubstitute(ISet<IVariable> protectedVariables, IVariable variable, Expression substitution) {

-      return !(protectedVariables.Contains(variable) && Dafny.Triggers.TriggersCollector.IsTriggerKiller(substitution));

+      return !(protectedVariables.Contains(variable) && triggersCollector.IsTriggerKiller(substitution));

     }

 

     private class VariablesCollector: BottomUpVisitor {

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index e83feebb..33be0da2 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -6,59 +6,76 @@ using System.Text;
 

 namespace Microsoft.Dafny.Triggers {

   class QuantifierSplitter : BottomUpVisitor {

-    internal enum Quantifier { Forall, Exists }

+    private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) {

+      if (opCode == BinaryExpr.Opcode.And) {

+        return BinaryExpr.Opcode.Or;

+      } else if (opCode == BinaryExpr.Opcode.Or) {

+        return BinaryExpr.Opcode.And;

+      } else {

+        throw new ArgumentException();

+      } 

+    }

+

+    // NOTE: If we wanted to split quantifiers as far as possible, it would be

+    // enough to put the formulas in DNF (for foralls) or CNF (for exists).

+    // Unfortunately, this would cause ill-behaved quantifiers to produce

+    // exponentially many smaller quantifiers.

 

-    internal static IEnumerable<Expression> BreakQuantifier(Expression expr, Quantifier quantifier) {

+    internal static IEnumerable<Expression> SplitExpr(Expression expr, BinaryExpr.Opcode separator) {

       expr = expr.Resolved;

+      var unary = expr as UnaryOpExpr;

       var binary = expr as BinaryExpr;

 

-      if (binary == null) {

-        yield return expr;

-        yield break;

+      if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) {

+        foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, e); }

+      } else if (binary != null && binary.Op == separator) {

+        foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; }

+        foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }

+      } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) {

+        foreach (var e in SplitExpr(new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, binary.E0), separator)) { yield return e; }

+        foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }

       }

+    }

 

-      var e0 = binary.E0;

-      var e1 = binary.E1;

-

-      if ((quantifier == Quantifier.Forall && binary.Op == BinaryExpr.Opcode.And) ||

-          (quantifier == Quantifier.Exists && binary.Op == BinaryExpr.Opcode.Or)) {

-        foreach (var e in BreakQuantifier(e0, quantifier)) { yield return e; }

-        foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; }

-      } else if (binary.Op == BinaryExpr.Opcode.Imp) {

-        if (quantifier == Quantifier.Forall) {

-          foreach (var e in BreakImplication(e0, e1, quantifier, expr.tok)) { yield return e; }

-        } else {

-          yield return new UnaryOpExpr(e1.tok, UnaryOpExpr.Opcode.Not, e1); // FIXME should be broken further

-          foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; }

-        }

-      } else {

-        yield return expr;

+    internal static IEnumerable<Expression> SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) {

+      foreach (var e1 in SplitExpr(pair.E1, separator)) { 

+        yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1);

       }

     }

 

-    internal static IEnumerable<Expression> BreakImplication(Expression ante, Expression post, Quantifier quantifier, IToken tok) { // FIXME: should work for exists and &&

-      foreach (var small_post in BreakQuantifier(post, quantifier)) {

-        var bin_post = small_post as BinaryExpr;

-        if (bin_post == null || bin_post.Op != BinaryExpr.Opcode.Imp) {

-          yield return new BinaryExpr(tok, BinaryExpr.Opcode.Imp, ante, small_post);

-        } else { // bin_post is an implication

-          var large_ante = new BinaryExpr(ante.tok, BinaryExpr.Opcode.And, ante, bin_post.E0);

-          foreach (var imp in BreakImplication(large_ante, bin_post.E1, quantifier, tok)) {

-            yield return imp;

-          }

+    internal static IEnumerable<Expression> SplitQuantifier(QuantifierExpr quantifier) {

+      var body = quantifier.LogicalBody();

+      var binary = body as BinaryExpr;

+

+      if (quantifier is ForallExpr) {

+        IEnumerable<Expression> stream;

+        if (binary != null && (binary.Op == BinaryExpr.Opcode.Imp || binary.Op == BinaryExpr.Opcode.Or)) {

+          stream = SplitAndStich(binary, BinaryExpr.Opcode.And);

+        } else {

+          stream = SplitExpr(body, BinaryExpr.Opcode.And);

+        }

+        foreach (var e in stream) {

+          yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes);

+        }

+      } else if (quantifier is ExistsExpr) {

+        IEnumerable<Expression> stream;

+        if (binary != null && binary.Op == BinaryExpr.Opcode.And) {

+          stream = SplitAndStich(binary, BinaryExpr.Opcode.Or);

+        } else {

+          stream = SplitExpr(body, BinaryExpr.Opcode.Or);

         }

+        foreach (var e in stream) {

+          yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes);

+        }

+      } else {

+        yield return quantifier;

       }

     }

-    

+        

     protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier

-      var forall = expr as ForallExpr;

-      var exists = expr as ExistsExpr;

-

-      if (forall != null && TriggerUtils.NeedsAutoTriggers(forall)) {

-        var rew = BreakQuantifier(forall.LogicalBody(), Quantifier.Forall);

-        //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));

-      } else if (exists != null && TriggerUtils.NeedsAutoTriggers(exists)) {

-        var rew = BreakQuantifier(exists.LogicalBody(), Quantifier.Exists);

+      var quantifier = expr as QuantifierExpr;

+      if (quantifier != null) {

+        var rew = SplitQuantifier(quantifier);

         //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));

       }

     }

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 3cbe3bd9..828e0e18 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -1,7 +1,11 @@
-using System;

+#define QUANTIFIER_WARNINGS

+

+using System;

 using System.Collections.Generic;

 using System.Linq;

 using System.Text;

+using Microsoft.Boogie;

+using System.Diagnostics.Contracts;

 

 //FIXME Generated triggers should be _triggers

 //FIXME: When scoring, do not consider old(x) to be higher than x.

@@ -9,18 +13,23 @@ using System.Text;
 namespace Microsoft.Dafny.Triggers {

   class QuantifierWithTriggers {

     internal QuantifierExpr quantifier;

-    internal List<MultiTriggerCandidate> triggers;

+    internal List<TriggerTerm> CandidateTerms;

+    internal List<TriggerCandidate> Candidates;

+    internal List<TriggerCandidate> RejectedCandidates;

+

+    internal bool AllowsLoops { get { return quantifier.Attributes.AsEnumerable().Any(a => a.Name == "loop"); } }

+    internal bool CouldSuppressLoops { get; set; }

 

     internal QuantifierWithTriggers(QuantifierExpr quantifier) {

       this.quantifier = quantifier;

-      this.triggers = null;

+      this.RejectedCandidates = new List<TriggerCandidate>();

     }

 

     internal void TrimInvalidTriggers() {

-      triggers = triggers.Where(tr => tr.MentionsAll(quantifier.BoundVars)).ToList();

+      Contract.Requires(CandidateTerms != null);

+      Contract.Requires(Candidates != null);

+      Candidates = TriggerUtils.Filter(Candidates, tr => tr.MentionsAll(quantifier.BoundVars), tr => { }).ToList();

     }

-

-    public bool QuantifierAlreadyHadTriggers { get { return !TriggerUtils.NeedsAutoTriggers(quantifier); } }

   }

 

   class QuantifiersCollection {

@@ -32,26 +41,32 @@ namespace Microsoft.Dafny.Triggers {
       this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList();

     }

 

-    void ComputeTriggers() {

-      CollectAndShareTriggers();

+    internal void ComputeTriggers(TriggersCollector triggersCollector) {

+      CollectAndShareTriggers(triggersCollector);

       TrimInvalidTriggers();

       BuildDependenciesGraph();

       SuppressMatchingLoops();

       SelectTriggers();

     }

+    

+    private bool SubsetGenerationPredicate(List<TriggerTerm> terms, TriggerTerm additionalTerm) {

+      // Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very

+      // large numbers of multi-triggers, most of which are useless. This filter

+      // restricts subsets of terms so that we only generate sets of terms where each

+      // element contributes at least one variable. In the example above, we'll only

+      // get 5 triggers.

+      return additionalTerm.Variables.Where(v => !terms.Any(t => t.Variables.Contains(v))).Any();

+    }

 

-    void CollectAndShareTriggers() {

-      var pool = quantifiers.SelectMany(q => TriggersCollector.CollectTriggers(q.quantifier));

-      var distinctPool = pool.Deduplicate((x, y) => ExprExtensions.ExpressionEq(x.Expr, y.Expr));

-      var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool).Select(candidates => new MultiTriggerCandidate(candidates)).ToList();

+    //FIXME document that this assumes that the quantifiers live in the same context and share the same variables

+    void CollectAndShareTriggers(TriggersCollector triggersCollector) {

+      var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier));

+      var distinctPool = pool.Deduplicate(TriggerTerm.Eq);

+      var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList();

 

       foreach (var q in quantifiers) {

-        if (q.QuantifierAlreadyHadTriggers) {

-          reporter.Info(MessageSource.Resolver, q.quantifier.tok, "Not generating triggers for this quantifier."); //FIXME: no_trigger is passed down to Boogie

-          return;

-        } else {

-          q.triggers = multiPool;

-        }

+        q.CandidateTerms = distinctPool;

+        q.Candidates = multiPool;

       }

     }

 

@@ -62,43 +77,111 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     void BuildDependenciesGraph() {

-      //FIXME

+      // FIXME: Think more about multi-quantifier dependencies

+      //class QuantifierDependency {

+      //  QuantifierWithTriggers Cause;

+      //  QuantifierWithTriggers Consequence;

+      //  List<TriggerCandidate> Triggers;

+      //  List<Expression> MatchingTerm;

+      //}

     }

 

     void SuppressMatchingLoops() {

-      //FIXME

+      // NOTE: This only looks for self-loops; that is, loops involving a single

+      // quantifier.

+

+      // For a given quantifier q, we introduce a triggering relation between trigger

+      // candidates by writing t1 → t2 if instantiating q from t1 introduces a ground

+      // term that matches t2. Then, we notice that this relation is transitive, since

+      // all triggers yield the same set of terms. This means that any matching loop

+      // t1 → ... → t1 can be reduced to a self-loop t1 → t1. Detecting such

+      // self-loops is then only a matter of finding terms in the body of the

+      // quantifier that match a given trigger.

+

+      // Of course, each trigger that actually appears in the body of the quantifier

+      // yields a trivial self-loop (e.g. P(i) in [∀ i {P(i)} ⋅ P(i)]), so we

+      // ignore this type of loops. In fact, we ignore any term in the body of the

+      // quantifier that matches one of the terms of the trigger (this ensures that

+      // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even

+      // ignore terms that almost match a trigger term, modulo a single variable

+      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop).

+      // This ignoring logic is implemented by the CouldCauseLoops method.

+

+      foreach (var q in quantifiers) {

+        var looping = new List<TriggerCandidate>();

+        var loopingSubterms = q.Candidates.ToDictionary(candidate => candidate, candidate => candidate.LoopingSubterms(q.quantifier).ToList());

+

+        var safe = TriggerUtils.Filter(

+          q.Candidates,

+          c => !loopingSubterms[c].Any(),

+          c => {

+            looping.Add(c);

+            c.Annotation = "loop with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", ");

+          }).ToList();

+

+        q.CouldSuppressLoops = safe.Count > 0;

+

+        if (!q.AllowsLoops && q.CouldSuppressLoops) {

+          q.Candidates = safe;

+          q.RejectedCandidates.AddRange(looping);

+        }

+      }

     }

 

     void SelectTriggers() {

       //FIXME

     }

 

-    private void CommitOne(QuantifierWithTriggers q) {

-      foreach (var multiCandidate in q.triggers) { //TODO: error message for when no triggers found

-        q.quantifier.Attributes = new Attributes("trigger", multiCandidate.terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes);

-      }

-

-

-      //TriggerUtils.DebugTriggers("  Final results:\n{0}", PickMultiTriggers(quantifier));

+    private void CommitOne(QuantifierWithTriggers q, object conjunctId) {

+      var errorLevel = ErrorLevel.Info;

+      var msg = new StringBuilder();

+      var indent = conjunctId != null ? "    " : "  ";

+      var header = conjunctId != null ? String.Format("  For conjunct {0}:{1}", conjunctId, Environment.NewLine) : "";

+

+      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: no_trigger is passed down to Boogie

+        msg.Append(indent).AppendLine("Not generating triggers for this quantifier.");

+      } else {

+        foreach (var candidate in q.Candidates) {

+          q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes);

+        }

 

-      //var multi_candidates = PickMultiTriggers(quantifier);

+        if (q.Candidates.Any()) {

+          msg.Append(indent).AppendLine("Selected triggers:");

+          foreach (var mc in q.Candidates) {

+            msg.Append(indent).Append("  ").AppendLine(mc.ToString());

+          }

+        }

 

-      //if (multi_candidates.RejectedMultiCandidates.Any()) {

-      //  var tooltip = TriggerUtils.JoinStringsWithHeader("Rejected: ", multi_candidates.RejectedMultiCandidates.Where(candidate => candidate.Tags != null)

-      //    .Select(candidate => candidate.AsDafnyAttributeString(true, true)));

-      //  reporter.Info(ErrorSource.Resolver, quantifier.tok, tooltip, quantifier.tok.val.Length);

-      //}

+        if (q.RejectedCandidates.Any()) {

+          msg.Append(indent).AppendLine("Rejected triggers:");

+          foreach (var mc in q.RejectedCandidates) {

+            msg.Append(indent).Append("  ").AppendLine(mc.ToString());

+          }

+        }

 

-      //if (multi_candidates.FinalMultiCandidates.Any()) {

-      //  var tooltip = JoinStringsWithHeader("Triggers: ", multi_candidates.FinalMultiCandidates.Select(multi_candidate => multi_candidate.AsDafnyAttributeString()));

-      //  reporter.Info(ErrorSource.Resolver, quantifier.tok, tooltip, quantifier.tok.val.Length);

-      //}

+#if QUANTIFIER_WARNINGS

+        if (!q.CandidateTerms.Any()) {

+          errorLevel = ErrorLevel.Warning;

+          msg.Append(indent).AppendLine("No terms found to trigger on.");

+        } else if (!q.Candidates.Any()) {

+          errorLevel = ErrorLevel.Warning;

+          msg.Append(indent).AppendLine("No trigger covering all quantified variables found.");

+        } else if (!q.CouldSuppressLoops) {

+          errorLevel = ErrorLevel.Warning;

+          msg.Append(indent).AppendLine("Suppressing loops would leave this quantifier without triggers.");

+        }

+#endif

+      }

 

-      //string warning = multi_candidates.Warning();

-      //if (warning != null) {

-      //  // FIXME reenable Resolver.Warning(quantifier.tok, warning);

-      //}

+      if (msg.Length > 0) {

+        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, header + msg.ToString());

+      }

     }

 

+    internal void CommitTriggers() {

+      foreach (var q in quantifiers) {

+        CommitOne(q, quantifiers.Count > 1 ? q.quantifier : null);

+      }

+    }

   }

 }

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index 7bebe1ac..da43abcc 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -22,6 +22,20 @@ namespace Microsoft.Dafny.Triggers {
     }

   }

 

+  internal struct TriggerMatch {

+    internal Expression Expr;

+    internal Dictionary<IVariable, Expression> Bindings;

+

+    internal static bool Eq(TriggerMatch t1, TriggerMatch t2) {

+      return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr);

+    }

+

+    internal bool CouldCauseLoops(List<TriggerTerm> terms) {

+      var expr = Expr;

+      return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNames(expr));

+    }

+  }

+

   internal static class ExprExtensions {

     internal static IEnumerable<Expression> AllSubExpressions(this Expression expr, bool strict = false) {

       foreach (var subexpr in expr.SubExpressions) {

@@ -75,7 +89,7 @@ namespace Microsoft.Dafny.Triggers {
       return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2));

     }

 

-    private static bool MatchesTrigger(this Expression expr, Expression trigger, ISet<BoundVar> holes, Dictionary<IVariable, Expression> bindings) {

+    internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet<BoundVar> holes, Dictionary<IVariable, Expression> bindings) {

       expr = expr.Resolved;

       trigger = trigger.Resolved;

 

@@ -96,27 +110,6 @@ namespace Microsoft.Dafny.Triggers {
       return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings));

     }

 

-    internal struct TriggerMatch {

-      internal Expression Expr;

-      internal Dictionary<IVariable, Expression> Bindings;

-

-      internal bool CouldCauseLoops(IEnumerable<TriggerCandidate> candidates) {

-        // A match for a trigger in the body of a quantifier can be a problem if 

-        // it yields to a matching loop: for example, f(x) is a bad trigger in 

-        //   forall x, y :: f(x) = f(f(x))

-        // In general, any such match can lead to a loop, but two special cases 

-        // will only lead to a finite number of instantiations:

-        // 1. The match equals one of the triggers in the set of triggers under

-        //    consideration. For example, { f(x) } a bad trigger above, but the

-        //    pair { f(x), f(f(x)) } is fine (instantiating won't yield new 

-        //    matches)

-        // 2. The match only differs from one of these triggers by variable 

-        //    names. This is a superset of the previous case.

-        var expr = Expr;

-        return !candidates.Any(c => c.Expr.ExpressionEqModuloVariableNames(expr));

-      }

-    }

-

     private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, ISet<BoundVar> holes) {

       var bindings = new Dictionary<IVariable, Expression>();

       return expr.MatchesTrigger(trigger, holes, bindings) ? new TriggerMatch { Expr = expr, Bindings = bindings } : (TriggerMatch?)null;

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 5a118a2f..dedbcbb1 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -15,21 +15,23 @@ namespace Microsoft.Dafny.Triggers {
       return copy;

     }

 

-    internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, int offset) {

+    internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, Func<List<T>, T, bool> predicate, int offset) {

       if (offset >= source.Count) {

         yield return new List<T>();

         yield break;

       }

 

-      foreach (var subset in AllSubsets<T>(source, offset + 1)) {

-        yield return CopyAndAdd(subset, source[offset]);

+      foreach (var subset in AllSubsets<T>(source, predicate, offset + 1)) {

+        if (predicate(subset, source[offset])) {

+          yield return CopyAndAdd(subset, source[offset]);

+        }

         yield return new List<T>(subset);

       }

     }

 

-    internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source) {

+    internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source, Func<List<T>, T, bool> predicate) {

       List<T> all = new List<T>(source);

-      foreach (var subset in AllSubsets(all, 0)) {

+      foreach (var subset in AllSubsets(all, predicate, 0)) {

         if (subset.Count > 0) {

           yield return subset;

         }

@@ -74,6 +76,17 @@ namespace Microsoft.Dafny.Triggers {
       return it1_has == it2_has && acc;

     }

 

+    internal static IEnumerable<T> Filter<T>(IEnumerable<T> elements, Func<T, bool> predicate, Action<T> reject) {

+      var positive = new List<T>();

+      foreach (var c in elements) {

+        if (predicate(c)) {

+          yield return c;

+        } else {

+          reject(c);

+        }

+      }

+    }

+

     internal static bool SameNullity<T>(T x1, T x2) where T : class {

       return (x1 == null) == (x2 == null);

     }

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 912a661c..e1f8a013 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -7,52 +7,68 @@ using System.Diagnostics.Contracts;
 using System.Diagnostics;

 

 namespace Microsoft.Dafny.Triggers {

-  struct TriggerCandidate {

+  class TriggerTerm {

     internal Expression Expr { get; set; }

     internal ISet<IVariable> Variables { get; set; }

 

     public override string ToString() {

       return Printer.ExprToString(Expr);

     }

+

+    internal static bool Eq(TriggerTerm t1, TriggerTerm t2) {

+      return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr);

+    }

   }

 

-  class MultiTriggerCandidate {

-    internal List<TriggerCandidate> terms { get; set; }

+  class TriggerCandidate {

+    internal List<TriggerTerm> Terms { get; set; }

+    internal string Annotation { get; set; }

+

+    internal TriggerCandidate(List<TriggerTerm> terms) {

+      this.Terms = terms;

+    }

 

-    internal MultiTriggerCandidate(List<TriggerCandidate> candidates) {

-      this.terms = candidates;

+    public TriggerCandidate(TriggerCandidate mc, string annotation) {

+      this.Terms = mc.Terms;

+      this.Annotation = annotation;

     }

 

     internal bool MentionsAll(List<BoundVar> vars) {

-      return vars.All(x => terms.Any(candidate => candidate.Variables.Contains(x)));

+      return vars.All(x => Terms.Any(term => term.Variables.Contains(x)));

     }

 

+    private string Repr { get { return Terms.MapConcat(t => Printer.ExprToString(t.Expr), ", "); } }

+

     public override string ToString() {

-      return String.Join(", ", terms);

+      return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")");

     }

 

-    public String AsDafnyAttributeString(bool wrap = true, bool includeTags = false) {

-      var repr = terms.MapConcat(t => Printer.ExprToString(t.Expr), ", ");

-      if (wrap) {

-        repr = "{:trigger " + repr + "}";

-      }

-      return repr;

+    internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

+      var matchingSubterms = MatchingSubterms(quantifier);

+      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

+    }

+

+    internal List<TriggerMatch> MatchingSubterms(QuantifierExpr quantifier) {

+      //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare against.

+      return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq);

+    }

+

+    public String AsDafnyAttributeString() {

+      return "{:trigger " + Repr + "}";

     }

   }

 

   class TriggerAnnotation {

     internal bool IsTriggerKiller;

     internal ISet<IVariable> Variables;

-    internal readonly List<TriggerCandidate> PrivateTerms;

-    internal readonly List<TriggerCandidate> ExportedTerms;

+    internal readonly List<TriggerTerm> PrivateTerms;

+    internal readonly List<TriggerTerm> ExportedTerms;

 

-    internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable<IVariable> Variables,

-                                IEnumerable<TriggerCandidate> AllCandidates, IEnumerable<TriggerCandidate> PrivateCandidates = null) {

+    internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable<IVariable> Variables, IEnumerable<TriggerTerm> AllTerms, IEnumerable<TriggerTerm> PrivateTerms = null) {

       this.IsTriggerKiller = IsTriggerKiller;

       this.Variables = new HashSet<IVariable>(Variables);

-

-      this.PrivateTerms = new List<TriggerCandidate>(PrivateCandidates == null ? Enumerable.Empty<TriggerCandidate>() : PrivateCandidates);

-      this.ExportedTerms = new List<TriggerCandidate>(AllCandidates == null ? Enumerable.Empty<TriggerCandidate>() : AllCandidates.Except(this.PrivateTerms));

+      this.PrivateTerms = new List<TriggerTerm>(PrivateTerms == null ? Enumerable.Empty<TriggerTerm>() : PrivateTerms);

+      this.ExportedTerms = new List<TriggerTerm>(AllTerms == null ? Enumerable.Empty<TriggerTerm>() : AllTerms.Except(this.PrivateTerms));

     }

 

     public override string ToString() {

@@ -66,15 +82,15 @@ namespace Microsoft.Dafny.Triggers {
         sb.AppendFormat(subindent, bv.Name);

       }

 

-      sb.AppendFormat(nindent, "Exported candidates:");

-      foreach (var candidate in ExportedTerms) {

-        sb.AppendFormat(subindent, candidate);

+      sb.AppendFormat(nindent, "Exported terms:");

+      foreach (var term in ExportedTerms) {

+        sb.AppendFormat(subindent, term);

       }

 

       if (PrivateTerms.Any()) {

-        sb.AppendFormat(nindent, "Private candidates:");

-        foreach (var candidate in PrivateTerms) {

-          sb.AppendFormat(subindent, candidate);

+        sb.AppendFormat(nindent, "Private terms:");

+        foreach (var term in PrivateTerms) {

+          sb.AppendFormat(subindent, term);

         }

       }

 

@@ -85,9 +101,7 @@ namespace Microsoft.Dafny.Triggers {
   public class TriggersCollector {

     Dictionary<Expression, TriggerAnnotation> cache;

 

-    private static TriggersCollector instance = new TriggersCollector();

-

-    private TriggersCollector() {

+    internal TriggersCollector() {

       this.cache = new Dictionary<Expression, TriggerAnnotation>();

     }

 

@@ -96,8 +110,8 @@ namespace Microsoft.Dafny.Triggers {
                                 .Aggregate(seed, (acc, e) => reduce(acc, e));

     }

 

-    private List<TriggerCandidate> CollectExportedCandidates(Expression expr) {

-      return ReduceAnnotatedSubExpressions<List<TriggerCandidate>>(expr, new List<TriggerCandidate>(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst);

+    private List<TriggerTerm> CollectExportedCandidates(Expression expr) {

+      return ReduceAnnotatedSubExpressions<List<TriggerTerm>>(expr, new List<TriggerTerm>(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst);

     }

 

     private ISet<IVariable> CollectVariables(Expression expr) {

@@ -108,8 +122,8 @@ namespace Microsoft.Dafny.Triggers {
       return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b);

     }

 

-    private IEnumerable<TriggerCandidate> OnlyPrivateCandidates(List<TriggerCandidate> candidates, IEnumerable<IVariable> privateVars) {

-      return candidates.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf

+    private IEnumerable<TriggerTerm> OnlyPrivateCandidates(List<TriggerTerm> terms, IEnumerable<IVariable> privateVars) {

+      return terms.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf

     }

 

     private TriggerAnnotation Annotate(Expression expr) {

@@ -195,18 +209,18 @@ namespace Microsoft.Dafny.Triggers {
     private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {

       bool expr_is_killer = false;

       var new_expr = CleanupExpr(expr, out expr_is_killer);

-      var new_candidate = new TriggerCandidate { Expr = new_expr, Variables = CollectVariables(expr) };

+      var new_term = new TriggerTerm { Expr = new_expr, Variables = CollectVariables(expr) };

 

-      List<TriggerCandidate> collected_candidates = CollectExportedCandidates(expr);

+      List<TriggerTerm> collected_terms = CollectExportedCandidates(expr);

       var children_contain_killers = CollectIsKiller(expr);

 

       if (!children_contain_killers) {

         // Add only if the children are not killers; the head has been cleaned up into non-killer form

-        collected_candidates.Add(new_candidate);

+        collected_terms.Add(new_term);

       }

 

       // This new node is a killer if its children were killers, or if it's non-cleaned-up head is a killer

-      return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_candidate.Variables, collected_candidates);

+      return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_term.Variables, collected_terms);

     }

 

     private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) {

@@ -218,13 +232,13 @@ namespace Microsoft.Dafny.Triggers {
       // only possible child here; there can be DatatypeValue nodes, for example (see vstte2012/Combinators.dfy).

       var annotation = AnnotatePotentialCandidate(expr);

       // Comparing by reference is fine here. Using sets could yield a small speedup

-      annotation.ExportedTerms.RemoveAll(candidate => expr.SubExpressions.Contains(candidate.Expr));

+      annotation.ExportedTerms.RemoveAll(term => expr.SubExpressions.Contains(term.Expr));

       return annotation;

     }

 

     private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable<BoundVar> boundVars) {

-      var candidates = CollectExportedCandidates(expr);

-      return new TriggerAnnotation(true, CollectVariables(expr), candidates, OnlyPrivateCandidates(candidates, boundVars));

+      var terms = CollectExportedCandidates(expr);

+      return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, boundVars));

     }

 

     private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) {

@@ -244,13 +258,13 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     // FIXME document that this will contain duplicates

-    internal static List<TriggerCandidate> CollectTriggers(QuantifierExpr quantifier) {

+    internal List<TriggerTerm> CollectTriggers(QuantifierExpr quantifier) {

       // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions

-      return instance.Annotate(quantifier).PrivateTerms;

+      return Annotate(quantifier).PrivateTerms;

     }

 

-    internal static bool IsTriggerKiller(Expression expr) {

-      return instance.Annotate(expr).IsTriggerKiller;

+    internal bool IsTriggerKiller(Expression expr) {

+      return Annotate(expr).IsTriggerKiller;

     }

   }

 }