Draft out a more advanced version of trigger generation

This new version will include a cleaner pipeline, and trigger splitting.

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 039aa56f..b5d89abd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -12895,6 +12895,8 @@ namespace Microsoft.Dafny {
             // that needed to be proved about the function was proved already in the previous module, even without the body definition).

           } else if (!FunctionBodyIsAvailable(f, currentModule)) {

             // Don't inline opaque functions or foreign protected functions

+          } else if (Attributes.Contains(f.Attributes, "no_inline")) {

+            // User manually prevented inlining

           } else if (CanSafelyInline(fexp, f)) {

             // inline this body

             var body = GetSubstitutedBody(fexp, f, false);

@@ -13106,7 +13108,7 @@ namespace Microsoft.Dafny {
     }

 

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

-      return !(protectedVariables.Contains(variable) && TriggerGenerator.IsTriggerKiller(substitution));

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

     }

 

     private class VariablesCollector: BottomUpVisitor {