1 /* Polyhedron::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_Status_idefs_hh 25 #define PPL_Status_idefs_hh 1 26 27 #ifndef PPL_IN_Polyhedron_CLASS 28 #error "Do not include Ph_Status_idefs.hh directly; use Polyhedron_defs.hh instead" 29 #endif 30 31 //! A conjunctive assertion about a polyhedron. 32 /*! \ingroup PPL_CXX_interface 33 The assertions supported are: 34 - <EM>zero-dim universe</EM>: the polyhedron is the zero-dimension 35 vector space \f$\Rset^0 = \{\cdot\}\f$; 36 - <EM>empty</EM>: the polyhedron is the empty set; 37 - <EM>constraints pending</EM>: the polyhedron is correctly 38 characterized by the attached system of constraints, which is 39 split in two non-empty subsets: the already processed constraints, 40 which are in minimal form, and the pending constraints, which 41 still have to be processed and may thus be inconsistent or 42 contain redundancies; 43 - <EM>generators pending</EM>: the polyhedron is correctly 44 characterized by the attached system of generators, which is 45 split in two non-empty subsets: the already processed generators, 46 which are in minimal form, and the pending generators, which still 47 have to be processed and may thus contain redundancies; 48 - <EM>constraints up-to-date</EM>: the polyhedron is correctly 49 characterized by the attached system of constraints, modulo the 50 processing of pending generators; 51 - <EM>generators up-to-date</EM>: the polyhedron is correctly 52 characterized by the attached system of generators, modulo the 53 processing of pending constraints; 54 - <EM>constraints minimized</EM>: the non-pending part of the system 55 of constraints attached to the polyhedron is in minimal form; 56 - <EM>generators minimized</EM>: the non-pending part of the system 57 of generators attached to the polyhedron is in minimal form; 58 - <EM>constraints' saturation matrix up-to-date</EM>: the attached 59 saturation matrix having rows indexed by non-pending generators and 60 columns indexed by non-pending constraints correctly expresses 61 the saturation relation between the attached non-pending constraints 62 and generators; 63 - <EM>generators' saturation matrix up-to-date</EM>: the attached 64 saturation matrix having rows indexed by non-pending constraints and 65 columns indexed by non-pending generators correctly expresses 66 the saturation relation between the attached non-pending constraints 67 and generators; 68 69 Not all the conjunctions of these elementary assertions constitute 70 a legal Status. In fact: 71 - <EM>zero-dim universe</EM> excludes any other assertion; 72 - <EM>empty</EM>: excludes any other assertion; 73 - <EM>constraints pending</EM> and <EM>generators pending</EM> 74 are mutually exclusive; 75 - <EM>constraints pending</EM> implies both <EM>constraints minimized</EM> 76 and <EM>generators minimized</EM>; 77 - <EM>generators pending</EM> implies both <EM>constraints minimized</EM> 78 and <EM>generators minimized</EM>; 79 - <EM>constraints minimized</EM> implies <EM>constraints up-to-date</EM>; 80 - <EM>generators minimized</EM> implies <EM>generators up-to-date</EM>; 81 - <EM>constraints' saturation matrix up-to-date</EM> implies both 82 <EM>constraints up-to-date</EM> and <EM>generators up-to-date</EM>; 83 - <EM>generators' saturation matrix up-to-date</EM> implies both 84 <EM>constraints up-to-date</EM> and <EM>generators up-to-date</EM>. 85 */ 86 class Status { 87 public: 88 //! By default Status is the <EM>zero-dim universe</EM> assertion. 89 Status(); 90 91 //! \name Test, remove or add an individual assertion from the conjunction 92 //@{ 93 bool test_zero_dim_univ() const; 94 void reset_zero_dim_univ(); 95 void set_zero_dim_univ(); 96 97 bool test_empty() const; 98 void reset_empty(); 99 void set_empty(); 100 101 bool test_c_up_to_date() const; 102 void reset_c_up_to_date(); 103 void set_c_up_to_date(); 104 105 bool test_g_up_to_date() const; 106 void reset_g_up_to_date(); 107 void set_g_up_to_date(); 108 109 bool test_c_minimized() const; 110 void reset_c_minimized(); 111 void set_c_minimized(); 112 113 bool test_g_minimized() const; 114 void reset_g_minimized(); 115 void set_g_minimized(); 116 117 bool test_sat_c_up_to_date() const; 118 void reset_sat_c_up_to_date(); 119 void set_sat_c_up_to_date(); 120 121 bool test_sat_g_up_to_date() const; 122 void reset_sat_g_up_to_date(); 123 void set_sat_g_up_to_date(); 124 125 bool test_c_pending() const; 126 void reset_c_pending(); 127 void set_c_pending(); 128 129 bool test_g_pending() const; 130 void reset_g_pending(); 131 void set_g_pending(); 132 //@} // Test, remove or add an individual assertion from the conjunction 133 134 //! Checks if all the invariants are satisfied. 135 bool OK() const; 136 137 PPL_OUTPUT_DECLARATIONS 138 139 /*! \brief 140 Loads from \p s an ASCII representation (as produced by 141 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 142 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 143 */ 144 bool ascii_load(std::istream& s); 145 146 private: 147 //! Status is implemented by means of a finite bitset. 148 typedef unsigned int flags_t; 149 150 //! \name Bit-masks for the individual assertions 151 //@{ 152 static const flags_t ZERO_DIM_UNIV = 0U; 153 static const flags_t EMPTY = 1U << 0; 154 static const flags_t C_UP_TO_DATE = 1U << 1; 155 static const flags_t G_UP_TO_DATE = 1U << 2; 156 static const flags_t C_MINIMIZED = 1U << 3; 157 static const flags_t G_MINIMIZED = 1U << 4; 158 static const flags_t SAT_C_UP_TO_DATE = 1U << 5; 159 static const flags_t SAT_G_UP_TO_DATE = 1U << 6; 160 static const flags_t CS_PENDING = 1U << 7; 161 static const flags_t GS_PENDING = 1U << 8; 162 //@} // Bit-masks for the individual assertions 163 164 //! This holds the current bitset. 165 flags_t flags; 166 167 //! Construct from a bit-mask. 168 Status(flags_t mask); 169 170 //! Check whether <EM>all</EM> bits in \p mask are set. 171 bool test_all(flags_t mask) const; 172 173 //! Check whether <EM>at least one</EM> bit in \p mask is set. 174 bool test_any(flags_t mask) const; 175 176 //! Set the bits in \p mask. 177 void set(flags_t mask); 178 179 //! Reset the bits in \p mask. 180 void reset(flags_t mask); 181 }; 182 183 #endif // !defined(PPL_Status_idefs_hh) 184