[PPL-devel] Octagon Closure on Half Matrix Form

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