[PPL-devel] Normalization

[Roberto Bagnara]

Running China+PPL on our benchmark suite I observed
the following phenomenon: when the constraints of polyhedra
are printed I see, e.g., both

  B + C + D + E - F = -2,

and 

  -B - C - D - E + F = 2.

These constraints are equivalent and are also normalized
with our current notion of normalization.
In fact, gcd(1,-1,-2) = gcd(-1,1,2) = 1.

The question is: are we using too weak a notion of normalization?
What happens if, for equalities, we insist having a non-negative
inhomogeneous term?

Notice that, in some places, we are rather syntactic when dealing
with constraints.  For instance, in Matrix::merge_rows_assign()
we regard the above constraints as different and we get them
both in the result.
Any idea?
Ciao,

     Roberto

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