Module: ppl/ppl Branch: master Commit: 6e74285860c8db3cd382da208e9c9042df406099 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6e74285860c8d...

Author: Patricia Hill p.m.hill@leeds.ac.uk Date: Wed Apr 1 09:31:06 2009 +0100

Changes to deal with //FIXME(0.10.1): the following is a bug! in src/Pointset_Powerset.templates.hh

As Grids are non-convex, the constructor for a powerset of nnc polyhedra from a powerset of grids has been implemented separately from the generic case. A test added to show that there was a bug which is now fixed.

The "//FIXME(0.10.1): ..." has been removed but a new FIXME added indicating this code will break if other non-convex or non-linear domains are added

---

src/Pointset_Powerset.cc | 15 +++++++++++++ src/Pointset_Powerset.defs.hh | 6 +++++ src/Pointset_Powerset.templates.hh | 12 +++++++++- tests/Powerset/fromgrid1.cc | 41 ++++++++++++++++++++++++++++++++++++ 4 files changed, 73 insertions(+), 1 deletions(-)

diff --git a/src/Pointset_Powerset.cc b/src/Pointset_Powerset.cc index ee2b119..e9933db 100644 --- a/src/Pointset_Powerset.cc +++ b/src/Pointset_Powerset.cc @@ -307,6 +307,21 @@ PPL::Pointset_PowersetPPL::NNC_Polyhedron

template <> template <> +PPL::Pointset_PowersetPPL::NNC_Polyhedron +::Pointset_Powerset(const Pointset_Powerset<Grid>& y, + Complexity_Class) + : Base(), space_dim(y.space_dimension()) { + Pointset_Powerset& x = *this; + for (Pointset_Powerset<Grid>::const_iterator i = y.begin(), + y_end = y.end(); i != y_end; ++i) + x.sequence.push_back(Determinate<NNC_Polyhedron> + (NNC_Polyhedron(i->element()))); + x.reduced = false; + assert(x.OK()); +} + +template <> +template <> PPL::Pointset_PowersetPPL::C_Polyhedron ::Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron>& y, Complexity_Class) diff --git a/src/Pointset_Powerset.defs.hh b/src/Pointset_Powerset.defs.hh index 4a9c94b..556beb9 100644 --- a/src/Pointset_Powerset.defs.hh +++ b/src/Pointset_Powerset.defs.hh @@ -1400,6 +1400,12 @@ Pointset_Powerset<NNC_Polyhedron>

template <> template <> +Pointset_Powerset<NNC_Polyhedron> +::Pointset_Powerset(const Pointset_Powerset<Grid>& y, + Complexity_Class); + +template <> +template <> Pointset_Powerset<C_Polyhedron> ::Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron>& y, Complexity_Class); diff --git a/src/Pointset_Powerset.templates.hh b/src/Pointset_Powerset.templates.hh index effdd6f..29196e4 100644 --- a/src/Pointset_Powerset.templates.hh +++ b/src/Pointset_Powerset.templates.hh @@ -65,8 +65,18 @@ Pointset_Powerset<NNC_Polyhedron> y_end = y.end(); i != y_end; ++i) x.sequence.push_back(Determinate<NNC_Polyhedron> (NNC_Polyhedron(i->element(), complexity))); - // FIXME(0.10.1): the following is a bug! + + // FIXME: If the domain elements can be represented _exactly_ as NNC + // polyhedra, then having x.reduced = y.reduced is correct. This is + // the case if the domains are both linear and convex which holds + // for all the currently supported instantiations except for + // Grids; for this reason the Grid specialization has a + // separate implementation. For any non-linear or non-convex + // domains (e.g., a domain of Intervals with restrictions or a + // domain of circles) that may be supported in the future, the + // assignment x.reduced = y.reduced will be a bug. x.reduced = y.reduced; + assert(x.OK()); }

diff --git a/tests/Powerset/fromgrid1.cc b/tests/Powerset/fromgrid1.cc index 3cbaa58..e8f5fc3 100644 --- a/tests/Powerset/fromgrid1.cc +++ b/tests/Powerset/fromgrid1.cc @@ -372,6 +372,46 @@ test15() { return ok; }

+// Constructs the powerset of NNC polyhedra from a powerset of grids +// where set of grids is omega reduced but the constructed set +// of NNC polyhedra is not omega reduced. +bool +test16() { + Variable x(0); + Variable y(1); + + Grid grid1(2); + grid1.add_congruence((x %= 0) / 2); + grid1.add_congruence((y %= 0) / 2); + Grid grid2(2); + grid2.add_congruence((x %= 1) / 2); + grid2.add_congruence((y %= 1) / 0); + + Pointset_Powerset<Grid> pps_gr(grid1); + pps_gr.add_disjunct(grid2); + + // At this stage, pps_gr is omega reduced but pps_gr.reduced flag will + // be set to false. + // So we add this test to set the omega reduction pps_gr.reduced + // flag to true. + bool top_closed = pps_gr.is_topologically_closed(); + + Pointset_Powerset<NNC_Polyhedron> pps(pps_gr); + + // pps is not omega reduced. + bool ok = (pps.size() == 2); + + Pointset_Powerset<NNC_Polyhedron> known_pps(2); + + ok = ok && (pps == known_pps) && pps.OK(); + + Pointset_Powerset<NNC_Polyhedron>::const_iterator i = pps.begin(); + NNC_Polyhedron phi = i->element(); + print_constraints(phi, "*** phi ***"); + + return ok; +} + } // namespace

BEGIN_MAIN @@ -390,4 +430,5 @@ BEGIN_MAIN DO_TEST(test13); DO_TEST(test14); DO_TEST(test15); + DO_TEST(test16); END_MAIN