[PPL-devel] [GIT] ppl/ppl(master): Changes to deal with //FIXME(0.10.1): the following is a bug!

[Patricia Hill]

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

Author: Patricia Hill <p.m.hill at 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_Powerset<PPL::NNC_Polyhedron>
 
 template <>
 template <>
+PPL::Pointset_Powerset<PPL::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_Powerset<PPL::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