Implement the SelectTrigger method, removing redundant triggers.

The idea is that we define an partial order on triggers (which may contain
multiple terms), and find all the maximal elements. The algorithm as
implemented is rather inefficient; in particular, is does not look at the
structure of the graph of the relation (thus is does many redundant
comparisons). See triggers/useless-triggers-are-removed.dfy for an example
where such a filter is useful.

5 files changed, 106 insertions, 24 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index e2afa2ee..bfa90d81 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -7,7 +7,6 @@ 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.

 

 namespace Microsoft.Dafny.Triggers {

@@ -28,7 +27,7 @@ namespace Microsoft.Dafny.Triggers {
     internal void TrimInvalidTriggers() {

       Contract.Requires(CandidateTerms != null);

       Contract.Requires(Candidates != null);

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

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

     }

   }

 

@@ -60,7 +59,13 @@ namespace Microsoft.Dafny.Triggers {
       return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();

     }

 

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

+    /// <summary>

+    /// Collect triggers from the body of each quantifier, and share them

+    /// between all quantifiers. This method assumes that all quantifiers

+    /// actually come from the same context, and were the result of a split that

+    /// gave them all the same variables.

+    /// </summary>

+    /// <param name="triggersCollector"></param>

     void CollectAndShareTriggers(TriggersCollector triggersCollector) {

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

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

@@ -79,13 +84,10 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     void BuildDependenciesGraph() {

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

-      //class QuantifierDependency {

-      //  QuantifierWithTriggers Cause;

-      //  QuantifierWithTriggers Consequence;

-      //  List<TriggerCandidate> Triggers;

-      //  List<Expression> MatchingTerm;

-      //}

+      // The problem of finding matching loops between multiple-triggers is hard; it

+      // seems to require one to track exponentially-sized dependencies between parts

+      // of triggers and quantifiers. For now, we only do single-quantifier loop

+      // detection

     }

 

     void SuppressMatchingLoops() {

@@ -111,14 +113,14 @@ namespace Microsoft.Dafny.Triggers {
 

       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 = "loops with " + loopingSubterms[c].MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");

+          candidate => candidate.LoopingSubterms(q.quantifier).ToList(),

+          (candidate, loopingSubterms) => !loopingSubterms.Any(),

+          (candidate, loopingSubterms) => {

+            looping.Add(candidate);

+            candidate.Annotation = "loops with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");

           }).ToList();

 

         q.CouldSuppressLoops = safe.Count > 0;

@@ -131,7 +133,15 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     void SelectTriggers() {

-      //FIXME

+      foreach (var q in quantifiers) { //FIXME Check whether this makes verification faster

+        q.Candidates = TriggerUtils.Filter(q.Candidates,

+          candidate => q.Candidates.Where(candidate.IsStrongerThan).ToList(),

+          (candidate, weakerCandidates) => !weakerCandidates.Any(),

+          (candidate, weakerCandidates) => {

+            q.RejectedCandidates.Add(candidate);

+            candidate.Annotation = "stronger than " + String.Join(", ", weakerCandidates);

+          }).ToList();

+      }

     }

 

     private void CommitOne(QuantifierWithTriggers q, bool addHeader) {

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 9ebcf846..6f76464b 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -76,13 +76,14 @@ 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) {

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

       var positive = new List<T>();

-      foreach (var c in elements) {

-        if (predicate(c)) {

-          yield return c;

+      foreach (var elem in elements) {

+        var conv = Converter(elem);

+        if (predicate(elem, conv)) {

+          yield return elem;

         } else {

-          reject(c);

+          reject(elem, conv);

         }

       }

     }

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 735baa01..3b2853ed 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -20,6 +20,20 @@ namespace Microsoft.Dafny.Triggers {
       // rather misleading.

     }

 

+    internal enum TermComparison {

+      SameStrength = 0, Stronger = 1, NotStronger = -1

+    }

+

+    internal TermComparison CompareTo(TriggerTerm other) {

+      if (this == other) {

+        return TermComparison.SameStrength;

+      } else if (Expr.AllSubExpressions(true).Any(other.Expr.ExpressionEq)) {

+        return TermComparison.Stronger;

+      } else {

+        return TermComparison.NotStronger;

+      }

+    }

+

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

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

     }

@@ -41,7 +55,7 @@ namespace Microsoft.Dafny.Triggers {
       return vars.All(x => Terms.Any(term => term.Variables.Contains(x)));

     }

 

-    private string Repr { get { return String.Join(", ", Terms); } }

+    internal string Repr { get { return String.Join(", ", Terms); } }

 

     public override string ToString() {

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

@@ -58,8 +72,23 @@ namespace Microsoft.Dafny.Triggers {
       return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq);

     }

 

-    public String AsDafnyAttributeString() {

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

+    internal bool IsStrongerThan(TriggerCandidate that) {

+      if (this == that) {

+        return false; 

+      }

+

+      var hasStrictlyStrongerTerm = false;

+      foreach (var t in Terms) {

+        var comparison = that.Terms.Select(t.CompareTo).Max();

+

+        // All terms of `this` must be at least as strong as a term of `that`

+        if (comparison == TriggerTerm.TermComparison.NotStronger) { return false; }

+

+        // Did we find a strictly stronger term?

+        hasStrictlyStrongerTerm = hasStrictlyStrongerTerm || comparison == TriggerTerm.TermComparison.Stronger;

+      }

+

+      return hasStrictlyStrongerTerm;

     }

   }

 

diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy
new file mode 100644
index 00000000..16458e41
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file ensures that Dafny does get rid of redundant triggers before

+// annotating a quantifier, and that ths process does not interfere with cycle

+// detection.

+

+function f(x: int): int

+function g(x: int): int

+function h(x: int): int

+

+method M()

+  // In the following, only f(x) is kept. Note that the subset enumeration was

+  // already smart enough to not build any trigger with multiple terms (it only

+  // built 5 candidates)

+  requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0

+

+  // Loop detection still works fine: in the following example, the trigger is

+  // f(f(x))

+  requires forall x: int :: f(x) == f(f(x))

+

+  // This works for multi-triggers, too:

+  requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0

+{

+}

diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
new file mode 100644
index 00000000..6c2c0a2b
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -0,0 +1,17 @@
+useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}

+ Rejected triggers:

+   {h(g(f(x)))} (stronger than {g(f(x))}, {f(x)})

+   {g(h(f(x)))} (stronger than {h(f(x))}, {f(x)})

+   {h(f(x))} (stronger than {f(x)})

+   {g(f(x))} (stronger than {f(x)})

+useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}

+ Rejected triggers: {f(x)} (loops with {f(f(x))})

+useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:

+   {g(f(x)), g(y)}, {f(y), f(x)}

+ Rejected triggers:

+   {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})

+   {g(f(x)), g(f(y))} (stronger than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})

+   {g(f(x)), f(y)} (stronger than {f(y), f(x)})

+   {g(f(y)), f(x)} (stronger than {f(y), f(x)})

+

+Dafny program verifier finished with 5 verified, 0 errors