Peter Schneider-Kamp wrote:
thanks for your quick help! This indeed solved our problem.
Good!
Right now we are using ppl with cTI to compare our Prolog termination analysis to that of cTI. We actually had to resort back to ppl 0.6 because there seems to have been a change in the interface used by cTI. Are there many drawbacks when using 0.6 compared to 0.8?
You should definitely use PPL 0.8. You will find a pre-release of cTI 1.1 in
ftp://ftp.cs.unipr.it/pub/cTI/snapshots/cTI-1.1pre1.tar.gz
This supports (actually, it requires) PPL 0.8. Please, let us know if it works for you.
The speedup from SICStus clpq to ppl is up to 50000 times. Very impressive. So, for fair evaluation we needed to get ppl to perform.
I understand.
For our own termination analyser we indeed do not know how to use it (yet). The finite domain constraints we have to solve are inherently non-linear. Do you have any ideas/pointers how one can deal with non-linear constraints?
Can you tell us more about these constraints? There are many different ways of giving up linearity.
Can ppl handle some kinds of non-linearism?
PPL 0.8 offers the Polyhedra_Powerset construction, which you can instantiate over general (not necessarily closed) convex polyhedra and bounded-difference shapes. Our experiments on powersets of bounded-difference shapes shows that this domain has very good scalability on the problem of deriving inter-argument size relations for Prolog programs (i.e., the analysis terminates in reasonable time for all the Prolog programs in the China benchmark suite, and this includes several "monsters").
Since yesterday, the CVS HEAD version of the PPL offers a domain of rational grids (see http://www.cs.unipr.it/ppl/abstractions). As far as we know, this is the first time a _complete_ domain of rational grids (e.g., with a provably correct widening operator) is made available to the public. (Of course, the Grid domain can be the argument of the Polyhedra_Powerset construction.)
Another way the PPL can be used for the analysis of non-linear relations is by translation of systems of (low-degree) polynomial constraint inequalities to convex polyhedra. Some preliminary results are reported in the [BRCZ05a] and [BRCZ05b] items of
http://www.cs.unipr.it/ppl/Documentation/citations
If you can give us more details about your constraints, we will try to be helpful. All the best,
Roberto