20 December 2016

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 in isl_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