1 /* Grid::Status class implementation (non-inline functions).
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 #include "ppl-config.h"
25 #include "Grid_defs.hh"
26 #include "assertions.hh"
27 #include <iostream>
28 #include <string>
29
30 namespace PPL = Parma_Polyhedra_Library;
31
32 namespace {
33
34 // These are the keywords that indicate the individual assertions.
35 const char* zero_dim_univ = "ZE";
36 const char* empty = "EM";
37 const char* consys_min = "CM";
38 const char* gensys_min = "GM";
39 const char* consys_upd = "CS";
40 const char* gensys_upd = "GS";
41 const char* satc_upd = "SC";
42 const char* satg_upd = "SG";
43 const char* consys_pending = "CP";
44 const char* gensys_pending = "GP";
45
46 /*! \relates Parma_Polyhedra_Library::Grid::Status
47 Reads a keyword and its associated on/off, +/- flag from \p s.
48 Returns <CODE>true</CODE> if the operation is successful,
49 returns <CODE>false</CODE> otherwise.
50 When successful, \p positive is set to <CODE>true</CODE> if the flag
51 is on; it is set to <CODE>false</CODE> otherwise.
52 */
53 bool
get_field(std::istream & s,const char * keyword,bool & positive)54 get_field(std::istream& s, const char* keyword, bool& positive) {
55 std::string str;
56 if (!(s >> str)
57 || (str[0] != '+' && str[0] != '-')
58 || str.substr(1) != keyword) {
59 return false;
60 }
61 positive = (str[0] == '+');
62 return true;
63 }
64
65 } // namespace
66
67 void
ascii_dump(std::ostream & s) const68 PPL::Grid::Status::ascii_dump(std::ostream& s) const {
69 s << (test_zero_dim_univ() ? '+' : '-') << zero_dim_univ << ' '
70 << (test_empty() ? '+' : '-') << empty << ' '
71 << ' '
72 << (test_c_minimized() ? '+' : '-') << consys_min << ' '
73 << (test_g_minimized() ? '+' : '-') << gensys_min << ' '
74 << ' '
75 << (test_c_up_to_date() ? '+' : '-') << consys_upd << ' '
76 << (test_g_up_to_date() ? '+' : '-') << gensys_upd << ' '
77 << ' '
78 << (test_c_pending() ? '+' : '-') << consys_pending << ' '
79 << (test_g_pending() ? '+' : '-') << gensys_pending << ' '
80 << ' '
81 << (test_sat_c_up_to_date() ? '+' : '-') << satc_upd << ' '
82 << (test_sat_g_up_to_date() ? '+' : '-') << satg_upd
83 << std::endl;
84 }
85
PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Grid::Status)86 PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Grid::Status)
87
88 bool
89 PPL::Grid::Status::ascii_load(std::istream& s) {
90 PPL_UNINITIALIZED(bool, positive);
91
92 if (!get_field(s, zero_dim_univ, positive)) {
93 return false;
94 }
95 if (positive) {
96 set_zero_dim_univ();
97 }
98
99 if (!get_field(s, empty, positive)) {
100 return false;
101 }
102 if (positive) {
103 set_empty();
104 }
105
106 if (!get_field(s, consys_min, positive)) {
107 return false;
108 }
109 if (positive) {
110 set_c_minimized();
111 }
112 else {
113 reset_c_minimized();
114 }
115
116 if (!get_field(s, gensys_min, positive)) {
117 return false;
118 }
119
120 if (positive) {
121 set_g_minimized();
122 }
123 else {
124 reset_g_minimized();
125 }
126
127 if (!get_field(s, consys_upd, positive)) {
128 return false;
129 }
130
131 if (positive) {
132 set_c_up_to_date();
133 }
134 else {
135 reset_c_up_to_date();
136 }
137
138 if (!get_field(s, gensys_upd, positive)) {
139 return false;
140 }
141 if (positive) {
142 set_g_up_to_date();
143 }
144 else {
145 reset_g_up_to_date();
146 }
147
148 if (!get_field(s, consys_pending, positive)) {
149 return false;
150 }
151 if (positive) {
152 set_c_pending();
153 }
154 else {
155 reset_c_pending();
156 }
157
158 if (!get_field(s, gensys_pending, positive)) {
159 return false;
160 }
161 if (positive) {
162 set_g_pending();
163 }
164 else {
165 reset_g_pending();
166 }
167
168 if (!get_field(s, satc_upd, positive)) {
169 return false;
170 }
171 if (positive) {
172 set_sat_c_up_to_date();
173 }
174 else {
175 reset_sat_c_up_to_date();
176 }
177
178 if (!get_field(s, satg_upd, positive)) {
179 return false;
180 }
181 if (positive) {
182 set_sat_g_up_to_date();
183 }
184 else {
185 reset_sat_g_up_to_date();
186 }
187
188 // Check invariants.
189 PPL_ASSERT(OK());
190 return true;
191 }
192
193 bool
OK() const194 PPL::Grid::Status::OK() const {
195 #ifndef NDEBUG
196 using std::endl;
197 using std::cerr;
198 #endif
199
200 if (test_zero_dim_univ()) {
201 // Zero-dim universe is OK.
202 return true;
203 }
204
205 if (test_empty()) {
206 Status copy = *this;
207 copy.reset_empty();
208 if (copy.test_zero_dim_univ()) {
209 return true;
210 }
211 #ifndef NDEBUG
212 cerr << "The empty flag is incompatible with any other one."
213 << endl << "Flags:" << endl;
214 ascii_dump(cerr);
215 #endif
216 return false;
217 }
218
219 if ((test_sat_c_up_to_date() || test_sat_g_up_to_date())
220 && !(test_c_up_to_date() && test_g_up_to_date())) {
221 #ifndef NDEBUG
222 cerr <<
223 "If a saturation matrix is up-to-date, congruences and\n"
224 "generators have to be both up-to-date."
225 << endl;
226 #endif
227 return false;
228 }
229
230 if (test_c_minimized() && !test_c_up_to_date()) {
231 #ifndef NDEBUG
232 cerr << "If congruences are minimized they must be up-to-date."
233 << endl;
234 #endif
235 return false;
236 }
237
238 if (test_g_minimized() && !test_g_up_to_date()) {
239 #ifndef NDEBUG
240 cerr << "If generators are minimized they must be up-to-date."
241 << endl;
242 #endif
243 return false;
244 }
245
246 if (test_c_pending() && test_g_pending()) {
247 #ifndef NDEBUG
248 cerr << "There cannot be both pending congruences and pending generators."
249 << endl;
250 #endif
251 return false;
252 }
253
254 if (test_c_pending() || test_g_pending()) {
255 if (!test_c_minimized() || !test_g_minimized()) {
256 #ifndef NDEBUG
257 cerr <<
258 "If there are pending congruences or generators, congruences\n"
259 "and generators must be minimized."
260 << endl;
261 #endif
262 return false;
263 }
264
265 if (!test_sat_c_up_to_date() && !test_sat_g_up_to_date()) {
266 #ifndef NDEBUG
267 cerr <<
268 "If there are pending congruences or generators, there must\n"
269 "be at least a saturation matrix up-to-date."
270 << endl;
271 #endif
272 return false;
273 }
274 }
275
276 // Any other case is OK.
277 return true;
278 }
279