isl 0.18 was released containing various improvements:
-
Improve elimination of redundant existentially quantified variables
In particular, finally implement the Omega test in isl. A more powerful (and more expensive) version of the Omega test was supposed to have been implemented already, but it missed some cases. Those cases are now also handled. For example, the set description
{ [m, w] : exists a : w - 2m - 5 <= 3a <= m - 2w }
is now simplified to{ [m, w] : w <= 1 + m }
. -
Improve coalescing
In particular, the following set descriptions are now also coalesced
{ [a, b] : 0 <= a <= 2 and b >= 0 and ((0 < b <= 13) or (2*floor((a + b)/2) >= -5 + a + 2b)) } { [a] : (2 <= a <= 5) or (a mod 2 = 1 and 1 <= a <= 5) } { [y, x] : (x - y) mod 3 = 2 and 2 <= y <= 200 and 0 <= x <= 2; [1, 0] } { [x, y] : (x - y) mod 3 = 2 and 2 <= y <= 200 and 0 <= x <= 2; [0, 1] } { [1, y] : -1 <= y <= 1; [x, -x] : 0 <= x <= 1 } { [1, y] : 0 <= y <= 1; [x, -x] : 0 <= x <= 1 } { [x, y] : 0 <= x <= 10 and x - 4*floor(x/4) <= 1 and y <= 0; [x, y] : 0 <= x <= 10 and x - 4*floor(x/4) > 1 and y <= 0; [x, y] : 0 <= x <= 10 and x - 5*floor(x/5) <= 1 and 0 < y; [x, y] : 0 <= x <= 10 and x - 5*floor(x/5) > 1 and 0 < y } { [x, 0] : 0 <= x <= 10 and x mod 2 = 0; [x, 0] : 0 <= x <= 10 and x mod 2 = 1; [x, y] : 0 <= x <= 10 and 1 <= y <= 10 }
-
Improve parametric integer programming
Based on analysis of a test case reported by Wenlei Bao, a major cause of the long run-time turned out to be the symmetry detection performed internally. The detected symmetry is exploited by replacing several upper bounds with a single additional parameter. This helps to speed up lexicographic optimization of some inputs with lots of symmetry, but causes a significant slow-down on this particular input because the parameters that appear in the replaced constraints may also appear in other constraints and through the replacement, the connection is lost. The symmetry detection is now only applied in cases where this problem does not occur.
A further analysis showed that quite some time was spent in exploring parts of the domain where the optimum is undefined. In a pure lexicographic optimization operation, the user is not interested in this part of the domain. The procedure was changed to start from the actual domain of the input rather than the corresponding universe such that the complement no longer needs to be explored at all. A possible down-side is that this actual domain may involve existentially quantified variables, which increases the dimension of the context and which may also appear in the final result. Special care therefore needs to be taking for the case where lexicographic optimization is being used for its side-effect of eliminating existentially quantified variables.
The upshot is that for the input
{ S_2[i, k, j] -> [o0, o1, o2, o3] : exists (e0 = floor((o1)/8): 8e0 = o1 and k <= 255 and o0 <= 255 and o2 <= 255 and o3 <= 255 - j and 7o3 >= 255 - j and 7o3 <= 7 - i and 240o3 <= 239 + o0 and 247o3 <= 247 + k - j and 247o3 <= 247 + k - o1 and 247o3 <= 247 + i and 248o3 >= 248 - o1 and 248o3 <= o2 and 254o3 >= i - o0 + o1 and 254o3 >= -o0 + o1 and 255o3 >= -i + o0 - o1 and 1792o3 >= -63736 + 257o1) }
the computation time went down from
real 6m36.786s user 6m36.032s sys 0m0.128s
to
real 0m0.040s user 0m0.032s sys 0m0.000s
-
preserve
isolate
option inisl_schedule_node_band_split
This is needed to simplify the implementation of full/partial tile separation for hybrid tiling in PPCG.
-
Print AST nodes in YAML format
-
Minor improvements to Python bindings