Merge split quantifiers with same triggers into one

Group split quantifiers by what triggers they got, and merged them back
into one quantifier.

Source/Dafny/Triggers/QuantifierSplitter.cs

@@ -5,8 +5,10 @@
 using System.Linq;
 using System.Text;
 
-namespace Microsoft.Dafny.Triggers {
-  class QuantifierSplitter : BottomUpVisitor {
+namespace Microsoft.Dafny.Triggers
+{
+  class QuantifierSplitter : BottomUpVisitor
+  {
     /// This cache was introduced because some statements (notably calc) return the same SubExpression multiple times.
     /// This ended up causing an inconsistent situation when the calc statement's subexpressions contained the same quantifier 
     /// twice: on the first pass that quantifier got its SplitQuantifiers generated, and on the the second pass these 
@@ -21,7 +23,7 @@ class QuantifierSplitter : BottomUpVisitor {
         return BinaryExpr.Opcode.And;
       } else {
         throw new ArgumentException();
-      } 
+      }
     }
 
     // NOTE: If we wanted to split quantifiers as far as possible, it would be
@@ -35,14 +37,6 @@ class QuantifierSplitter : BottomUpVisitor {
       return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };
     }
 
-    private static Attributes CopyAttributes(Attributes source) {
-      if (source == null) {
-        return null;
-      } else {
-        return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev));
-      }
-    }
-
     internal static IEnumerable<Expression> SplitExpr(Expression expr, BinaryExpr.Opcode separator) {
       expr = expr.Resolved;
       var unary = expr as UnaryOpExpr;
@@ -81,7 +75,7 @@ class QuantifierSplitter : BottomUpVisitor {
         }
         foreach (var e in stream) {
           var tok = new NestedToken(quantifier.tok, e.tok);
-          yield return new ForallExpr(tok, ((ForallExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
+          yield return new ForallExpr(tok, ((ForallExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
         }
       } else if (quantifier is ExistsExpr) {
         IEnumerable<Expression> stream;
@@ -92,16 +86,16 @@ class QuantifierSplitter : BottomUpVisitor {
         }
         foreach (var e in stream) {
           var tok = new NestedToken(quantifier.tok, e.tok);
-          yield return new ExistsExpr(tok, ((ExistsExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
+          yield return new ExistsExpr(tok, ((ExistsExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
         }
       } else {
         yield return quantifier;
       }
     }
-    
+
     private static bool AllowsSplitting(ComprehensionExpr quantifier) {
       // allow split if attributes doesn't contains "split" or it is "split: true" and it is not an empty QuantifierExpr (boundvar.count>0)
-      bool splitAttr = true; 
+      bool splitAttr = true;
       return (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) && (quantifier.BoundVars.Count > 0);
     }
 

Source/Dafny/Triggers/QuantifiersCollection.cs

@@ -31,11 +31,13 @@ class QuantifierWithTriggers {
 
   class QuantifiersCollection {
     readonly ErrorReporter reporter;
-    readonly List<QuantifierWithTriggers> quantifiers;
+    readonly ComprehensionExpr expr;  //  the expression where the splits are originated from
+    List<QuantifierWithTriggers> quantifiers;
 
-    internal QuantifiersCollection(IEnumerable<ComprehensionExpr> quantifiers, ErrorReporter reporter) {
+    internal QuantifiersCollection(ComprehensionExpr expr, IEnumerable<ComprehensionExpr> quantifiers, ErrorReporter reporter) {
       Contract.Requires(quantifiers.All(q => !(q is QuantifierExpr) || ((QuantifierExpr)q).SplitQuantifier == null));
       this.reporter = reporter;
+      this.expr = expr; 
       this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList();
     }
 
@@ -45,6 +47,7 @@ class QuantifiersCollection {
       BuildDependenciesGraph();
       SuppressMatchingLoops();
       SelectTriggers();
+      CombineSplitQuantifier();
     }
 
     private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) {
@@ -151,6 +154,80 @@ class QuantifiersCollection {
       }
     }
 
+    internal class QuantifierGroup
+    {
+      internal QuantifierWithTriggers quantifier;
+      internal List<ComprehensionExpr> expressions;
+
+      public QuantifierGroup(QuantifierWithTriggers q, List<ComprehensionExpr> expressions) {
+        this.quantifier = q;
+        this.expressions = expressions;
+      }
+    }
+
+    // group split quantifier by what triggers they got, and merged them back into one quantifier.
+    private void CombineSplitQuantifier() {
+      if (quantifiers.Count > 1) {
+        List<QuantifierGroup> groups = new List<QuantifierGroup>();
+        groups.Add(new QuantifierGroup(quantifiers[0], new List<ComprehensionExpr> { quantifiers[0].quantifier }));
+        for (int i = 1; i < quantifiers.Count; i++) {
+          bool found = false;
+          for (int j = 0; j < groups.Count; j++) {
+            if (HasSameTriggers(quantifiers[i], groups[j].quantifier)) {
+              // belong to the same group
+              groups[j].expressions.Add(quantifiers[i].quantifier);
+              found = true;
+              break;
+            } 
+          }
+          if (!found) {
+            // start a new group
+            groups.Add(new QuantifierGroup(quantifiers[i], new List<ComprehensionExpr> { quantifiers[i].quantifier }));
+          }
+        }
+        if (groups.Count == quantifiers.Count) {
+          // have the same number of splits, so no splits are combined.
+          return;
+        }
+        // merge expressions in each group back to one quantifier.
+        List<QuantifierWithTriggers> list = new List<QuantifierWithTriggers>();
+        List<Expression> splits = new List<Expression>();
+        foreach (var group in groups) {
+          QuantifierWithTriggers q = group.quantifier;
+          if (q.quantifier is ForallExpr) {
+            ForallExpr quantifier = (ForallExpr)q.quantifier;
+            Expression expr = QuantifiersToExpression(quantifier.tok, BinaryExpr.ResolvedOpcode.And, group.expressions);
+            q.quantifier = new ForallExpr(quantifier.tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, expr, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
+          } else if (q.quantifier is ExistsExpr) {
+            ExistsExpr quantifier = (ExistsExpr)q.quantifier;
+            Expression expr = QuantifiersToExpression(quantifier.tok, BinaryExpr.ResolvedOpcode.Or, group.expressions);
+            q.quantifier = new ExistsExpr(quantifier.tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, expr, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
+          }
+          list.Add(q);
+          splits.Add(q.quantifier);
+        }
+        this.quantifiers = list;
+        Contract.Assert(this.expr is QuantifierExpr); // only QuantifierExpr has SplitQuantifier
+        ((QuantifierExpr)this.expr).SplitQuantifier = splits;
+      }
+    }
+
+    private bool HasSameTriggers(QuantifierWithTriggers one, QuantifierWithTriggers other) {
+      return TriggerUtils.SameLists(one.Candidates, other.Candidates, SameTriggerCandidate);
+    }
+
+    private static bool SameTriggerCandidate(TriggerCandidate arg1, TriggerCandidate arg2) {
+      return TriggerUtils.SameLists(arg1.Terms, arg2.Terms, TriggerTerm.Eq); 
+    }
+
+    private Expression QuantifiersToExpression(IToken tok, BinaryExpr.ResolvedOpcode op, List<ComprehensionExpr> expressions) {
+      var expr = expressions[0].Term;
+      for (int i = 1; i < expressions.Count; i++) {
+        expr = new BinaryExpr(tok, op, expr, expressions[i].Term);
+      }
+      return expr;
+    }
+
     private void CommitOne(QuantifierWithTriggers q, bool addHeader) {
       var errorLevel = ErrorLevel.Info;
       var msg = new StringBuilder();

Source/Dafny/Triggers/QuantifiersCollector.cs

@@ -25,16 +25,16 @@ internal class QuantifierCollector : TopDownVisitor<bool> {
       if (e != null && (e.BoundVars.Count > 0) && !quantifiers.Contains(e)) {
         if (e is SetComprehension || e is MapComprehension) {
           quantifiers.Add(e);
-          quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(e, 1), reporter));
+          quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(e, 1), reporter));
         } else if (e is ForallExpr || e is ExistsExpr) {
           var quantifier = e as QuantifierExpr;
           quantifiers.Add(quantifier);
           if (quantifier.SplitQuantifier != null) {
             var collection = quantifier.SplitQuantifier.Select(q => q as ComprehensionExpr).Where(q => q != null);
-            quantifierCollections.Add(new QuantifiersCollection(collection, reporter));
+            quantifierCollections.Add(new QuantifiersCollection(e, collection, reporter));
             quantifiers.UnionWith(quantifier.SplitQuantifier);
           } else {
-            quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));
+            quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(quantifier, 1), reporter));
           }
         }
       }

Source/Dafny/Triggers/TriggerUtils.cs

@@ -15,6 +15,14 @@ class TriggerUtils {
       return copy;
     }
 
+    public static Attributes CopyAttributes(Attributes source) {
+      if (source == null) {
+        return null;
+      } else {
+        return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev));
+      }
+    }
+
     internal class SetOfTerms {
       internal bool IsRedundant { get; private set; }
       internal List<TriggerTerm> Terms { get; set; }

Test/dafny0/AutoReq.dfy.expect

@@ -1,11 +1,5 @@
 AutoReq.dfy(247,4): Error: possible violation of function precondition
 AutoReq.dfy(239,13): Related location
-AutoReq.dfy(239,59): Related location
-Execution trace:
-    (0,0): anon0
-    (0,0): anon4_Else
-AutoReq.dfy(247,4): Error: possible violation of function precondition
-AutoReq.dfy(239,13): Related location
 AutoReq.dfy(239,35): Related location
 Execution trace:
     (0,0): anon0
@@ -49,4 +43,4 @@ Execution trace:
     (0,0): anon0
     (0,0): anon11_Then
 
-Dafny program verifier finished with 52 verified, 9 errors
+Dafny program verifier finished with 52 verified, 8 errors

Test/dafny0/TriggerInPredicate.dfy.expect

@@ -1,5 +1,4 @@
-TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)".
-TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z".
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y) && z".
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

Test/dafny4/git-issue2.dfy

@@ -0,0 +1,83 @@
+// RUN: %dafny /rprint:"%t.rprint" /print:"%t.print" /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type sp_state
+type operand = int
+
+function sp_op_const(c:int) : int { c }
+
+predicate {:opaque} InBounds(s:sp_state, o:operand, v:int)
+{
+    0 <= o < 0x1_0000_0000
+}
+
+lemma lemma_K_InBounds()
+    ensures forall s:sp_state :: 
+                InBounds(s, sp_op_const(0x428a2f98), 0x428a2f98) &&
+                InBounds(s, sp_op_const(0x71374491), 0x71374491) &&
+                InBounds(s, sp_op_const(0xb5c0fbcf), 0xb5c0fbcf) &&
+                InBounds(s, sp_op_const(0xe9b5dba5), 0xe9b5dba5) &&
+                InBounds(s, sp_op_const(0x3956c25b), 0x3956c25b) &&
+                InBounds(s, sp_op_const(0x59f111f1), 0x59f111f1) &&
+                InBounds(s, sp_op_const(0x923f82a4), 0x923f82a4) &&
+                InBounds(s, sp_op_const(0xab1c5ed5), 0xab1c5ed5) &&
+                InBounds(s, sp_op_const(0xd807aa98), 0xd807aa98) &&
+                InBounds(s, sp_op_const(0x12835b01), 0x12835b01) &&
+                InBounds(s, sp_op_const(0x243185be), 0x243185be) &&
+                InBounds(s, sp_op_const(0x550c7dc3), 0x550c7dc3) &&
+                InBounds(s, sp_op_const(0x72be5d74), 0x72be5d74) &&
+                InBounds(s, sp_op_const(0x80deb1fe), 0x80deb1fe) &&
+                InBounds(s, sp_op_const(0x9bdc06a7), 0x9bdc06a7) &&
+                InBounds(s, sp_op_const(0xc19bf174), 0xc19bf174) &&
+                InBounds(s, sp_op_const(0xe49b69c1), 0xe49b69c1) &&
+                InBounds(s, sp_op_const(0xefbe4786), 0xefbe4786) &&
+                InBounds(s, sp_op_const(0x0fc19dc6), 0x0fc19dc6) &&
+                InBounds(s, sp_op_const(0x240ca1cc), 0x240ca1cc) &&
+                InBounds(s, sp_op_const(0x2de92c6f), 0x2de92c6f) &&
+                InBounds(s, sp_op_const(0x4a7484aa), 0x4a7484aa) &&
+                InBounds(s, sp_op_const(0x5cb0a9dc), 0x5cb0a9dc) &&
+                InBounds(s, sp_op_const(0x76f988da), 0x76f988da) &&
+                InBounds(s, sp_op_const(0x983e5152), 0x983e5152) &&
+                InBounds(s, sp_op_const(0xa831c66d), 0xa831c66d) &&
+                InBounds(s, sp_op_const(0xb00327c8), 0xb00327c8) &&
+                InBounds(s, sp_op_const(0xbf597fc7), 0xbf597fc7) &&
+                InBounds(s, sp_op_const(0xc6e00bf3), 0xc6e00bf3) &&
+                InBounds(s, sp_op_const(0xd5a79147), 0xd5a79147) &&
+                InBounds(s, sp_op_const(0x06ca6351), 0x06ca6351) &&
+                InBounds(s, sp_op_const(0x14292967), 0x14292967) &&
+                InBounds(s, sp_op_const(0x27b70a85), 0x27b70a85) &&
+                InBounds(s, sp_op_const(0x2e1b2138), 0x2e1b2138) &&
+                InBounds(s, sp_op_const(0x4d2c6dfc), 0x4d2c6dfc) &&
+                InBounds(s, sp_op_const(0x53380d13), 0x53380d13) &&
+                InBounds(s, sp_op_const(0x650a7354), 0x650a7354) &&
+                InBounds(s, sp_op_const(0x766a0abb), 0x766a0abb) &&
+                InBounds(s, sp_op_const(0x81c2c92e), 0x81c2c92e) &&
+                InBounds(s, sp_op_const(0x92722c85), 0x92722c85) &&
+                InBounds(s, sp_op_const(0xa2bfe8a1), 0xa2bfe8a1) &&
+                InBounds(s, sp_op_const(0xa81a664b), 0xa81a664b) &&
+                InBounds(s, sp_op_const(0xc24b8b70), 0xc24b8b70) &&
+                InBounds(s, sp_op_const(0xc76c51a3), 0xc76c51a3) &&
+                InBounds(s, sp_op_const(0xd192e819), 0xd192e819) &&
+                InBounds(s, sp_op_const(0xd6990624), 0xd6990624) &&
+                InBounds(s, sp_op_const(0xf40e3585), 0xf40e3585) &&
+                InBounds(s, sp_op_const(0x106aa070), 0x106aa070) &&
+                InBounds(s, sp_op_const(0x19a4c116), 0x19a4c116) &&
+                InBounds(s, sp_op_const(0x1e376c08), 0x1e376c08) &&
+                InBounds(s, sp_op_const(0x2748774c), 0x2748774c) &&
+                InBounds(s, sp_op_const(0x34b0bcb5), 0x34b0bcb5) &&
+                InBounds(s, sp_op_const(0x391c0cb3), 0x391c0cb3) &&
+                InBounds(s, sp_op_const(0x4ed8aa4a), 0x4ed8aa4a) &&
+                InBounds(s, sp_op_const(0x5b9cca4f), 0x5b9cca4f) &&
+                InBounds(s, sp_op_const(0x682e6ff3), 0x682e6ff3) &&
+                InBounds(s, sp_op_const(0x748f82ee), 0x748f82ee) &&
+                InBounds(s, sp_op_const(0x78a5636f), 0x78a5636f) &&
+                InBounds(s, sp_op_const(0x84c87814), 0x84c87814) &&
+                InBounds(s, sp_op_const(0x8cc70208), 0x8cc70208) &&
+                InBounds(s, sp_op_const(0x90befffa), 0x90befffa) &&
+                InBounds(s, sp_op_const(0xa4506ceb), 0xa4506ceb) &&
+                InBounds(s, sp_op_const(0xbef9a3f7), 0xbef9a3f7) &&
+                InBounds(s, sp_op_const(0xc67178f2), 0xc67178f2) 
+{ reveal_InBounds(); }
+
+
+

Test/dafny4/git-issue2.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 5 verified, 0 errors

Test/triggers/function-applications-are-triggers.dfy.expect

@@ -1,10 +1,6 @@
 function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)}
-function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f.requires(10)":
-   Selected triggers:
-     {f(10)}, {f.requires(10)}, {P(f)}
-function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f(10) == 0":
-   Selected triggers:
-     {f(10)}, {f.requires(10)}, {P(f)}
+function-applications-are-triggers.dfy(10,9): Info: Selected triggers:
+   {f(10)}, {f.requires(10)}, {P(f)}
 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:

Test/triggers/loop-detection-messages--unit-tests.dfy.expect

@@ -9,28 +9,16 @@ loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f
 loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f(i) == g(i)":
    Selected triggers:
      {g(i)}, {f(i)}
-loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression "false ==> f(i) == f(i + 1)":
-   Selected triggers: {f(i)} (may loop with "f(i + 1)")
-   /!\ Suppressing loops would leave this expression without triggers.
-loop-detection-messages--unit-tests.dfy(16,9): Info: For expression "false ==> f(i) == f(i)":
-   Selected triggers: {f(i)}
-loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i + 1)":
-   Selected triggers: {f(i)} (may loop with "f(i + 1)")
-loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i)":
-   Selected triggers: {f(i)}
+loop-detection-messages--unit-tests.dfy(16,9): Warning: Selected triggers: {f(i)} (may loop with "f(i + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(17,9): Info: Selected triggers: {f(i)} (may loop with "f(i + 1)")
 loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}
 loop-detection-messages--unit-tests.dfy(20,9): Warning: /!\ No terms found to trigger on.
 loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for "false ==> f(i + 1) == 0". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
 loop-detection-messages--unit-tests.dfy(23,9): Info: Selected triggers: {f(j), f(i)}
 loop-detection-messages--unit-tests.dfy(24,9): Warning: /!\ No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> f(i) == f(i)":
-   Selected triggers: {g(j), f(i)}
-loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> g(j) == 0":
-   Selected triggers: {g(j), f(i)}
-loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> f(i) == f(i)":
-   /!\ No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> g(j + 1) == 0":
-   /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(25,9): Info: Selected triggers: {g(j), f(i)}
+loop-detection-messages--unit-tests.dfy(26,9): Warning: /!\ No trigger covering all quantified variables found.
 loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for "false ==> f(i) == f(i)". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
 loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for "false ==> f(i) == f(i)".