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@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@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel