[PPL-devel] Print dimensions

[Roberto Bagnara]

Enrico Oliosi wrote:
 > I have a last question: when I define my variables in my
 > toy language and print the constraints the library print
 > their dimensions and not the variables.
 > I.e.:
 >
 > myvar := 1 becomes A = 1
 >
 > I tried to replace the dimension with var-names but
 > I couldn't do it.
 > Is there a way to do it or I can only print the dimensions?

Dear Enrico,

I believe you are confusing the variables in your program,
with dimensions, variables and their printed names in the PPL.

Let me try to explain.

A dimension in the PPL is simply an unsigned integer.

A PPL variable is given by an object of type Variable
that essentially corresponds to a dimension.  The class Variable
in the PPL is there only to help with good software engineering
practices.  To summarize, if you write

    Variable x(1);

then `x' is a C++ variable of type `Variable' that corresponds
to the dimension numbered 1 (i.e., the second dimension, as
dimensions are numbered starting from 0).
If you then write

   cout << x;

the output will be "B" because the default output function
will print "A" for a (any) variable corresponding to dimension
0, "B" for  a (any) variable corresponding to dimension 1,
then "C", ..., "Z", "A1", "B1", ..., "Z1", "A2", ...

If you don't like this output function you can change it.
See the documentation and the source file `writevariable1.cc'
in the `tests' subdirectories for the exact details and examples.

The let us come to your example.  If I understand correctly,
you have written a static analyzer that reads a program
containing the statement

     myvar := 1

Presumably you associate this variable instance in the analyzed
program with dimensions 0 of some polyhedron.  When you print
the constraint(s) corresponding to the program point just after
the assignment, you obtain

     A = 1

that, in the light of the explanation above, should now be
unsurprising.

If you want

     myvar = 1

to be printed instead, then you should be able to reverse the process
whereby you associated a variable named "myvar" in your program to
dimension 0 of the polyhedron corresponding to that program point.
Then you can set the output function for Variable (see the
documentation of Variable::set_output_function()) so as to obtain what
you want.  Alternatively, you may even not use the PPL output operator
and build yours, even though this is probably not worth the effort in
your case.
All the best,

     Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it