Get relative bounds for dimensions

[skius]

I am looking for a way to extract relative bounds of a dimension to the other dimensions (in the Polyhedra domain), i.e. given the state { -i + x - 1 >= 0; i >= 0 } I ultimately want to get [0, x-1] as bounds for i. This is of course a straight-forward example, but what if there was additionally a lower bound for i of e.g. i >= y where y <= 5? Best case might be two conjunct constraints of [0, x-1] and [y, x-1]?

To implement this, I was looking for a function that gives respective bounds for a dimension, e.g. for i it might return { >= 0, >= y, <= x-1}

Is there a way to achieve this? Or perhaps a reason why it's not a good idea/feasible to implement this (be that in ELINA or externally)?

Thanks for the work on this library!

(PS: The reason I'm looking for this is because I'm trying to give more user-friendly bounds if a user asks "what values can i take" than throwing the full state at them, and more precise results than simply saying [0, +oo])

[GgnDpSngh]

Hi there,

Thanks for your comment. Currently, we can only provide the interval bounds for a variable. We directly do not support the desired functionality as we did not find any application in standard program analysis. However, it is possible to process the constraints obtained from the function "elina_abstract0_to_lincons0_array" to achieve the desired functionality. You can separate the constraints where your chosen variable has a positive coefficient and where it is negative. E.g. if one gets {2x-3y+1>=0, x-2y>=0, -x+4y>=2, x+y>=6 } then you can output y<={2/3x+1/3,x/2} and y>={x/4+1/2,6-x}.

Please let me know if there are any further questions.

Cheers, Gagandeep Singh

[skius]

Thank you, I'll try this approach.

Best