diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 16:36:21 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 16:36:21 -0700 |
| commit | 5176621e39435ddda9293b8ad0968cf1d7639fb6 (patch) | |
| tree | 822cc65b67f51afc548a36822416dc15ebcdb06e /Test/triggers | |
| parent | 5734c8b39065b73835092fc5ede4a7c589374be2 (diff) | |
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.
Diffstat (limited to 'Test/triggers')
| -rw-r--r-- | Test/triggers/useless-triggers-are-removed.dfy | 25 | ||||
| -rw-r--r-- | Test/triggers/useless-triggers-are-removed.dfy.expect | 17 |
2 files changed, 42 insertions, 0 deletions
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
|