00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <config.h>
00024
00025 #include "Polyhedron.defs.hh"
00026 #include <iostream>
00027 #include <string>
00028 #include <cassert>
00029
00030 namespace PPL = Parma_Polyhedra_Library;
00031
00032 namespace {
00033
00034
00035 const char* zero_dim_univ = "ZE";
00036 const char* empty = "EM";
00037 const char* consys_min = "CM";
00038 const char* gensys_min = "GM";
00039 const char* consys_upd = "CS";
00040 const char* gensys_upd = "GS";
00041 const char* satc_upd = "SC";
00042 const char* satg_upd = "SG";
00043 const char* consys_pending = "CP";
00044 const char* gensys_pending = "GP";
00045
00053 bool
00054 get_field(std::istream& s, const char* keyword, bool& positive) {
00055 std::string str;
00056 if (!(s >> str)
00057 || (str[0] != '+' && str[0] != '-')
00058 || str.substr(1) != keyword)
00059 return false;
00060 positive = (str[0] == '+');
00061 return true;
00062 }
00063
00064 }
00065
00066 void
00067 PPL::Polyhedron::Status::ascii_dump(std::ostream& s) const {
00068 s << (test_zero_dim_univ() ? '+' : '-') << zero_dim_univ << ' '
00069 << (test_empty() ? '+' : '-') << empty << ' '
00070 << ' '
00071 << (test_c_minimized() ? '+' : '-') << consys_min << ' '
00072 << (test_g_minimized() ? '+' : '-') << gensys_min << ' '
00073 << ' '
00074 << (test_c_up_to_date() ? '+' : '-') << consys_upd << ' '
00075 << (test_g_up_to_date() ? '+' : '-') << gensys_upd << ' '
00076 << ' '
00077 << (test_c_pending() ? '+' : '-') << consys_pending << ' '
00078 << (test_g_pending() ? '+' : '-') << gensys_pending << ' '
00079 << ' '
00080 << (test_sat_c_up_to_date() ? '+' : '-') << satc_upd << ' '
00081 << (test_sat_g_up_to_date() ? '+' : '-') << satg_upd << ' ';
00082 }
00083
00084 PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Polyhedron::Status);
00085
00086 bool
00087 PPL::Polyhedron::Status::ascii_load(std::istream& s) {
00088 bool positive;
00089
00090 if (!get_field(s, zero_dim_univ, positive))
00091 return false;
00092 if (positive)
00093 set_zero_dim_univ();
00094
00095 if (!get_field(s, empty, positive))
00096 return false;
00097 if (positive)
00098 set_empty();
00099
00100 if (!get_field(s, consys_min, positive))
00101 return false;
00102 if (positive)
00103 set_c_minimized();
00104 else
00105 reset_c_minimized();
00106
00107 if (!get_field(s, gensys_min, positive))
00108 return false;
00109 if (positive)
00110 set_g_minimized();
00111 else
00112 reset_g_minimized();
00113
00114 if (!get_field(s, consys_upd, positive))
00115 return false;
00116 if (positive)
00117 set_c_up_to_date();
00118 else
00119 reset_c_up_to_date();
00120
00121 if (!get_field(s, gensys_upd, positive))
00122 return false;
00123 if (positive)
00124 set_g_up_to_date();
00125 else
00126 reset_g_up_to_date();
00127
00128 if (!get_field(s, consys_pending, positive))
00129 return false;
00130 if (positive)
00131 set_c_pending();
00132 else
00133 reset_c_pending();
00134
00135 if (!get_field(s, gensys_pending, positive))
00136 return false;
00137 if (positive)
00138 set_g_pending();
00139 else
00140 reset_g_pending();
00141
00142 if (!get_field(s, satc_upd, positive))
00143 return false;
00144 if (positive)
00145 set_sat_c_up_to_date();
00146 else
00147 reset_sat_c_up_to_date();
00148
00149 if (!get_field(s, satg_upd, positive))
00150 return false;
00151 if (positive)
00152 set_sat_g_up_to_date();
00153 else
00154 reset_sat_g_up_to_date();
00155
00156
00157 assert(OK());
00158 return true;
00159 }
00160
00161 bool
00162 PPL::Polyhedron::Status::OK() const {
00163 #ifndef NDEBUG
00164 using std::endl;
00165 using std::cerr;
00166 #endif
00167
00168 if (test_zero_dim_univ())
00169
00170 return true;
00171
00172 if (test_empty()) {
00173 Status copy = *this;
00174 copy.reset_empty();
00175 if (copy.test_zero_dim_univ())
00176 return true;
00177 else {
00178 #ifndef NDEBUG
00179 cerr << "The empty flag is incompatible with any other one."
00180 << endl;
00181 #endif
00182 return false;
00183 }
00184 }
00185
00186 if ((test_sat_c_up_to_date() || test_sat_g_up_to_date())
00187 && !(test_c_up_to_date() && test_g_up_to_date())) {
00188 #ifndef NDEBUG
00189 cerr <<
00190 "If a saturation matrix is up-to-date, constraints and\n"
00191 "generators have to be both up-to-date."
00192 << endl;
00193 #endif
00194 return false;
00195 }
00196
00197 if (test_c_minimized() && !test_c_up_to_date()) {
00198 #ifndef NDEBUG
00199 cerr << "If constraints are minimized they must be up-to-date."
00200 << endl;
00201 #endif
00202 return false;
00203 }
00204
00205 if (test_g_minimized() && !test_g_up_to_date()) {
00206 #ifndef NDEBUG
00207 cerr << "If generators are minimized they must be up-to-date."
00208 << endl;
00209 #endif
00210 return false;
00211 }
00212
00213 if (test_c_pending() && test_g_pending()) {
00214 #ifndef NDEBUG
00215 cerr << "There cannot be both pending constraints and pending generators."
00216 << endl;
00217 #endif
00218 return false;
00219 }
00220
00221 if (test_c_pending() || test_g_pending()) {
00222 if (!test_c_minimized() || !test_g_minimized()) {
00223 #ifndef NDEBUG
00224 cerr <<
00225 "If there are pending constraints or generators, constraints\n"
00226 "and generators must be minimized."
00227 << endl;
00228 #endif
00229 return false;
00230 }
00231
00232 if (!test_sat_c_up_to_date() && !test_sat_g_up_to_date()) {
00233 #ifndef NDEBUG
00234 cerr <<
00235 "If there are pending constraints or generators, there must\n"
00236 "be at least a saturation matrix up-to-date."
00237 << endl;
00238 #endif
00239 return false;
00240 }
00241 }
00242
00243
00244 return true;
00245 }