[PPL-devel] Complement of a logical Equation
Enea Zaffanella
zaffanella at cs.unipr.it
Mon Feb 29 13:52:58 CET 2016
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 at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20160229/2eb3f5c9/attachment.htm>
More information about the PPL-devel
mailing list