Adding a new variable and interval to Poly

[cwright7101]

(Help Request, not an issue with the library necessarily) I am using the library with C++ and don't have access to Apron.

I am wanting to insert a new variable with INT_MIN and INT_MAX interval constraints to a poly. (I know this example is simple, but I want to build on it to keep adding variables and relationships).

auto man_ = createManager(false); auto newVarlin = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, curSize); elina_linexpr0_set_coeff_scalar_int(newVarlin, curSize, 1); newVarlin->p.linterm[0].dim = curSize; elina_linexpr0_set_cst_interval_int(newVarlin, INT_MIN, INT_MAX); auto lincons = elina_lincons0_make(ELINA_CONS_SUPEQ, newVarlin, nullptr); auto lincons_array = elina_lincons0_array_make(1); lincons_array.p[0] = lincons; auto top = opt_pktop(man, curDims.realdim, curDims.intdim + 2); auto linPoly = opt_pk_meet_linconsarray(man.get(), false, top, &lincons_array); elina_lincons0_array_clear(&lincons_array); //(I know I don't have to convert and back again, but in my actual code I am doing a stuff in between) elina_lincons0_array_t arr0 = opt_pk_to_linconsarray(man, linPoly); elina_lincons0_array_fprint(stdout, &arr0, nullptr); fflush(stdout); elina_lincons0_array_clear(&arr0);

If I print the array as above, I will get something like:

1 array of constraints of size 1 0: x0 + 2147483647 >= 0

Is there a different way to do this to include both the INT_MIN and INT_MAX constraints? I am new to this library as well so feel free to point out misconceptions you see.

[GgnDpSngh]

Hi Christopher,

Thanks for your interest in using ELINA. If you want to obtain both bounds for the variable then you need to create two separate constraints for the bounds. Currently, your call adds only one constraint to the Polyhedra x+[INT_MIN, INT_MAX] >=0 which is soundly approximated in the result. Here would be a minimal example for your use case:

auto lincons_array = elina_lincons0_array_make(2); // adds x+INT_MIN>=0 auto newVarlin1 = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, curSize); elina_linexpr0_set_coeff_scalar_int(newVarlin1, curSize, 1); newVarlin1->p.linterm[0].dim = curSize; elina_linexpr0_set_cst_scalar_int(newVarlin1, INT_MIN); auto lincons1 = elina_lincons0_make(ELINA_CONS_SUPEQ, newVarlin1, nullptr); lincons_array.p[0] = lincons1;

//adds -x+INT_MAX>=0 auto newVarlin2 = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, curSize); elina_linexpr0_set_coeff_scalar_int(newVarlin2, curSize, -1); newVarlin2->p.linterm[0].dim = curSize; elina_linexpr0_set_cst_scalar_int(newVarlin2, INT_MAX); auto lincons2 = elina_lincons0_make(ELINA_CONS_SUPEQ, newVarlin2, nullptr); lincons_array.p[0] = lincons2;

Let me know if it works.

Cheers, Gagandeep Singh

[cwright7101]

Thank you very much! That works if I print the lincons array, but if I add to a pk and then convert back I am not getting what I expect. More context:

That works to give me the lincons_array I am expecting and I can print that using elina_lincons0_array_fprint(stdout, &lincons_array, nullptr);

auto man = createManager(false); auto currPoly = opt_pkbottom(man, 0, 0); auto curDims = opt_pkdimension(man, currPoly_); size_t curSize = 0; auto lincons_array = elina_lincons0_array_make(2); auto varMinLin = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, curSize); elina_linexpr0_set_coeff_scalar_int(varMinLin, curSize, 1); varMinLin->p.linterm[0].dim = curSize; elina_linexpr0_set_cst_scalar_int(varMinLin, INT_MIN); auto lincons1 = elina_lincons0_make(ELINA_CONS_SUPEQ, varMinLin, nullptr); lincons_array.p[0] = lincons1; auto varMaxLin = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, curSize); elina_linexpr0_set_coeff_scalar_int(varMaxLin, curSize, -1); varMaxLin->p.linterm[0].dim = curSize; elina_linexpr0_set_cst_scalar_int(varMaxLin, INT_MAX); auto lincons2 = elina_lincons0_make(ELINA_CONS_SUPEQ, varMaxLin, nullptr); lincons_array.p[1] = lincons2; elina_lincons0_array_fprint(stdout, &lincons_array, nullptr); fflush(stdout); and get the output:

2 array of constraints of size 2 0: x0 - 2147483648 >= 0 1: -x0 + 2147483647 >= 0 But, if I try to do a meet with a top state (or bottom state) with the same dimensions after the above code (So I create the lincons array as above and now want to add it to a pk array to pass that around):

if (opt_pk_isbottom(man, currPoly_)) { opt_pkfree(man, currPoly_); // no destruct auto on pktop // Add one var dim and 2 constraints? currPoly = opt_pktop(man, curDims.realdim + 1, curDims.intdim + 2); } else { auto dimadd = elina_dimchangealloc(1, 2); // tell which var the dimension is adding to? Constraints will be for var 0 dimadd->dim[0] = curSize; dimadd->dim[1] = curSize; currPoly = opt_pk_adddimensions(man, true, currPoly_, dimadd, false); elina_dimchange_free(dimadd); } auto linPoly = opt_pk_meet_linconsarray(man, false, currPoly_, &lincons_array); elina_lincons0_array_t arr0 = opt_pk_to_linconsarray(man, linPoly); elina_lincons0_array_fprint(stdout, &arr0, nullptr); fflush(stdout); elina_lincons0_array_clear(&arr0); elina_lincons0_array_clear(&lincons_array); opt_pkfree(man, linPoly); opt_pkfree(man, currPoly); freeManager(man);

I will get the output:

2 array of constraints of size 2 0: x0 - 2147483648 >= 0 1: -x0 + 2147483647 >= 0 1 array of constraints of size 1 0: -1 >= 0

So I guess my new question is how to add to a PK array, pass around the array as part of the state I create, and then meet/join etc and then convert to elina_lincons0_array_t for printing?

[GgnDpSngh]

Hi Christopher,

Your method is correct, however, the set of constraints you add are unsatisfiable as x0 cannot be less than or equal to 2147483647 and greater than or equal to 2147483648 simultaneously. If you changed the coefficients for the upper and the lower bounds, you will get a non-bottom polyhedron.

Let me know if this helps.

Cheers, Gagandeep Singh

[cwright7101]

Thanks for pointing out my stupidity :)