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