00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #ifndef PPL_Linear_System_defs_hh
00024 #define PPL_Linear_System_defs_hh 1
00025
00026 #include "Linear_System.types.hh"
00027 #include "Row.types.hh"
00028 #include "Bit_Row.types.hh"
00029 #include "Bit_Matrix.types.hh"
00030 #include "Matrix.defs.hh"
00031 #include "Topology.hh"
00032 #include "Linear_Row.defs.hh"
00033
00034 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00036
00052 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00053
00054 class Parma_Polyhedra_Library::Linear_System : public Matrix {
00055 public:
00057
00060 Linear_System(Topology topol);
00061
00063
00077 Linear_System(Topology topol,
00078 dimension_type n_rows, dimension_type n_columns);
00079
00080 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00082
00087 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00088 struct With_Pending {
00089 };
00090
00092 Linear_System(const Linear_System& y);
00093
00095 Linear_System(const Linear_System& y, With_Pending);
00096
00098 Linear_System& operator=(const Linear_System& y);
00099
00101 void assign_with_pending(const Linear_System& y);
00102
00104 void swap(Linear_System& y);
00105
00107 static dimension_type max_space_dimension();
00108
00110
00118 dimension_type space_dimension() const;
00119
00121 void remove_trailing_columns(dimension_type n);
00122
00124
00125
00126
00127
00128
00129
00130
00131
00132
00133
00134
00135
00136
00137
00138
00139 void permute_columns(const std::vector<dimension_type>& cycles);
00140
00142
00143
00144 Linear_Row& operator[](dimension_type k);
00145
00147 const Linear_Row& operator[](dimension_type k) const;
00149
00151 void strong_normalize();
00152
00154 void sign_normalize();
00155
00157
00158
00159 Topology topology() const;
00160
00162 bool is_sorted() const;
00163
00168 bool is_necessarily_closed() const;
00169
00174 dimension_type num_lines_or_equalities() const;
00175
00177 dimension_type first_pending_row() const;
00178
00180 dimension_type num_pending_rows() const;
00182
00187 bool check_sorted() const;
00188
00190 void set_necessarily_closed();
00191
00193 void set_not_necessarily_closed();
00194
00196 void set_rows_topology();
00197
00199 void unset_pending_rows();
00200
00202 void set_index_first_pending_row(dimension_type i);
00203
00205 void set_sorted(bool b);
00206
00208
00219 void resize_no_copy(dimension_type new_n_rows, dimension_type new_n_columns);
00220
00222
00233 void add_rows_and_columns(dimension_type n);
00234
00239 void insert(const Linear_Row& r);
00240
00245 void insert_pending(const Linear_Row& r);
00246
00248 void add_row(const Linear_Row& r);
00249
00251 void add_pending_row(Linear_Row::Flags flags);
00252
00254 void add_pending_row(const Linear_Row& r);
00255
00257
00260 void add_rows(const Linear_System& y);
00261
00263 void add_pending_rows(const Linear_System& y);
00264
00269 void sort_rows();
00270
00275 void sort_rows(dimension_type first_row, dimension_type last_row);
00276
00285 void merge_rows_assign(const Linear_System& y);
00286
00291 void sort_pending_and_remove_duplicates();
00292
00293 class With_Bit_Matrix_iterator;
00294
00302 void sort_and_remove_with_sat(Bit_Matrix& sat);
00303
00305
00316 dimension_type gauss(dimension_type n_lines_or_equalities);
00317
00328 void back_substitute(dimension_type n_lines_or_equalities);
00329
00334 void simplify();
00335
00340 void normalize();
00341
00343 void clear();
00344
00345 PPL_OUTPUT_DECLARATIONS
00346
00357 bool ascii_load(std::istream& s);
00358
00360 memory_size_type total_memory_in_bytes() const;
00361
00363 memory_size_type external_memory_in_bytes() const;
00364
00366
00376 bool OK(bool check_strong_normalized = true) const;
00377
00378 private:
00380 Topology row_topology;
00381
00383 dimension_type index_first_pending;
00384
00390 bool sorted;
00391
00393 struct Row_Less_Than {
00394 bool operator()(const Row& x, const Row& y) const;
00395 };
00396 };
00397
00398 namespace std {
00399
00400 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00402
00403 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00404 void swap(Parma_Polyhedra_Library::Linear_System& x,
00405 Parma_Polyhedra_Library::Linear_System& y);
00406
00407 }
00408
00409 namespace Parma_Polyhedra_Library {
00410
00411 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00413
00414 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00415 bool operator==(const Linear_System& x, const Linear_System& y);
00416
00417 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00419
00420 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00421 bool operator!=(const Linear_System& x, const Linear_System& y);
00422
00423 }
00424
00425 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00427
00433 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00434 class Parma_Polyhedra_Library::Linear_System::With_Bit_Matrix_iterator {
00435 public:
00436 typedef std::vector<Row>::iterator Iter1;
00437 typedef std::vector<Bit_Row>::iterator Iter2;
00438
00439 private:
00440 Iter1 i1;
00441 Iter2 i2;
00442
00443 public:
00444
00445 typedef std::iterator_traits<Iter1>::iterator_category iterator_category;
00446 typedef std::iterator_traits<Iter1>::value_type value_type;
00447 typedef std::iterator_traits<Iter1>::difference_type difference_type;
00448 typedef std::iterator_traits<Iter1>::pointer pointer;
00449 typedef std::iterator_traits<Iter1>::reference reference;
00450
00452 With_Bit_Matrix_iterator(Iter1 iter1, Iter2 iter2);
00453
00455 With_Bit_Matrix_iterator(const With_Bit_Matrix_iterator& y);
00456
00458 ~With_Bit_Matrix_iterator();
00459
00461 With_Bit_Matrix_iterator&
00462 operator=(const With_Bit_Matrix_iterator& y);
00463
00465
00466 With_Bit_Matrix_iterator& operator++();
00467 With_Bit_Matrix_iterator operator++(int);
00468
00469 With_Bit_Matrix_iterator& operator--();
00470 With_Bit_Matrix_iterator operator--(int);
00471
00472 With_Bit_Matrix_iterator& operator+=(difference_type d);
00473 With_Bit_Matrix_iterator operator+(difference_type d) const;
00474
00475 With_Bit_Matrix_iterator& operator-=(difference_type d);
00476 With_Bit_Matrix_iterator operator-(difference_type d) const;
00478
00480 difference_type operator-(const With_Bit_Matrix_iterator& y) const;
00481
00483
00484 bool operator==(const With_Bit_Matrix_iterator& y) const;
00485 bool operator!=(const With_Bit_Matrix_iterator& y) const;
00486 bool operator<(const With_Bit_Matrix_iterator& y) const;
00488
00490 reference operator*() const;
00491
00493 pointer operator->() const;
00494
00496 void iter_swap(const With_Bit_Matrix_iterator& y) const;
00497
00498 };
00499
00500 namespace std {
00501
00502 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00504
00505 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00506 void
00507 iter_swap(Parma_Polyhedra_Library
00508 ::Linear_System::With_Bit_Matrix_iterator x,
00509 Parma_Polyhedra_Library
00510 ::Linear_System::With_Bit_Matrix_iterator y);
00511
00512 }
00513
00514 #include "Linear_System.inlines.hh"
00515
00516 #endif // !defined(PPL_Linear_System_defs_hh)