1 /* Grid::Status class declaration. 2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> 3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) 4 5 This file is part of the Parma Polyhedra Library (PPL). 6 7 The PPL is free software; you can redistribute it and/or modify it 8 under the terms of the GNU General Public License as published by the 9 Free Software Foundation; either version 3 of the License, or (at your 10 option) any later version. 11 12 The PPL is distributed in the hope that it will be useful, but WITHOUT 13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 15 for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software Foundation, 19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 20 21 For the most up-to-date information see the Parma Polyhedra Library 22 site: http://bugseng.com/products/ppl/ . */ 23 24 #ifndef PPL_Grid_Status_idefs_hh 25 #define PPL_Grid_Status_idefs_hh 1 26 27 #ifndef PPL_IN_Grid_CLASS 28 #error "Do not include Grid_Status_idefs.hh directly; use Grid_defs.hh instead" 29 #endif 30 31 //! A conjunctive assertion about a grid. 32 /*! 33 The assertions supported that are in use are: 34 - <EM>zero-dim universe</EM>: the grid is the zero-dimension 35 vector space \f$\Rset^0 = \{\cdot\}\f$; 36 - <EM>empty</EM>: the grid is the empty set; 37 - <EM>congruences up-to-date</EM>: the grid is correctly 38 characterized by the attached system of congruences, modulo the 39 processing of pending generators; 40 - <EM>generators up-to-date</EM>: the grid is correctly 41 characterized by the attached system of generators, modulo the 42 processing of pending congruences; 43 - <EM>congruences minimized</EM>: the non-pending part of the system 44 of congruences attached to the grid is in minimal form; 45 - <EM>generators minimized</EM>: the non-pending part of the system 46 of generators attached to the grid is in minimal form. 47 48 Other supported assertions are: 49 - <EM>congruences pending</EM> 50 - <EM>generators pending</EM> 51 - <EM>congruences' saturation matrix up-to-date</EM> 52 - <EM>generators' saturation matrix up-to-date</EM>. 53 54 Not all the conjunctions of these elementary assertions constitute 55 a legal Status. In fact: 56 - <EM>zero-dim universe</EM> excludes any other assertion; 57 - <EM>empty</EM>: excludes any other assertion; 58 - <EM>congruences pending</EM> and <EM>generators pending</EM> 59 are mutually exclusive; 60 - <EM>congruences pending</EM> implies both <EM>congruences minimized</EM> 61 and <EM>generators minimized</EM>; 62 - <EM>generators pending</EM> implies both <EM>congruences minimized</EM> 63 and <EM>generators minimized</EM>; 64 - <EM>congruences minimized</EM> implies <EM>congruences up-to-date</EM>; 65 - <EM>generators minimized</EM> implies <EM>generators up-to-date</EM>; 66 - <EM>congruences' saturation matrix up-to-date</EM> implies both 67 <EM>congruences up-to-date</EM> and <EM>generators up-to-date</EM>; 68 - <EM>generators' saturation matrix up-to-date</EM> implies both 69 <EM>congruences up-to-date</EM> and <EM>generators up-to-date</EM>. 70 */ 71 class Status { 72 public: 73 //! By default Status is the <EM>zero-dim universe</EM> assertion. 74 Status(); 75 76 //! \name Test, remove or add an individual assertion from the conjunction 77 //@{ 78 bool test_zero_dim_univ() const; 79 void reset_zero_dim_univ(); 80 void set_zero_dim_univ(); 81 82 bool test_empty() const; 83 void reset_empty(); 84 void set_empty(); 85 86 bool test_c_up_to_date() const; 87 void reset_c_up_to_date(); 88 void set_c_up_to_date(); 89 90 bool test_g_up_to_date() const; 91 void reset_g_up_to_date(); 92 void set_g_up_to_date(); 93 94 bool test_c_minimized() const; 95 void reset_c_minimized(); 96 void set_c_minimized(); 97 98 bool test_g_minimized() const; 99 void reset_g_minimized(); 100 void set_g_minimized(); 101 102 bool test_sat_c_up_to_date() const; 103 void reset_sat_c_up_to_date(); 104 void set_sat_c_up_to_date(); 105 106 bool test_sat_g_up_to_date() const; 107 void reset_sat_g_up_to_date(); 108 void set_sat_g_up_to_date(); 109 110 bool test_c_pending() const; 111 void reset_c_pending(); 112 void set_c_pending(); 113 114 bool test_g_pending() const; 115 void reset_g_pending(); 116 void set_g_pending(); 117 //@} // Test, remove or add an individual assertion from the conjunction 118 119 //! Checks if all the invariants are satisfied. 120 bool OK() const; 121 122 PPL_OUTPUT_DECLARATIONS 123 124 /*! \brief 125 Loads from \p s an ASCII representation (as produced by 126 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 127 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 128 */ 129 bool ascii_load(std::istream& s); 130 131 private: 132 //! Status is implemented by means of a finite bitset. 133 typedef unsigned int flags_t; 134 135 //! \name Bitmasks for the individual assertions 136 //@{ 137 static const flags_t ZERO_DIM_UNIV = 0U; 138 static const flags_t EMPTY = 1U << 0; 139 static const flags_t C_UP_TO_DATE = 1U << 1; 140 static const flags_t G_UP_TO_DATE = 1U << 2; 141 static const flags_t C_MINIMIZED = 1U << 3; 142 static const flags_t G_MINIMIZED = 1U << 4; 143 static const flags_t SAT_C_UP_TO_DATE = 1U << 5; 144 static const flags_t SAT_G_UP_TO_DATE = 1U << 6; 145 static const flags_t CS_PENDING = 1U << 7; 146 static const flags_t GS_PENDING = 1U << 8; 147 //@} // Bitmasks for the individual assertions 148 149 //! This holds the current bitset. 150 flags_t flags; 151 152 //! Construct from a bitmask. 153 Status(flags_t mask); 154 155 //! Check whether <EM>all</EM> bits in \p mask are set. 156 bool test_all(flags_t mask) const; 157 158 //! Check whether <EM>at least one</EM> bit in \p mask is set. 159 bool test_any(flags_t mask) const; 160 161 //! Set the bits in \p mask. 162 void set(flags_t mask); 163 164 //! Reset the bits in \p mask. 165 void reset(flags_t mask); 166 }; 167 168 #endif // !defined(PPL_Grid_Status_idefs_hh) 169