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 "Bounding_Box.defs.hh"
00025 #include "Variable.defs.hh"
00026 #include "Constraint.defs.hh"
00027 #include "Constraint_System.inlines.hh"
00028 #include <iostream>
00029
00030 namespace PPL = Parma_Polyhedra_Library;
00031
00032 template <typename Iterator>
00033 void
00034 PPL::Bounding_Box::CC76_widening_assign(const Bounding_Box& y,
00035 Iterator first, Iterator last) {
00036 for (dimension_type i = vec.size(); i-- > 0; ) {
00037 Interval& x_vec_i = vec[i];
00038 const Interval& y_vec_i = y.vec[i];
00039
00040
00041 UBoundary& x_ub = x_vec_i.upper_bound();
00042 ERational& x_ubb = x_ub.bound();
00043 const ERational& y_ubb = y_vec_i.upper_bound().bound();
00044 assert(y_ubb <= x_ubb);
00045 if (y_ubb < x_ubb) {
00046 Iterator k = std::lower_bound(first, last, x_ubb);
00047 if (k != last) {
00048 if (x_ubb < *k)
00049 x_ubb = *k;
00050 }
00051 else
00052 x_ub = UBoundary(ERational(PLUS_INFINITY), UBoundary::OPEN);
00053 }
00054
00055
00056 LBoundary& x_lb = x_vec_i.lower_bound();
00057 ERational& x_lbb = x_lb.bound();
00058 const ERational& y_lbb = y_vec_i.lower_bound().bound();
00059 assert(y_lbb >= x_lbb);
00060 if (y_lbb > x_lbb) {
00061 Iterator k = std::lower_bound(first, last, x_lbb);
00062 if (k != last) {
00063 if (x_lbb < *k)
00064 if (k != first)
00065 x_lbb = *--k;
00066 else
00067 x_lb = LBoundary(ERational(MINUS_INFINITY), LBoundary::OPEN);
00068 }
00069 else
00070 x_lbb = *--k;
00071 }
00072 }
00073 }
00074
00075 void
00076 PPL::Bounding_Box::CC76_widening_assign(const Bounding_Box& y) {
00077 static ERational stop_points[] = {
00078 ERational(-2, ROUND_NOT_NEEDED),
00079 ERational(-1, ROUND_NOT_NEEDED),
00080 ERational(0, ROUND_NOT_NEEDED),
00081 ERational(1, ROUND_NOT_NEEDED),
00082 ERational(2, ROUND_NOT_NEEDED)
00083 };
00084 CC76_widening_assign(y,
00085 stop_points,
00086 stop_points
00087 + sizeof(stop_points)/sizeof(stop_points[0]));
00088 }
00089
00090 PPL::Constraint_System
00091 PPL::Bounding_Box::constraints() const {
00092 Constraint_System cs;
00093 dimension_type space_dim = space_dimension();
00094 if (space_dim == 0) {
00095 if (is_empty())
00096 cs = Constraint_System::zero_dim_empty();
00097 }
00098 else if (is_empty())
00099 cs.insert(0*Variable(space_dim-1) <= -1);
00100 else {
00101
00102
00103 cs.insert(0*Variable(space_dim-1) <= 0);
00104
00105 for (dimension_type k = 0; k < space_dim; ++k) {
00106 bool closed = false;
00107 PPL::Coefficient n;
00108 PPL::Coefficient d;
00109 if (get_lower_bound(k, closed, n, d)) {
00110 if (closed)
00111 cs.insert(d*Variable(k) >= n);
00112 else
00113 cs.insert(d*Variable(k) > n);
00114 }
00115 if (get_upper_bound(k, closed, n, d)) {
00116 if (closed)
00117 cs.insert(d*Variable(k) <= n);
00118 else
00119 cs.insert(d*Variable(k) < n);
00120 }
00121 }
00122 }
00123 return cs;
00124 }
00125
00127 std::ostream&
00128 PPL::IO_Operators::operator<<(std::ostream& s, const PPL::Bounding_Box& bbox) {
00129 if (bbox.is_empty()) {
00130 s << "empty";
00131 return s;
00132 }
00133 const dimension_type dimension = bbox.space_dimension();
00134 for (dimension_type k = 0; k < dimension; ++k) {
00135 bool closed = false;
00136 PPL::Coefficient n;
00137 PPL::Coefficient d;
00138 if (bbox.get_lower_bound(k, closed, n, d)) {
00139 s << (closed ? "[" : "(")
00140 << n;
00141 if (d != 1)
00142 s << "/" << d;
00143 s << ", ";
00144 }
00145 else
00146 s << "(-inf, ";
00147 if (bbox.get_upper_bound(k, closed, n, d)) {
00148 s << n;
00149 if (d != 1)
00150 s << "/" << d;
00151 s << (closed ? "]" : ")");
00152 }
00153 else
00154 s << "+inf)";
00155 s << "\n";
00156 }
00157 return s;
00158 }