[mlir][Presburger] Add IntegerRelation::gist (context-based simplification)
Add IntegerRelation::gist(context), a port of ISL's isl_basic_map_gist
(uset_gist / uset_gist_full). It replaces the relation S by a relation
S' such that S' ∩ context == S ∩ context, with as few constraints as
possible: constraints of S that are implied by the context together with
the remaining constraints of S are removed, and the remaining constraints
may be rewritten using the equalities of the context. Outside of the
context S' may differ from S, so the result is only meaningful together
with the context. The result has at most as many constraints as S
(except that the constraints defining a division that is still used may
be restored, see below), never more local variables, and never involves
variables that S does not involve; in particular, locals of the context
are never introduced.
Trivial cases: an obviously empty context yields the universe; if the
intersection with the context is found to be empty later (inconsistent
combined equalities, a context that turns out to be rationally empty, or
an empty combined Simplex), the result is empty; an obviously empty S
[43 lines not shown]
[mlir][Presburger] Add PresburgerRelation::gist
Add PresburgerRelation::gist (and PresburgerSet forwarding overloads)
for a convex context and for a context that is itself a union of
disjuncts, following ISL's isl_map_gist / isl_map_gist_basic_map.
For a convex context, each disjunct is simplified separately with
IntegerRelation::gist; disjuncts that become empty are dropped and if any
disjunct becomes the universe, the universe is returned.
For a non-convex context, the trivial cases (universe set or context,
empty context, equal set and context, context being a subset of the
set) are handled first. Otherwise, the context is approximated by a
convex set. Instead of ISL's unshifted simple hull of the context and the
set, we use the universe together with all constraints of the disjuncts
of the context and of the set that are valid for every disjunct of the
context (checked with Simplex); including the constraints of the set
allows removing constraints that are implied by every disjunct of the
context even if they are not implied by the simple hull.
[mlir][Presburger] Add IntegerRelation::reduceUsingEqualities helper
Add a protected helper that rewrites all constraints of a relation using
the equalities of another relation in the same space, without changing
the intersection of the two. This is a port of ISL's
isl_basic_set_reduce_using_equalities together with
project_onto_involved: the equalities are first projected onto the
variables that occur in the relation being reduced, so that no new
variables (in particular, no locals of the other relation) are
introduced, and each remaining equality is then used to eliminate its
last variable with a non-zero coefficient from every constraint, so that
later variables (locals) are eliminated in favor of earlier ones.
This is a building block for context-based simplification (gist) and is
exercised by the gist tests added in a follow-up commit, since there is
no existing pattern for unit-testing protected members of
IntegerRelation.
[mlir][Presburger] NFC: factor out removeRedundantConstraintsFromSimplex
Split the compaction loops of IntegerRelation::removeRedundantConstraints
into a new protected helper, removeRedundantConstraintsFromSimplex, which
removes the constraints of the relation that are marked redundant in a
given Simplex, where the relation's constraints start at a given offset
in the Simplex (inequalities first, then each equality as a pair).
This allows reusing the same compaction logic when the relation's
constraints have been added to a Simplex that already contains other
constraints, e.g., for context-based simplification (gist), where the
context's constraints come first and are never marked redundant.
[mlir][Presburger] Add PresburgerRelation::gist
Add PresburgerRelation::gist (and PresburgerSet forwarding overloads)
for a convex context and for a context that is itself a union of
disjuncts, following ISL's isl_map_gist / isl_map_gist_basic_map.
For a convex context, each disjunct is simplified separately with
IntegerRelation::gist; disjuncts that become empty are dropped and if any
disjunct becomes the universe, the universe is returned.
For a non-convex context, the trivial cases (universe set or context,
empty context, equal set and context, context being a subset of the
set) are handled first. Otherwise, the context is approximated by a
convex set. Instead of ISL's unshifted simple hull of the context and the
set, we use the universe together with all constraints of the disjuncts
of the context and of the set that are valid for every disjunct of the
context (checked with Simplex); including the constraints of the set
allows removing constraints that are implied by every disjunct of the
context even if they are not implied by the simple hull.
[mlir][Presburger] Add IntegerRelation::gist (context-based simplification)
Add IntegerRelation::gist(context), a port of ISL's isl_basic_map_gist
(uset_gist / uset_gist_full). It replaces the relation S by a relation
S' such that S' ∩ context == S ∩ context, with as few constraints as
possible: constraints of S that are implied by the context together with
the remaining constraints of S are removed, and the remaining constraints
may be rewritten using the equalities of the context. Outside of the
context S' may differ from S, so the result is only meaningful together
with the context. The result has at most as many constraints as S
(except that the constraints defining a division that is still used may
be restored, see below), never more local variables, and never involves
variables that S does not involve; in particular, locals of the context
are never introduced.
Trivial cases: an obviously empty context yields the universe; if the
intersection with the context is found to be empty later (inconsistent
combined equalities, a context that turns out to be rationally empty, or
an empty combined Simplex), the result is empty; an obviously empty S
[43 lines not shown]
