[PPL-devel] difference on pointset powerset

[Enea Zaffanella]

On 08/14/2017 07:00 PM, j.c.vandepol at 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-interface-1.2-html/domains_predicates.html
> (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 at cs.unipr.it 
>> <mailto:zaffanella at 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 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
>>
>
> --
> 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>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20170814/cb3d25db/attachment.htm>