From 5176621e39435ddda9293b8ad0968cf1d7639fb6 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 20 Aug 2015 16:36:21 -0700
Subject: Implement the SelectTrigger method, removing redundant triggers.

The idea is that we define an partial order on triggers (which may contain
multiple terms), and find all the maximal elements. The algorithm as
implemented is rather inefficient; in particular, is does not look at the
structure of the graph of the relation (thus is does many redundant
comparisons). See triggers/useless-triggers-are-removed.dfy for an example
where such a filter is useful.
---
 Test/triggers/useless-triggers-are-removed.dfy     | 25 ++++++++++++++++++++++
 .../useless-triggers-are-removed.dfy.expect        | 17 +++++++++++++++
 2 files changed, 42 insertions(+)
 create mode 100644 Test/triggers/useless-triggers-are-removed.dfy
 create mode 100644 Test/triggers/useless-triggers-are-removed.dfy.expect

(limited to 'Test/triggers')

diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy
new file mode 100644
index 00000000..16458e41
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that Dafny does get rid of redundant triggers before
+// annotating a quantifier, and that ths process does not interfere with cycle
+// detection.
+
+function f(x: int): int
+function g(x: int): int
+function h(x: int): int
+
+method M()
+  // In the following, only f(x) is kept. Note that the subset enumeration was
+  // already smart enough to not build any trigger with multiple terms (it only
+  // built 5 candidates)
+  requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0
+
+  // Loop detection still works fine: in the following example, the trigger is
+  // f(f(x))
+  requires forall x: int :: f(x) == f(f(x))
+
+  // This works for multi-triggers, too:
+  requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0
+{
+}
diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
new file mode 100644
index 00000000..6c2c0a2b
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -0,0 +1,17 @@
+useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}
+ Rejected triggers:
+   {h(g(f(x)))} (stronger than {g(f(x))}, {f(x)})
+   {g(h(f(x)))} (stronger than {h(f(x))}, {f(x)})
+   {h(f(x))} (stronger than {f(x)})
+   {g(f(x))} (stronger than {f(x)})
+useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}
+ Rejected triggers: {f(x)} (loops with {f(f(x))})
+useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:
+   {g(f(x)), g(y)}, {f(y), f(x)}
+ Rejected triggers:
+   {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})
+   {g(f(x)), g(f(y))} (stronger than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})
+   {g(f(x)), f(y)} (stronger than {f(y), f(x)})
+   {g(f(y)), f(x)} (stronger than {f(y), f(x)})
+
+Dafny program verifier finished with 5 verified, 0 errors
-- 
cgit v1.2.3