Hello, dear PPL developers,
I have a naive question.
I there built-in function in PPL to test whether an abstract domain has universe dimension (i.e. \top) at index 'k'?
For now, the best that I can imagine is to unconstraint dimension 'k' and check whether the original one and the one with dimension 'k' unconstrained equals. I guess this is not the right way in PPL. In addition, maybe 'unconstrain' is approximative, to test equality between the original and the unconstraint does not make sense?
What is your opinion?
Thank you for your help.
Zhoulai
p.s for info, I am using Java interface of PPL.
Hello Zhoulai.
On 07/04/13 07:18, Zhoulai wrote:
I there built-in function in PPL to test whether an abstract domain has universe dimension (i.e. \top) at index 'k'?
I guess you want to know if the k-th dimension is unconstrained.
The easiest thing is to test whether the line whose direction is the k-th dimension is subsumed. Kind regards,
Roberto
On 07/04/2013 08:19 AM, Roberto Bagnara wrote:
Hello Zhoulai.
On 07/04/13 07:18, Zhoulai wrote:
I there built-in function in PPL to test whether an abstract domain has universe dimension (i.e. \top) at index 'k'?
I guess you want to know if the k-th dimension is unconstrained.
The easiest thing is to test whether the line whose direction is the k-th dimension is subsumed. Kind regards,
Roberto
An even easier approach is to use method "constrains":
bool constrains(Variable var) const;
or better, since you are interested in the Java interface:
public native boolean constrains(Variable var);
Enea.
participants (3)
-
Enea Zaffanella -
Roberto Bagnara -
Zhoulai