add isl_options_{get,set}_pip_symmetry
commit1879898775e3d10f23505a70ba7a3e6a3e8eba38
authorSven Verdoolaege <skimo@kotnet.org>
Wed, 8 Jun 2016 15:33:23 +0000 (8 17:33 +0200)
committerSven Verdoolaege <skimo@kotnet.org>
Fri, 10 Jun 2016 06:23:57 +0000 (10 08:23 +0200)
tree3584e4b958f17f794d42255202552a7c559ee083
parent05dfd4c793f97e046472cb50fbc8b82498358fe4
add isl_options_{get,set}_pip_symmetry

This allows users of the isl library to turn off symmetry detection.
Symmetry detection can result in a significant speed-up on some inputs.
For example, on testsets/pip/cnt_sum2.pip, isl_pip takes 0m20.656s
without symmetry detection and 0m1.540s with symmetry detection.
The representation of the result is also much smaller with symmetry detection.

However, symmetry detection introduces an extra parameter, which
may result in some computations taking much longer, even to the point
of offsetting the advantages of symmetry detection.
For example, for the binary relation

{ 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) }

reported by Wenlei Bao, lexicographic minimization takes
7m24.836s with symmetry detection and 0m0.304s without.
In particular, the minimization procedure seems to be taking
a lot more time exploring parts of the context based purely
on the parameters added by the symmetry detection,
introducing many extra integer divisions.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
doc/user.pod
include/isl/options.h
isl_options.c