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.

1 files changed, 5 insertions, 12 deletions

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();

       }

     }