Generate triggers for nested quantifiers as well

The new 'quantifiers' list keeps track of the quantifiers that have already been
seen, so that they are not added both as a member of a collection and as a
single quantifier.

1 files changed, 7 insertions, 3 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index a43aae7a..b30cb6b1 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -9,6 +9,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Dafny.Triggers { //FIXME rename this file

   internal class QuantifierCollector : TopDownVisitor<object> {

     readonly ErrorReporter reporter;

+    private HashSet<Expression> quantifiers = new HashSet<Expression>();

     internal List<QuantifiersCollection> quantifierCollections = new List<QuantifiersCollection>();

 

     public QuantifierCollector(ErrorReporter reporter) {

@@ -16,17 +17,20 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file
       this.reporter = reporter;

     }

 

-    protected override bool VisitOneExpr(Expression expr, ref object st) {

+    protected override bool VisitOneExpr(Expression expr, ref object _) {

       var quantifier = expr as QuantifierExpr;

-      if (quantifier != null) {

+

+      if (quantifier != null && !quantifiers.Contains(quantifier)) {

+        quantifiers.Add(quantifier);

         if (quantifier.SplitQuantifier != null) {

           var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);

           quantifierCollections.Add(new QuantifiersCollection(collection, reporter));

-          return false;

+          foreach (var q in quantifier.SplitQuantifier) { quantifiers.Add(q); }

         } else {

           quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));

         }

       }

+

       return true;

     }

   }