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. --- .../function-applications-are-triggers.dfy.expect | 2 +- .../redundancy-detection-is-bidirectional.dfy | 29 ++++++++++++++++++++++ ...edundancy-detection-is-bidirectional.dfy.expect | 12 +++++++++ 3 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy.expect (limited to 'Test/triggers') diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 7922e88d..501cfa51 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1 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: - {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)} + {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)} Dafny program verifier finished with 2 verified, 0 errors 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); +} diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect new file mode 100644 index 00000000..78c9e7ca --- /dev/null +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect @@ -0,0 +1,12 @@ +redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers: + {R(x), Q(y)}, {P(x, y)} +redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers: + {R(x), Q(y)}, {P(x, y)} +redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers: + {P(x, y)}, {R(x), Q(y)} +redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} +redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} +redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} +redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} + +Dafny program verifier finished with 11 verified, 0 errors -- cgit v1.2.3