Small fix: there is no loop in (forall x :: Q(x) && Q(0))

Again, spotted by Chris :)

3 files changed, 8 insertions, 6 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 114d5f5d..b77afccb 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -100,7 +100,9 @@ namespace Microsoft.Dafny.Triggers {
       // quantifier that matches one of the terms of the trigger (this ensures that

       // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even

       // ignore terms that almost match a trigger term, modulo a single variable

-      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop).

+      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). 

+      // The last thing that we ignore is matching variables against constants, 

+      // to ensure that P(x) is not flagged as looping with P(0).

       // This ignoring logic is implemented by the CouldCauseLoops method.

 

       foreach (var q in quantifiers) {

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index 71414eee..dccd996d 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -33,7 +33,7 @@ namespace Microsoft.Dafny.Triggers {
 

     internal bool CouldCauseLoops(List<TriggerTerm> terms) {

       var expr = Expr;

-      return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNames(expr));

+      return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNamesAndConstants(expr));

     }

   }

 

@@ -79,15 +79,15 @@ namespace Microsoft.Dafny.Triggers {
       return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2));

     }

 

-    internal static bool ExpressionEqModuloVariableNames(this Expression expr1, Expression expr2) {

+    internal static bool ExpressionEqModuloVariableNamesAndConstants(this Expression expr1, Expression expr2) {

       expr1 = expr1.Resolved;

       expr2 = expr2.Resolved;

 

       if (expr1 is IdentifierExpr) {

-        return expr2 is IdentifierExpr;

+        return expr2 is IdentifierExpr || expr2 is LiteralExpr;

       }

 

-      return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2));

+      return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNamesAndConstants(e1, e2));

     }

 

     internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet<BoundVar> holes, Dictionary<IVariable, Expression> bindings) {

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy
index df1d78c3..06541b70 100644
--- a/Test/triggers/redundancy-detection-is-bidirectional.dfy
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy
@@ -1,7 +1,7 @@
 // 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

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

 // triggers.

 

 predicate P(x: int, y: int)