Polyhedra domain does not set exactness flag correctly when calculating join

[Cu3PO42]

Hi Gagandeep,

I have run into another issue with the polyhedra domain. Consider the following two abstract values (with two dimensions each):

• x0 - x1 >= 0 ∧ x1 >= 0
• x0 >= 0 ∧ -x1 >= 0

Their join is given by x0 - x1 >= 0 ∧ x0 >= 0. ELINA calculates this correctly, but does not set the exactness flag to true, even though this is exact and not an over-approximation.

You can use the following code to reproduce this:

elina_manager_t *man = opt_pk_manager_alloc(false);
elina_funopt_t opt;
elina_funopt_init(&opt);
opt.flag_exact_wanted = true;
opt.algorithm = INT_MAX;
elina_manager_set_funopt(man, ELINA_FUNID_JOIN, &opt);

elina_abstract0_t *abs1 = elina_abstract0_top(man, 0, 2);
elina_abstract0_t *abs2 = elina_abstract0_top(man, 0, 2);

elina_linexpr0_t *expr1 = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 2);
elina_coeff_set_scalar_double(expr1->p.coeff, 1);
elina_coeff_set_scalar_double(expr1->p.coeff + 1, -1);

elina_linexpr0_t *expr2 = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 2);
elina_coeff_set_scalar_double(expr2->p.coeff + 1, 1);

elina_lincons0_array_t cons_array1 = elina_lincons0_array_make(2);
cons_array1.p[0] = elina_lincons0_make(ELINA_CONS_SUPEQ, expr1, NULL);
cons_array1.p[1] = elina_lincons0_make(ELINA_CONS_SUPEQ, expr2, NULL);

elina_linexpr0_t *expr3 = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 2);
elina_coeff_set_scalar_double(expr3->p.coeff, 1);

elina_linexpr0_t *expr4 = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 2);
elina_coeff_set_scalar_double(expr4->p.coeff + 1, -1);

elina_lincons0_array_t cons_array2 = elina_lincons0_array_make(2);
cons_array2.p[0] = elina_lincons0_make(ELINA_CONS_SUPEQ, expr3, NULL);
cons_array2.p[1] = elina_lincons0_make(ELINA_CONS_SUPEQ, expr4, NULL);

elina_abstract0_meet_lincons_array(man, true, abs1, &cons_array1);
elina_abstract0_meet_lincons_array(man, true, abs2, &cons_array2);

elina_abstract0_join(man, true, abs1, abs2);

printf("Was exact: %d", elina_manager_get_flag_exact(man));

Best regards,
Tobias