Hi PPL-developers

I would be glad if you could help me find answers to the following questions:

1. Having software verification in mind (problems over integers) which abstract domain(s) (more precisely domains provided by PPL) provide good trade-off between complexity and expressiveness? 

2. In the article (http://bugseng.com/products/ppl/documentation/BagnaraRZH02.pdf), you mentioned that poly_hull_assign is different from upper_bound_assign for Polyhedra, but in the user manual I found the following text:


What are the differences between these two functions? Do they differ in precision? complexity?

3. What is the function corresponding to poly_hull_assign for Octagon?

Many thanks in advance
Bishoksan