Start committing generated triggers when /autoTriggers is 1

1 files changed, 9 insertions, 4 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 4e274189..0798510a 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -39,15 +39,14 @@ namespace Microsoft.Dafny
   }

 

   public class TriggerGeneratingRewriter : IRewriter {

-    Triggers.QuantifierCollectionsFinder finder;

-

     internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {

       Contract.Requires(reporter != null);

-      this.finder = new Triggers.QuantifierCollectionsFinder(reporter);

     }

 

     internal override void PostResolve(ModuleDefinition m) {

-      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { //CLEMENT

+      var finder = new Triggers.QuantifierCollectionsFinder(reporter);

+

+      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

         if (decl is Function) {

           var function = (Function)decl;

           finder.Visit(function.Ens, null);

@@ -64,6 +63,12 @@ namespace Microsoft.Dafny
           }

         }

       }

+      

+      var triggersCollector = new Triggers.TriggersCollector();

+      foreach (var quantifierCollection in finder.quantifierCollections) {

+        quantifierCollection.ComputeTriggers(triggersCollector);

+        quantifierCollection.CommitTriggers();

+      }

     }

   }