of_list [(x_1, a_1);..; (x_n, a_n)] c builds the affine expression a_1 x_1 + ... + a_n x_n + c. Duplicates or zeros coefficients are accepted (for instance 2 x_0 + 0 x_1 + 3 x_0 is a valid input for 5 x_0).
Returns a list sorted in increasing order of Ident.compare without duplicates nor zeros.
compose le [v_1, l_1;...; v_n, l_n] replaces each variable v_i by l_i in l. No duplicates are allowed.
Returns one of the (non zero) coefficients in the linear expression (if any).
val pp : Stdlib.Format.formatter -> t -> unit