Basile STARYNKEVITCH wrote:

Hello Roberto & All,

I am really a very newbie in PPL. Just trying to use it right now (in the GCC MELT branch, if that does matter). So sorry for my very stupid (or at least basic) questions.

Any question is welcome.

First, is there somehere a tutorial or user FAQ page? More specifically, I'm looking for a 2-column table of "to do this, use that" rows which gives quick "overview" of the PPL. I don't mind if the "todo this" column contains a few math terms or equations and I would expect the "use that" column to contain names (and if possible HTML links) of C++ method signatures.

We do not have (yet?) a tutorial. We just started a FAQ on the web site (http://www.cs.unipr.it/ppl/FAQ), but it does not really fit with your questions above.

We have many test programs, but most of them are written in C++, whereas I understand you are more interested in the C interface. We have a demo program in demos/ppl_lpsol/ppl_lpsol.c, but this is mostly meant to test our MIP solver.

We do have manuals, produced using Doxygen. On the web page http://www.cs.unipr.it/ppl/Documentation/#user you can find several links pointing to manuals in various formats. For instance, for on-line (html) browsing for C++: http://www.cs.unipr.it/ppl/Documentation/user/ppl-user-0.10-html/ For C, http://www.cs.unipr.it/ppl/Documentation/user/ppl-user-c-interface-0.10-html...

Note that the main descriptions for the library operators can be found at the beginning of the C++ manual (what we call the *core* manual).

Also, is there somehere a summary of the C API, ie something like a table C++ API call, C API call?

In both manuals there are lists of relevant datatypes and, for each datatype, there is the list of corresponding functions/methods.

To avoid repetitions, the "configuration independent" C language interface manual only lists a subset of the set of datatypes that can be obtained via configuration options (in particular, you have a detailed description of all o fthe functions available for ppl_Polyhedron_t; if a different domain is selected, you might expect it will have a similar set of functions available).

At last, I would like to make a projection of a constraint system into a subset of its coordinates e.g. geometrically, projecting the 5-dimensional polyhedra defined by one constraint system over x,y,z,u,v into a constraint system over x,y,u (hence eliminating z & v). What is the API for such things?

Geometrically, projection boils down to the removal of space dimensions.

I'll try to provide a step-by-step explanation here below for someone using the C interface (something that I am not really used to).

Supposing you have your constraint system in variable cs, you first construct your polyhedron object using `cs_in':

ppl_Polyhedron_t ph; ppl_new_C_Polyhedron_from_Constraint_System(&ph, cs_in);

(This assumes that you want to preserve the contents of `cs_in'.) Then you need to build the set of variables to be projected away:

ppl_dimension_type to_be_removed[2]; to_be_removed[0] = z; to_be_removed[1] = v;

You are now ready to call the function doing the job:

ppl_Polyhedron_remove_space_dimensions(ph, to_be_removed, 2);

and access the result (in minimal form):

ppl_const_Constraint_System_t cs_out; ppl_Polyhedron_get_minimized_constraints(ph, &cs_out);

As mentioned in the main manual, you need to be careful, since after the call the resulting polyhedron will have just 3 dimensions and their names would not match the previous ones. For instance, if you started with x=0, y=1, z=2, u=3 and v=4, after projecting away z and v as done before you will end up with a polyhedron on the dimensions x=0, y=1 and z=2 (i.e., the remaining dimensions are automatically shifted).

Out of curiosity, I would guess (because I remember Roberto telling me about) that the PPL is indeed used for some static analysis of software tool. Is there any papers on that subject?

Regards

Well, you can find some links on applications using the PPL on the following page: http://www.cs.unipr.it/ppl/Applications/

Many of the listed applications are also described in published papers; see our bibliography of PPL citations at http://www.cs.unipr.it/ppl/Documentation/citations

I should also mention our paper that is going to appear on TCS: http://www.cs.unipr.it/~zaffanella/Papers/Abstracts/TCS09

Cheers, Enea.