[PPL-devel] Octagon Closure on Half Matrix Form

[Markus Kusano]

Hello,

After reading a few of the papers on the PPL improvments to the
Octagon domain, I have a question on reasoning about the equivalence
between the half-matrix and full-matrix strong closure algorithms.

Looking at the function `strong_closure_assign()` in
`Octagonal_Shape_templates.hh` my understanding is that it computes
the strong closure on the triangular (half) matrix twice. So, for each
of the k = 0..n steps it visits each cell in the half-matrix twice
which is the same as, in the full matrix, visiting each cell and its
coherent-cell.

Is my understanding correct? I am trying to reason about parallelizing
some of the Octagon algorithms.

Thanks a bunch,
Markus