From c55cb226f4de90b080aa809d883d52c3386db063 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 26 Aug 2015 18:36:34 -0700 Subject: 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. --- .../redundancy-detection-is-bidirectional.dfy | 29 ++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy (limited to 'Test/triggers/redundancy-detection-is-bidirectional.dfy') 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); +} -- cgit v1.2.3 From 7a993f6c87eaa82f383b1c5e7411f1878d4edf30 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 16:10:25 -0700 Subject: Small fix: there is no loop in (forall x :: Q(x) && Q(0)) Again, spotted by Chris :) --- Source/Dafny/Triggers/QuantifiersCollection.cs | 4 +++- Source/Dafny/Triggers/TriggerExtensions.cs | 8 ++++---- Test/triggers/redundancy-detection-is-bidirectional.dfy | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) (limited to 'Test/triggers/redundancy-detection-is-bidirectional.dfy') 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 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 holes, Dictionary 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) -- cgit v1.2.3