1 /* Polyhedron::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 "Polyhedron_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::Polyhedron::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::Polyhedron::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 }
84
PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Polyhedron::Status)85 PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Polyhedron::Status)
86
87 bool
88 PPL::Polyhedron::Status::ascii_load(std::istream& s) {
89 PPL_UNINITIALIZED(bool, positive);
90
91 if (!get_field(s, zero_dim_univ, positive)) {
92 return false;
93 }
94 if (positive) {
95 set_zero_dim_univ();
96 }
97
98 if (!get_field(s, empty, positive)) {
99 return false;
100 }
101 if (positive) {
102 set_empty();
103 }
104
105 if (!get_field(s, consys_min, positive)) {
106 return false;
107 }
108 if (positive) {
109 set_c_minimized();
110 }
111 else {
112 reset_c_minimized();
113 }
114
115 if (!get_field(s, gensys_min, positive)) {
116 return false;
117 }
118 if (positive) {
119 set_g_minimized();
120 }
121 else {
122 reset_g_minimized();
123 }
124
125 if (!get_field(s, consys_upd, positive)) {
126 return false;
127 }
128 if (positive) {
129 set_c_up_to_date();
130 }
131 else {
132 reset_c_up_to_date();
133 }
134
135 if (!get_field(s, gensys_upd, positive)) {
136 return false;
137 }
138 if (positive) {
139 set_g_up_to_date();
140 }
141 else {
142 reset_g_up_to_date();
143 }
144
145 if (!get_field(s, consys_pending, positive)) {
146 return false;
147 }
148 if (positive) {
149 set_c_pending();
150 }
151 else {
152 reset_c_pending();
153 }
154
155 if (!get_field(s, gensys_pending, positive)) {
156 return false;
157 }
158 if (positive) {
159 set_g_pending();
160 }
161 else {
162 reset_g_pending();
163 }
164
165 if (!get_field(s, satc_upd, positive)) {
166 return false;
167 }
168 if (positive) {
169 set_sat_c_up_to_date();
170 }
171 else {
172 reset_sat_c_up_to_date();
173 }
174
175 if (!get_field(s, satg_upd, positive)) {
176 return false;
177 }
178 if (positive) {
179 set_sat_g_up_to_date();
180 }
181 else {
182 reset_sat_g_up_to_date();
183 }
184
185 // Check invariants.
186 PPL_ASSERT(OK());
187 return true;
188 }
189
190 bool
OK() const191 PPL::Polyhedron::Status::OK() const {
192 #ifndef NDEBUG
193 using std::endl;
194 using std::cerr;
195 #endif
196
197 if (test_zero_dim_univ()) {
198 // Zero-dim universe is OK.
199 return true;
200 }
201
202 if (test_empty()) {
203 Status copy = *this;
204 copy.reset_empty();
205 if (copy.test_zero_dim_univ()) {
206 return true;
207 }
208 else {
209 #ifndef NDEBUG
210 cerr << "The empty flag is incompatible with any other one."
211 << endl;
212 #endif
213 return false;
214 }
215 }
216
217 if ((test_sat_c_up_to_date() || test_sat_g_up_to_date())
218 && !(test_c_up_to_date() && test_g_up_to_date())) {
219 #ifndef NDEBUG
220 cerr <<
221 "If a saturation matrix is up-to-date, constraints and\n"
222 "generators have to be both up-to-date."
223 << endl;
224 #endif
225 return false;
226 }
227
228 if (test_c_minimized() && !test_c_up_to_date()) {
229 #ifndef NDEBUG
230 cerr << "If constraints are minimized they must be up-to-date."
231 << endl;
232 #endif
233 return false;
234 }
235
236 if (test_g_minimized() && !test_g_up_to_date()) {
237 #ifndef NDEBUG
238 cerr << "If generators are minimized they must be up-to-date."
239 << endl;
240 #endif
241 return false;
242 }
243
244 if (test_c_pending() && test_g_pending()) {
245 #ifndef NDEBUG
246 cerr << "There cannot be both pending constraints and pending generators."
247 << endl;
248 #endif
249 return false;
250 }
251
252 if (test_c_pending() || test_g_pending()) {
253 if (!test_c_minimized() || !test_g_minimized()) {
254 #ifndef NDEBUG
255 cerr <<
256 "If there are pending constraints or generators, constraints\n"
257 "and generators must be minimized."
258 << endl;
259 #endif
260 return false;
261 }
262
263 if (!test_sat_c_up_to_date() && !test_sat_g_up_to_date()) {
264 #ifndef NDEBUG
265 cerr <<
266 "If there are pending constraints or generators, there must\n"
267 "be at least a saturation matrix up-to-date."
268 << endl;
269 #endif
270 return false;
271 }
272 }
273
274 // Any other case is OK.
275 return true;
276 }
277