Does ELINA support the join and meet operators in case of the NNC Polyhedra?

[GgnDpSngh]

Hi there,

No, currently we do not support NNC Polyhedra.

Cheers, Gagandeep Singh

[val-co]

Can Polyhedra of different dimensions (but topologically closed) be joined using this library? Or does the number of dimensions have to be the same?

[GgnDpSngh]

Hi,

Yes, it is possible. You can add extra unconstrained dimensions to the smaller polyhedron by using "elina_abstract0_add_dimensions" with "project" flag set to false and applying the join function from ELINA.

Cheers, Gagandeep Singh

[val-co]

Also, are there any plans to provide a python interface of the polyhedra domain with the join and meet operators?

[GgnDpSngh]

Sorry for the delay, I did not see it but you can call the polyhedra domain from the Python interface (https://github.com/eth-sri/ELINA/blob/master/python_interface/opt_pk.py).

[val-co]

Thank you! Is this also the case with the join and meet operators for polyhedra?

[GgnDpSngh]

Yes, see the examples here: https://github.com/eth-sri/ELINA/blob/master/python_interface/tests/elina_pk_test.py

[valco79]

Last question - If I have a polyhedra defined by four variables x1, x2, x3 and x4 and I want to "decompose" this into two smaller polyhedra with variables x1, x2, x4 and variables x4, x2, then is this possible in ELINA (python)?

[GgnDpSngh]

It will automatically compute the decomposition, e.g., if you start with a top element and add the constraints {x1-x2<=0, x3+5x4>=0} using the meet_lincons then it will create a decomposed polyhedron with the partition you mentioned above (similar behavior with other transformers like assignments). However, if the polyhedron is not decomposable (e.g., you add the constraint x1+x2-x3-x4<=0), then it is not possible to force a particular decomposition!

[valco79]

If I have the same polyhedra defined by four variables x1, x2, x3 and x4, can I instead remove the dimension x3 to get one of my partitions as above (python) ? Can the polyhedra be transformed from 4 to 3 dimensions this way?

[GgnDpSngh]

Yes, you can use the remove_dimension function to do that!