00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <config.h>
00024 #include "Polyhedra_Powerset.defs.hh"
00025 #include <utility>
00026
00027 namespace PPL = Parma_Polyhedra_Library;
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066
00067 template <>
00068 void
00069 PPL::Polyhedra_Powerset<PPL::NNC_Polyhedron>
00070 ::poly_difference_assign(const Polyhedra_Powerset& y) {
00071 Polyhedra_Powerset& x = *this;
00072
00073 x.omega_reduce();
00074 y.omega_reduce();
00075 Sequence new_sequence = x.sequence;
00076 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
00077 const NNC_Polyhedron& py = yi->element();
00078 Sequence tmp_sequence;
00079 for (Sequence_const_iterator nsi = new_sequence.begin(),
00080 ns_end = new_sequence.end(); nsi != ns_end; ++nsi) {
00081 std::pair<NNC_Polyhedron, Polyhedra_Powerset<NNC_Polyhedron> > partition
00082 = linear_partition(py, nsi->element());
00083 const Polyhedra_Powerset<NNC_Polyhedron>& residues = partition.second;
00084
00085 std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
00086 }
00087 std::swap(tmp_sequence, new_sequence);
00088 }
00089 std::swap(x.sequence, new_sequence);
00090 x.reduced = false;
00091 assert(x.OK());
00092 }
00093
00094 template <>
00095 bool
00096 PPL::Polyhedra_Powerset<PPL::NNC_Polyhedron>
00097 ::geometrically_covers(const Polyhedra_Powerset& y) const {
00098 const Polyhedra_Powerset& x = *this;
00099 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi)
00100 if (!check_containment(yi->element(), x))
00101 return false;
00102 return true;
00103 }
00104
00106 bool
00107 PPL::check_containment(const NNC_Polyhedron& ph,
00108 const Polyhedra_Powerset<NNC_Polyhedron>& ps) {
00109 Polyhedra_Powerset<NNC_Polyhedron> tmp(ph.space_dimension(), EMPTY);
00110 tmp.add_disjunct(ph);
00111 for (Polyhedra_Powerset<NNC_Polyhedron>::const_iterator
00112 i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
00113 const NNC_Polyhedron& pi = i->element();
00114 for (Polyhedra_Powerset<NNC_Polyhedron>::iterator
00115 j = tmp.begin(); j != tmp.end(); ) {
00116 const NNC_Polyhedron& pj = j->element();
00117 if (pi.contains(pj))
00118 j = tmp.drop_disjunct(j);
00119 else
00120 ++j;
00121 }
00122 if (tmp.empty())
00123 return true;
00124 else {
00125 Polyhedra_Powerset<NNC_Polyhedron> new_disjuncts(ph.space_dimension(),
00126 EMPTY);
00127 for (Polyhedra_Powerset<NNC_Polyhedron>::iterator
00128 j = tmp.begin(); j != tmp.end(); ) {
00129 const NNC_Polyhedron& pj = j->element();
00130 if (pj.is_disjoint_from(pi))
00131 ++j;
00132 else {
00133 std::pair<NNC_Polyhedron, Polyhedra_Powerset<NNC_Polyhedron> >
00134 partition = linear_partition(pi, pj);
00135 new_disjuncts.upper_bound_assign(partition.second);
00136 j = tmp.drop_disjunct(j);
00137 }
00138 }
00139 tmp.upper_bound_assign(new_disjuncts);
00140 }
00141 }
00142 return false;
00143 }