Range.isCoveredBy

1 // Note that given two logical conditions A and B,
2 // "A implies B" is equivalent to (A == true) <= (B == true)
3 
4 auto target = This(12, 17);
5 This[] ranges;
6 
7 // neither tessellated nor covered
8 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
9 
10 ranges ~= [This(1, 5)];
11 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
12 ranges.length = 0;
13 assumeSafeAppend(ranges);
14 
15 ranges ~= [This(12, 15)];
16 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
17 ranges.length = 0;
18 assumeSafeAppend(ranges);
19 
20 ranges ~= [This(14, 17)];
21 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
22 ranges.length = 0;
23 assumeSafeAppend(ranges);
24 
25 ranges ~= [This(18, 25)];
26 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
27 ranges.length = 0;
28 assumeSafeAppend(ranges);
29 
30 ranges ~= [This(1, 5), This(19, 20)];
31 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
32 ranges.length = 0;
33 assumeSafeAppend(ranges);
34 
35 ranges ~= [This(1, 13), This(16, 20)];
36 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
37 ranges.length = 0;
38 assumeSafeAppend(ranges);
39 
40 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
41 
42 // covered, but not tessellated
43 ranges ~= [This(11, 17)];
44 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
45 ranges.length = 0;
46 assumeSafeAppend(ranges);
47 
48 ranges ~= [This(12, 18)];
49 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
50 ranges.length = 0;
51 assumeSafeAppend(ranges);
52 
53 ranges ~= [This(11, 18)];
54 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
55 ranges.length = 0;
56 assumeSafeAppend(ranges);
57 
58 ranges ~= [This(1, 15), This(14, 20)];
59 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
60 ranges.length = 0;
61 assumeSafeAppend(ranges);
62 
63 ranges ~= [This(12, 15), This(15, 17)];
64 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
65 ranges.length = 0;
66 assumeSafeAppend(ranges);
67 
68 ranges ~= [This(12, 16), This(14, 17)];
69 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
70 ranges.length = 0;
71 assumeSafeAppend(ranges);
72 
73 // tessellated
74 ranges ~= [This(12, 17)];
75 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
76 ranges.length = 0;
77 assumeSafeAppend(ranges);
78 
79 ranges ~= [This(12, 14), This(15, 17)];
80 test!("<=")(target.isTessellatedBy(ranges), target.isCoveredBy(ranges));
81 ranges.length = 0;
82 assumeSafeAppend(ranges);