1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This test 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);
}
|
