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
00025 #include "Saturation_Matrix.defs.hh"
00026 #include "globals.defs.hh"
00027 #include <iostream>
00028 #include <string>
00029
00030 #include "swapping_sort.icc"
00031
00032 namespace PPL = Parma_Polyhedra_Library;
00033
00034 PPL::Saturation_Matrix&
00035 PPL::Saturation_Matrix::operator=(const Saturation_Matrix& y){
00036 rows = y.rows;
00037 row_size = y.row_size;
00038 assert(OK());
00039 return *this;
00040 }
00041
00042 void
00043 PPL::Saturation_Matrix::sort_rows() {
00044 typedef std::vector<Saturation_Row>::iterator Iter;
00045
00046 Iter first = rows.begin();
00047 Iter last = rows.end();
00048 swapping_sort(first, last, Saturation_Row_Less_Than());
00049
00050 Iter new_last = swapping_unique(first, last);
00051
00052 rows.erase(new_last, last);
00053 assert(OK());
00054 }
00055
00056 void
00057 PPL::Saturation_Matrix::add_row(const Saturation_Row& row) {
00058 const dimension_type new_rows_size = rows.size() + 1;
00059 if (rows.capacity() < new_rows_size) {
00060
00061 std::vector<Saturation_Row> new_rows;
00062 new_rows.reserve(compute_capacity(new_rows_size, max_num_rows()));
00063 new_rows.insert(new_rows.end(), new_rows_size, Saturation_Row());
00064
00065 dimension_type i = new_rows_size-1;
00066 new_rows[i] = row;
00067
00068 while (i-- > 0)
00069 new_rows[i].swap(rows[i]);
00070
00071 std::swap(rows, new_rows);
00072 }
00073 else
00074
00075 rows.push_back(row);
00076 assert(OK());
00077 }
00078
00079 void
00080 PPL::Saturation_Matrix::transpose() {
00081 const Saturation_Matrix& x = *this;
00082 const dimension_type nrows = num_rows();
00083 const dimension_type ncols = num_columns();
00084 Saturation_Matrix tmp(ncols, nrows);
00085 for (dimension_type i = nrows; i-- > 0; )
00086 for (unsigned long j = x[i].last(); j != ULONG_MAX; j = x[i].prev(j))
00087 tmp[j].set(i);
00088 swap(tmp);
00089 assert(OK());
00090 }
00091
00092 void
00093 PPL::Saturation_Matrix::transpose_assign(const Saturation_Matrix& y) {
00094 const dimension_type y_nrows = y.num_rows();
00095 const dimension_type y_ncols = y.num_columns();
00096 Saturation_Matrix tmp(y_ncols, y_nrows);
00097 for (dimension_type i = y_nrows; i-- > 0; )
00098 for (unsigned long j = y[i].last(); j != ULONG_MAX; j = y[i].prev(j))
00099 tmp[j].set(i);
00100 swap(tmp);
00101 assert(OK());
00102 }
00103
00104 void
00105 PPL::Saturation_Matrix::resize(dimension_type new_n_rows,
00106 dimension_type new_n_columns) {
00107 assert(OK());
00108 const dimension_type old_num_rows = num_rows();
00109 if (new_n_columns < row_size) {
00110 const dimension_type num_preserved_rows
00111 = std::min(old_num_rows, new_n_rows);
00112 Saturation_Matrix& x = *this;
00113 for (dimension_type i = num_preserved_rows; i-- > 0; )
00114 x[i].clear_from(new_n_columns);
00115 }
00116 row_size = new_n_columns;
00117 if (new_n_rows > old_num_rows) {
00118 if (rows.capacity() < new_n_rows) {
00119
00120 std::vector<Saturation_Row> new_rows;
00121 new_rows.reserve(compute_capacity(new_n_rows, max_num_rows()));
00122 new_rows.insert(new_rows.end(), new_n_rows, Saturation_Row());
00123
00124 for (dimension_type i = old_num_rows; i-- > 0; )
00125 new_rows[i].swap(rows[i]);
00126
00127 std::swap(rows, new_rows);
00128 }
00129 else
00130
00131 rows.insert(rows.end(), new_n_rows - old_num_rows, Saturation_Row());
00132 }
00133 else if (new_n_rows < old_num_rows)
00134
00135 rows.erase(rows.begin() + new_n_rows, rows.end());
00136
00137 assert(OK());
00138 }
00139
00140 void
00141 PPL::Saturation_Matrix::ascii_dump(std::ostream& s) const {
00142 const Saturation_Matrix& x = *this;
00143 const char separator = ' ';
00144 s << num_rows() << separator << 'x' << separator
00145 << num_columns() << "\n";
00146 for (dimension_type i = 0; i < num_rows(); ++i) {
00147 for (dimension_type j = 0; j < num_columns(); ++j)
00148 s << x[i][j] << separator;
00149 s << "\n";
00150 }
00151 }
00152
00153 PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Saturation_Matrix);
00154
00155 bool
00156 PPL::Saturation_Matrix::ascii_load(std::istream& s) {
00157 Saturation_Matrix& x = *this;
00158 dimension_type nrows;
00159 dimension_type ncols;
00160 std::string str;
00161 if (!(s >> nrows))
00162 return false;
00163 if (!(s >> str))
00164 return false;
00165 if (!(s >> ncols))
00166 return false;
00167 resize(nrows, ncols);
00168
00169 for (dimension_type i = 0; i < num_rows(); ++i)
00170 for (dimension_type j = 0; j < num_columns(); ++j) {
00171 int bit;
00172 if (!(s >> bit))
00173 return false;
00174 if (bit)
00175 x[i].set(j);
00176 else
00177 x[i].clear(j);
00178 }
00179
00180 assert(OK());
00181 return true;
00182 }
00183
00184 PPL::memory_size_type
00185 PPL::Saturation_Matrix::external_memory_in_bytes() const {
00186 memory_size_type n = rows.capacity() * sizeof(Row);
00187 for (dimension_type i = num_rows(); i-- > 0; )
00188 n += rows[i].external_memory_in_bytes();
00189 return n;
00190 }
00191
00192 bool
00193 PPL::Saturation_Matrix::OK() const {
00194 #ifndef NDEBUG
00195 using std::endl;
00196 using std::cerr;
00197 #endif
00198
00199 const Saturation_Matrix& x = *this;
00200 for (dimension_type i = num_rows(); i-- > 1; ) {
00201 const Saturation_Row& row = x[i];
00202 if (!row.OK())
00203 return false;
00204 else if (row.last() != ULONG_MAX && row.last() >= row_size) {
00205 #ifndef NDEBUG
00206 cerr << "Saturation_Matrix[" << i << "] is a row with too many bits!"
00207 << endl
00208 << "(row_size == " << row_size
00209 << ", row.last() == " << row.last() << ")"
00210 << endl;
00211 #endif
00212 return false;
00213 }
00214 }
00215 return true;
00216 }
00217
00218 #ifndef NDEBUG
00219 bool
00220 PPL::Saturation_Matrix::check_sorted() const {
00221 const Saturation_Matrix& x = *this;
00222 for (dimension_type i = num_rows(); i-- > 1; )
00223 if (compare(x[i-1], x[i]) > 0)
00224 return false;
00225 return true;
00226 }
00227 #endif