I'm in the process of writing a paper about my improvements to pip and I wanted to compare to the PPL implementation too. (At least, I'd like to compare the execution times. I probably won't be diving into source to find out which optimizations in isl have also been implemented in PPL.)

However, ppl_pips seems to produce incorrect results on some test cases. I'm using version products_root-2871-gc02e988. (The git repo does not appear to have any tags for the releases.)

For bart-big.pip, ppl_pips returns

Parameter N = (3*L + 64) div 256 if N >= 1 and -3*L + 256*N >= 64 then {-K + M ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - N} else _|_

Which essentially means that it only found a solutions for L = 64, while there should be a solution for every value of L in the context.

For bouleti.pip, ppl_pips returns

_|_

That is, it claims that there is no solution, while isl_pip and PipLib's exampleMP do find solutions. Here is one of them: [p0, p1, p2, p3, p4, p5] -> { [1, 11, 4, 1, 2, 1, 2, 2, 1] : p3 = 1 and p4 = 11 and p5 = 2 and p0 = 0 and p1 = 0 and p2 = 2 }

The following iscc session demonstrates that this is indeed a solution

Q := 24 17 1 0 0 0 -1 0 0 0 0 0 1 -1 1 0 0 0 0 1 0 0 0 0 0 0 -1 0 0 1 -1 1 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 1 -1 1 0 0 0 0 1 0 0 0 0 0 0 0 -1 0 1 -1 1 0 0 0 0 1 0 0 0 0 0 1 0 0 0 -1 1 0 -1 0 0 0 1 -1 0 0 0 0 0 0 0 0 1 -1 0 1 0 0 0 1 0 -1 0 0 0 0 0 0 0 1 -1 0 0 1 0 0 1 0 0 1 0 0 0 0 0 0 -1 1 0 0 0 -1 -1 1 0 0 0 1 0 0 0 0 0 -1 0 0 0 0 0 -1 1 0 0 0 1 1 -1 0 0 0 -1 0 0 0 0 0 0 1 0 0 -1 0 0 0 2 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 0 -1 0 0 0 0 0 -1 1 0 0 0 0 0 0 1 1 -1 -1 0 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 -1 1 0 0 0 0 0 0 0 1 0 -1 0 0 0 0 0 -1 1 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 -1 1 0 0 0 0 0 0 0 0 1 -1 0 0 0 0 0 -1 1 1 1 0 0 0 0 0 0 0 -2 2 0 -1 -1 0 0 1 0 0 0 2 0 0 0 0 0 -2 1 0 0 0 -1 0 1 0 -1 0 0 0 0 0 4 3 -6 0 0 0 0 0 0 1 0 0 0 0 4 3 0 0 0 -7 1 0 0 -1 0 0 1 1 1 1 0 0 0 -2 -4 -4 7 0 0 0 0 0 0 1 0 0 0 -2 -4 -4 0 0 0 10 -3 0 1 1 1 0 1 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 ; {[1, 11, 4, 1, 2, 1, 2, 2, 1, 0, 0, 2, 1, 11, 2]} <= Q; True C := 1 8 1 0 -1 1 0 0 0 -1 ; {[0, 0, 2, 1, 11, 2]} <= C; True

Also, I wonder if you have a parser for the output format of ppl_pips so that I could compare the results produced by ppl_pips with those produced by isl_pip.

skimo