Further relax the loop detection conditions

Mismatches are now allowed up to expressions not involving any of the bound
variables of the quantifier under inspection.

3 files changed, 25 insertions, 8 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index b77afccb..50458ab7 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -101,8 +101,11 @@ namespace Microsoft.Dafny.Triggers {
       // [∀ 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). 

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

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

+      // In addition, we ignore cases where the only differences between a trigger

+      // and a trigger match are places where a variable is replaced with an 

+      // expression whose free variables do not intersect that of the quantifier 

+      // in which that expression is found. For examples of this behavious, see

+      // triggers/literals-do-not-cause-loops.

       // 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 dccd996d..d4a822a8 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -31,9 +31,15 @@ namespace Microsoft.Dafny.Triggers {
       return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr);

     }

 

-    internal bool CouldCauseLoops(List<TriggerTerm> terms) {

+    /// <summary>

+    ///  This method checks whether this match could actually cause a loop, given a set of terms participating in a trigger; 

+    ///  to compute an answer, we match the Expr of this match against the Exprs of each of these term, allowing for harmless 

+    ///  variations. If any of these tests does match, this term likely won't cause a loop.

+    ///  The boundVars list is useful to determine that forall x :: P(x) == P(y+z) does not loop.

+    /// </summary>

+    internal bool CouldCauseLoops(List<TriggerTerm> terms, ISet<BoundVar> boundVars) {

       var expr = Expr;

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

+      return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars));

     }

   }

 

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

     }

 

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

+    internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet<BoundVar> boundVars) {

       expr1 = expr1.Resolved;

       expr2 = expr2.Resolved;

 

       if (expr1 is IdentifierExpr) {

-        return expr2 is IdentifierExpr || expr2 is LiteralExpr;

+        if (expr2 is IdentifierExpr) {

+          return true;

+        } else {

+          var freeInE2 = Translator.ComputeFreeVariables(expr2);

+          freeInE2.IntersectWith(boundVars);

+          return !freeInE2.Any();

+        }

       }

 

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

+      return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, 

+        expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars));

     }

 

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

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index d78bcb9e..cc3b1978 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -69,7 +69,8 @@ namespace Microsoft.Dafny.Triggers {
     internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       var matchingSubterms = this.MatchingSubterms(quantifier);

-      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

+      var boundVars = new HashSet<BoundVar>(quantifier.BoundVars);

+      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars));

     }

 

     internal List<TriggerMatch> MatchingSubterms(QuantifierExpr quantifier) {