Simplification of quantifiers

[Lars van den Haak]

In an email conversation someone mentioned to me that your tool is to perform additional simplifications, in addition to SAT/UNSAT queries; 

for example, the ISL tool simplifies `forall i j, 0 <= i < N/4 /\ 0 <= j < 4 -> P(i * 4 + j)` into `forall i, 0 <= i < N -> P(i)`.

Is it described somewhere on how this simplification is done?
(And is it correct that your tool can do this?)

[Sven Verdoolaege]

If the notation above is meant to define a set (which would be
{ [x] : exists i,j : 0 <= 4*i < N /\ 0 <= j < 4 and x = i * 4 + j }
in isl notation), then isl manipulates such sets.
Internally, it does try to simpify the constraints,
but that's only to try and make the operations a bit more efficient.
I don't think I've ever written down exactly what it does
in terms of constraint simplification because I don't think
there is much new in it.
You can however use isl to check whether the two set descriptions
(if that is what they are) are the same:

[N] -> { [x] : exists i,j : 0 <= 4*i < N /\ 0 <= j < 4 and x = i * 4 + j } =
[N] -> { [i] : 0 <= i < N };
$0 := False

So, no they are not the same.
In particular, for N=1, the first set is { [0:3] },
while the second set is just { [0] }.

skimo