00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #include <config.h>
00025
00026 #include "Grid.defs.hh"
00027
00028 #include <cassert>
00029 #include <iostream>
00030
00031 namespace PPL = Parma_Polyhedra_Library;
00032
00033 void
00034 PPL::Grid::select_wider_congruences(const Grid& y,
00035 Congruence_System& cgs_selected) const {
00036
00037
00038 assert(space_dim == y.space_dim);
00039 assert(!marked_empty());
00040 assert(!y.marked_empty());
00041 assert(congruences_are_minimized());
00042 assert(y.congruences_are_minimized());
00043
00044
00045
00046 for (dimension_type dim = con_sys.space_dimension(), x_row = 0, y_row = 0;
00047 dim > 0; --dim) {
00048 assert(dim_kinds[dim] == CON_VIRTUAL
00049 || dim_kinds[dim] == y.dim_kinds[dim]);
00050 switch (dim_kinds[dim]) {
00051 case PROPER_CONGRUENCE:
00052 {
00053 const Congruence& cg = con_sys[x_row];
00054 const Congruence& y_cg = y.con_sys[y_row];
00055 if (cg.is_equal_at_dimension(dim, y_cg))
00056
00057 cgs_selected.insert(cg);
00058 ++x_row;
00059 ++y_row;
00060 }
00061 break;
00062 case EQUALITY:
00063 cgs_selected.insert(con_sys[x_row]);
00064 ++x_row;
00065 ++y_row;
00066 break;
00067 case CON_VIRTUAL:
00068 y.dim_kinds[dim] == CON_VIRTUAL || ++y_row;
00069 break;
00070 }
00071 }
00072 }
00073
00074 void
00075 PPL::Grid::widening_assign(const Grid& const_y, unsigned* tp) {
00076 Grid& x = *this;
00077 Grid& y = const_cast<Grid&>(const_y);
00078
00079 if (x.space_dim != y.space_dim)
00080 throw_dimension_incompatible("widening_assign(y)", "y", y);
00081
00082
00083
00084 #ifndef NDEBUG
00085 {
00086
00087 const Grid x_copy = x;
00088 const Grid y_copy = y;
00089 assert(x_copy.contains(y_copy));
00090 }
00091 #endif
00092
00093
00094 if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
00095 return;
00096
00097
00098 if (x.congruences_are_up_to_date()) {
00099 if (!x.congruences_are_minimized()) {
00100 if (simplify(x.con_sys, x.dim_kinds)) {
00101
00102 x.set_empty();
00103 return;
00104 }
00105 x.set_congruences_minimized();
00106 }
00107 }
00108 else
00109 x.update_congruences();
00110
00111
00112 if (y.congruences_are_up_to_date()) {
00113 if (!y.congruences_are_minimized()) {
00114 if (simplify(y.con_sys, y.dim_kinds)) {
00115
00116 y.set_empty();
00117 return;
00118 }
00119 y.set_congruences_minimized();
00120 }
00121 }
00122 else
00123 y.update_congruences();
00124
00125 if (con_sys.num_equalities() < y.con_sys.num_equalities())
00126 return;
00127
00128
00129
00130 Congruence_System cgs;
00131 x.select_wider_congruences(y, cgs);
00132
00133 if (cgs.num_rows() == con_sys.num_rows())
00134
00135 return;
00136
00137
00138
00139 Grid result(x.space_dim);
00140 result.add_recycled_congruences(cgs);
00141
00142
00143
00144 if (tp && *tp > 0) {
00145
00146
00147
00148 if (!x.contains(result))
00149 --(*tp);
00150 }
00151 else
00152
00153 std::swap(x, result);
00154
00155 assert(x.OK(true));
00156 }
00157
00158 void
00159 PPL::Grid::limited_extrapolation_assign(const Grid& y,
00160 const Congruence_System& cgs,
00161 unsigned* tp) {
00162 Grid& x = *this;
00163
00164
00165 if (x.space_dim != y.space_dim)
00166 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00167 "y", y);
00168
00169 const dimension_type cgs_space_dim = cgs.space_dimension();
00170 if (x.space_dim < cgs_space_dim)
00171 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00172 "cgs", cgs);
00173
00174 dimension_type cgs_num_rows = cgs.num_rows();
00175
00176 if (cgs_num_rows == 0) {
00177 x.widening_assign(y, tp);
00178 return;
00179 }
00180
00181 #ifndef NDEBUG
00182 {
00183
00184 const Grid x_copy = x;
00185 const Grid y_copy = y;
00186 assert(x_copy.contains(y_copy));
00187 }
00188 #endif
00189
00190 if (y.marked_empty())
00191 return;
00192 if (x.marked_empty())
00193 return;
00194
00195
00196
00197 if (x.space_dim == 0)
00198 return;
00199
00200
00201
00202
00203 if (!x.generators_are_up_to_date() && !x.update_generators())
00204
00205 return;
00206
00207 if (tp == NULL || *tp == 0) {
00208
00209 Congruence_System new_cgs;
00210
00211
00212
00213 for (dimension_type i = 0; i < cgs_num_rows; ++i) {
00214 const Congruence& cg = cgs[i];
00215 if (x.relation_with(cg) == Poly_Con_Relation::is_included())
00216 new_cgs.insert(cg);
00217 }
00218 x.widening_assign(y, tp);
00219 x.add_congruences(new_cgs);
00220 }
00221 else
00222
00223 x.widening_assign(y, tp);
00224
00225 assert(OK());
00226 }