[PPL-devel] difference on pointset powerset

[Enea Zaffanella]

Hello.

The Pointset_Powerset domain has a difference_assign operator.
If I remember correctly, when instantiated to used NNC_Polyhedron,
the operator should be precise.

For instance:

pset1 = { A >= 0 }
pset2 = { B = 0, A = 0 }
pset1.difference_assign(pset2) = { A >= 0, B > 0 }, { A >= 0, -B > 0 }, 
{ B = 0, A > 0 }

Examples of its use (in the C++ interface) can be seen in

    tests/Powerset/difference1.cc

where, however, it is instantiated with the C_Polyhedron class.

As for the Prolog interface, this should be the foreign predicate to call:

extern "C" Prolog_foreign_return_type
   ppl_Pointset_Powerset_NNC_Polyhedron_difference_assign
   (Prolog_term_ref t_lhs, Prolog_term_ref t_rhs);

Let us know if it works as expected.

Cheers,
Enea.


On 08/08/2017 02:39 PM, j.c.vandepol at utwente.nl wrote:
> Dear developers of PPL,
>
> Is it possible to directly compute the set-difference of two pointset 
> powersets?
>
> In particular, I’m interested in the precise complement;
> convex difference approximations are not sufficient for my case.
>
> Kind regards,
> Jaco van de Pol
>
>
> -- 
> Prof. Jaco van de Pol
> University of Twente (NL)
> Formal Methods and Tools
> http://www.cs.utwente.nl/~vdpol <http://www.cs.utwente.nl/%7Evdpol>
>
>
>
> _______________________________________________
> 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/20170814/115584aa/attachment.htm>