Hello.

The PPL encodes some forms of logical statements as constraints. "a = 5" can be encoded as a Constraint object as follows (in the appropriate context, assuming you are using the C++ interface):

Variable a(0);

Constraint c(a == 5);

There is no way to compute the complement of an equality constraint, because it is not a hyper/half space (it is the union of two open half-spaces).

You can compute the two half-spaces separately: the constraint above is encoded as "a - 5 == 0".
You can tale the underlying linear expression (a - 5) and use it to construct the two open half-spaces
(a - 5 < 0 and a - 5 > 0).

Hope my answer is clear enough.

Enea.

On 02/25/2016 07:17 PM, Rao,Nakul I wrote:

Hi

I am using Parma Polyhedra library in a Formal Verification project. I was unable to find a function that computes the complement of a logical equation.

For example, complement of a=5 will be a!=5.

Could you tell me how I could do this.

Thanks and Regards

Nakul
_______________________________________________
PPL-devel mailing list
PPL-devel@cs.unipr.it
http://www.cs.unipr.it/mailman/listinfo/ppl-devel