isl_tab_basic_map_partial_lexopt: detect modulos and integer divisions earlier
commit4d3b232895b23992afdae6ddbffdf503619ee8f3
authorSven Verdoolaege <sven@cerebras.net>
Fri, 17 Mar 2023 10:08:15 +0000 (17 11:08 +0100)
committerSven Verdoolaege <sven@cerebras.net>
Sat, 25 May 2024 15:31:27 +0000 (25 17:31 +0200)
tree0e10dbeae75013d8784c489a896d71a573814b32
parent9f2afbda68297894159f302c7922205c9314baf6
isl_tab_basic_map_partial_lexopt: detect modulos and integer divisions earlier

In particular, perform the detection before (potentially) extracting
the domain.  In cases where the domain is indeed extracted from
the basic map, this can result in a more structured representation
of the extracted domain.
If the domain is extracted first, then it may involve
existentially quantified variables corresponding
to the original output variables,
but the connection to those original output variables is lost.
The existentially quantified variables then remain in the domain
even if some information is later discovered about the output variables.
If modulos are detected first, then the originally implicit information
about the modulos is also made explicitly available in the domain.

This is useful both for the currently detected modulos as well as
for the additional forms of modulos that will be detected
in an upcoming commit.
For example, without this change, computing the lexicographic minimum
of { [a=0:71] -> [b=0:7] : (a - 3 * b + 21) % 24 >= 21 }
would produce

    { [a] -> [(floor((a)/3) - 8*floor((a)/24))] :
        exists (e0: 0 <= a <= 71 and 0 <= e0 <= 7 and
                24*floor((-3 + a - 3e0)/24) <= -24 + a - 3e0) }

after the upcoming commit instead of the simpler

    { [a] -> [(floor((a)/3) - 8*floor((a)/24))] : 0 <= a <= 71 }

that is obtained with the change in this commit.

Signed-off-by: Sven Verdoolaege <sven@cerebras.net>
isl_tab_lexopt_templ.c