On 08/14/2017 07:00 PM, j.c.vandepol@utwente.nl wrote:

Dear Enea,

Thanks, this is going to help a lot! Where can I find a list of all PPL-Prolog predicates? I didn’t find this particular one in http://bugseng.com/products/ppl/documentation//user/ppl-user-prolog-interfac... (well, apparently I can replace “Polyhedron” in ppl_Polyhedron_difference_assign by anything I need?)

Some domains support different sets of operators. If you have compiled the library from sources, then in the build directory, under interfaces/Prolog you should find several .hh files, where you can see the names of the foreign predicates. These header files are named according to the *instantiations* of the abstract domains that have been enabled at configuration time (using --enable-instantiations). By default (i.e., if you have enable the Prolog interface without chosing instantiations) you should see something like the following ppl_prolog_BD_Shape_double.hh ppl_prolog_BD_Shape_mpq_class.hh ppl_prolog_BD_Shape_mpz_class.hh ppl_prolog_Constraints_Product_C_Polyhedron_Grid.hh ppl_prolog_domains.hh ppl_prolog_Double_Box.hh ppl_prolog_Grid.hh ppl_prolog_Octagonal_Shape_double.hh ppl_prolog_Octagonal_Shape_mpq_class.hh ppl_prolog_Octagonal_Shape_mpz_class.hh ppl_prolog_Pointset_Powerset_C_Polyhedron.hh ppl_prolog_Pointset_Powerset_NNC_Polyhedron.hh ppl_prolog_Polyhedron.hh ppl_prolog_Rational_Box.hh Hope this is enough to put you on the right track. Cheers, Enea.

Kind regards, Jaco van de Pol

...

On 14 Aug 2017, at 18:53, Enea Zaffanella <zaffanella@cs.unipr.it <mailto:zaffanella@cs.unipr.it>> wrote:

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 <http://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

-- 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>