Improve the redundancy detection algorithm used while constructing sets of terms

Based on an issue noted by Chris with redundancy removal resuls being dependent
on the order of the terms. Interestingly, one of our tests already had an
instance of that problem.

Also fix the issue with nested quantifiers getting redundant triggers.

7 files changed, 143 insertions, 23 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c7aae173..9bff2038 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2965,6 +2965,7 @@ namespace Microsoft.Dafny {
     }

   }

 

+  [DebuggerDisplay("Bound<{name}>")]

   public class BoundVar : NonglobalVariable {

     public override bool IsMutable {

       get {

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 6555b52a..114d5f5d 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -47,15 +47,9 @@ namespace Microsoft.Dafny.Triggers {
       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.

-      // Note that this may still be an over-approximation, as in the following example:

-      // forall a, b :: forall x :: a[x] || b[x] > 0.

-      return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();

+    private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) {

+      return true; // FIXME Remove this

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

     }

 

     /// <summary>

@@ -68,11 +62,10 @@ namespace Microsoft.Dafny.Triggers {
     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) {

-        q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed

-        q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList();

+        q.CandidateTerms = distinctPool; // The list of candidate terms is immutable

+        q.Candidates = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate, q.quantifier.BoundVars).Select(set => set.ToTriggerCandidate()).ToList();

       }

     }

 

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 4fd139e2..efa1f167 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -15,29 +15,109 @@ namespace Microsoft.Dafny.Triggers {
       return copy;

     }

 

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

+    internal class SetOfTerms {

+      internal bool IsRedundant { get; private set; }

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

+

+      private ISet<BoundVar> variables;

+      private Dictionary<BoundVar, TriggerTerm> termOwningAUniqueVar;

+      private Dictionary<TriggerTerm, ISet<BoundVar>> uniqueVarsOwnedByATerm;

+

+      public int Count { get { return Terms.Count; } }

+

+      private SetOfTerms() { }

+

+      internal TriggerCandidate ToTriggerCandidate() {

+        return new TriggerCandidate(Terms);

+      }

+      

+      internal static SetOfTerms Empty() {

+        var newSet = new SetOfTerms();

+        newSet.IsRedundant = false;

+        newSet.Terms = new List<TriggerTerm>();

+        newSet.variables = new HashSet<BoundVar>();

+        newSet.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>();

+        newSet.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>();

+        return newSet;

+      }

+

+      /// <summary>

+      /// 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. As it copies its

+      /// argument, this method updates various datastructures that allow it to

+      /// efficiently track ownership relations between formulae and bound variables,

+      /// and sets the IsRedundant flag of the returned set, allowing the caller to

+      /// discard that set of terms, and the ones that would have been built on top of

+      /// it, thus ensuring that the only sets of terms produced in the end are sets

+      /// of terms in which each element contributes (owns) at least one variable.

+      ///

+      /// Note that this is trickier than just checking every term for new variables;

+      /// indeed, a new term that does bring new variables in can make an existing

+      /// term redundant (see redundancy-detection-does-its-job-properly.dfy).

+      /// </summary>

+      internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet<BoundVar> relevantVariables) {

+        var copy = new SetOfTerms();

+        copy.Terms = new List<TriggerTerm>(Terms);

+        copy.variables = new HashSet<BoundVar>(variables);

+        copy.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>(termOwningAUniqueVar);

+        copy.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>(uniqueVarsOwnedByATerm);

+

+        copy.Terms.Add(term);

+

+        var varsInNewTerm = new HashSet<BoundVar>(term.BoundVars);

+        varsInNewTerm.IntersectWith(relevantVariables);

+

+        var ownedByNewTerm = new HashSet<BoundVar>();

+

+        // Check #0: does this term bring anything new?

+        copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv));

+        copy.variables.UnionWith(varsInNewTerm);

+        

+        // Check #1: does this term claiming ownership of all its variables cause another term to become useless?

+        foreach (var v in varsInNewTerm) {

+          TriggerTerm originalOwner;

+          if (copy.termOwningAUniqueVar.TryGetValue(v, out originalOwner)) {

+            var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner];

+            alsoOwnedByOriginalOwner.Remove(v);

+            if (!alsoOwnedByOriginalOwner.Any()) {

+              copy.IsRedundant = true;

+            }

+          } else {

+            ownedByNewTerm.Add(v);

+            copy.termOwningAUniqueVar[v] = term;

+          }

+        }

+

+        // Actually claim ownership

+        copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm;

+

+        return copy;

+      }

+    }

+

+    internal static IEnumerable<SetOfTerms> AllSubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, int offset, ISet<BoundVar> relevantVariables) {

       if (offset >= source.Count) {

-        yield return new List<T>();

+        yield return SetOfTerms.Empty();

         yield break;

       }

 

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

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

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

+      foreach (var subset in AllSubsets(source, predicate, offset + 1, relevantVariables)) {

+        var newSet = subset.CopyWithAdd(source[offset], relevantVariables);

+        if (!newSet.IsRedundant && predicate(subset, source[offset])) { // Fixme remove the predicate?

+          yield return newSet;

         }

-        yield return new List<T>(subset);

+        yield return subset;

       }

     }

 

-    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, predicate, 0)) {

+    internal static IEnumerable<SetOfTerms> AllNonEmptySubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, IEnumerable<BoundVar> relevantVariables) {

+      foreach (var subset in AllSubsets(source, predicate, 0, new HashSet<BoundVar>(relevantVariables))) {

         if (subset.Count > 0) {

           yield return subset;

         }

       }

     }

-

+    

     internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 69c47d90..d78bcb9e 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -11,6 +11,11 @@ namespace Microsoft.Dafny.Triggers {
     internal Expression Expr { get; set; }

     internal Expression OriginalExpr { get; set; }

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

+    internal IEnumerable<BoundVar> BoundVars {

+      get {

+        return Variables.Select(v => v as BoundVar).Where(v => v != null);

+      }

+    }

 

     public override string ToString() {

       return Printer.ExprToString(Expr); 

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 7922e88d..501cfa51 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1
 function-applications-are-triggers.dfy(11,9): Info: Selected triggers:

    {f(10)}, {f.requires(10)}

 function-applications-are-triggers.dfy(12,5): Info: Selected triggers:

-   {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}

+   {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)}

 

 Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy
new file mode 100644
index 00000000..df1d78c3
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

+

+// This tests checks for tricky cases of redundancy suppression when building

+// triggers.

+

+predicate P(x: int, y: int)

+predicate Q(x: int)

+predicate R(x: int)

+

+method M() {

+  // For this term, it is enough to order the terms by number of variables

+  assert forall x, y :: true || P(x, y) || Q(y) || R(x);

+  assert forall x, y :: true || Q(y) || P(x, y) || R(x);

+  assert forall x, y :: true || Q(y) || R(x) || P(x, y);

+}

+

+predicate PP(x: int, y: int, z: int)

+predicate QQ(x: int, y: int)

+predicate RR(x: int, y: int)

+predicate SS(x: int, y: int)

+

+method MM() {

+  // Not for this one, though

+  assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);

+}

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
new file mode 100644
index 00000000..78c9e7ca
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
@@ -0,0 +1,12 @@
+redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:

+   {R(x), Q(y)}, {P(x, y)}

+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:

+   {R(x), Q(y)}, {P(x, y)}

+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:

+   {P(x, y)}, {R(x), Q(y)}

+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+

+Dafny program verifier finished with 11 verified, 0 errors