1 /* 2 * Copyright 2008-2009 Katholieke Universiteit Leuven 3 * 4 * Use of this software is governed by the MIT license 5 * 6 * Written by Sven Verdoolaege, K.U.Leuven, Departement 7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium 8 */ 9 10 #include <isl_ctx_private.h> 11 #include <isl_map_private.h> 12 #include "isl_basis_reduction.h" 13 #include "isl_scan.h" 14 #include <isl_seq.h> 15 #include "isl_tab.h" 16 #include <isl_val_private.h> 17 #include <isl_vec_private.h> 18 19 struct isl_counter { 20 struct isl_scan_callback callback; 21 isl_int count; 22 isl_int max; 23 }; 24 25 static isl_stat increment_counter(struct isl_scan_callback *cb, 26 __isl_take isl_vec *sample) 27 { 28 struct isl_counter *cnt = (struct isl_counter *)cb; 29 30 isl_int_add_ui(cnt->count, cnt->count, 1); 31 32 isl_vec_free(sample); 33 34 if (isl_int_is_zero(cnt->max) || isl_int_lt(cnt->count, cnt->max)) 35 return isl_stat_ok; 36 return isl_stat_error; 37 } 38 39 static int increment_range(struct isl_scan_callback *cb, isl_int min, isl_int max) 40 { 41 struct isl_counter *cnt = (struct isl_counter *)cb; 42 43 isl_int_add(cnt->count, cnt->count, max); 44 isl_int_sub(cnt->count, cnt->count, min); 45 isl_int_add_ui(cnt->count, cnt->count, 1); 46 47 if (isl_int_is_zero(cnt->max) || isl_int_lt(cnt->count, cnt->max)) 48 return 0; 49 isl_int_set(cnt->count, cnt->max); 50 return -1; 51 } 52 53 /* Call callback->add with the current sample value of the tableau "tab". 54 */ 55 static int add_solution(struct isl_tab *tab, struct isl_scan_callback *callback) 56 { 57 struct isl_vec *sample; 58 59 if (!tab) 60 return -1; 61 sample = isl_tab_get_sample_value(tab); 62 if (!sample) 63 return -1; 64 65 return callback->add(callback, sample); 66 } 67 68 static isl_stat scan_0D(__isl_take isl_basic_set *bset, 69 struct isl_scan_callback *callback) 70 { 71 struct isl_vec *sample; 72 73 sample = isl_vec_alloc(bset->ctx, 1); 74 isl_basic_set_free(bset); 75 76 if (!sample) 77 return isl_stat_error; 78 79 isl_int_set_si(sample->el[0], 1); 80 81 return callback->add(callback, sample); 82 } 83 84 /* Look for all integer points in "bset", which is assumed to be bounded, 85 * and call callback->add on each of them. 86 * 87 * We first compute a reduced basis for the set and then scan 88 * the set in the directions of this basis. 89 * We basically perform a depth first search, where in each level i 90 * we compute the range in the i-th basis vector direction, given 91 * fixed values in the directions of the previous basis vector. 92 * We then add an equality to the tableau fixing the value in the 93 * direction of the current basis vector to each value in the range 94 * in turn and then continue to the next level. 95 * 96 * The search is implemented iteratively. "level" identifies the current 97 * basis vector. "init" is true if we want the first value at the current 98 * level and false if we want the next value. 99 * Solutions are added in the leaves of the search tree, i.e., after 100 * we have fixed a value in each direction of the basis. 101 */ 102 isl_stat isl_basic_set_scan(__isl_take isl_basic_set *bset, 103 struct isl_scan_callback *callback) 104 { 105 isl_size dim; 106 struct isl_mat *B = NULL; 107 struct isl_tab *tab = NULL; 108 struct isl_vec *min; 109 struct isl_vec *max; 110 struct isl_tab_undo **snap; 111 int level; 112 int init; 113 enum isl_lp_result res; 114 115 dim = isl_basic_set_dim(bset, isl_dim_all); 116 if (dim < 0) { 117 bset = isl_basic_set_free(bset); 118 return isl_stat_error; 119 } 120 121 if (dim == 0) 122 return scan_0D(bset, callback); 123 124 min = isl_vec_alloc(bset->ctx, dim); 125 max = isl_vec_alloc(bset->ctx, dim); 126 snap = isl_alloc_array(bset->ctx, struct isl_tab_undo *, dim); 127 128 if (!min || !max || !snap) 129 goto error; 130 131 tab = isl_tab_from_basic_set(bset, 0); 132 if (!tab) 133 goto error; 134 if (isl_tab_extend_cons(tab, dim + 1) < 0) 135 goto error; 136 137 tab->basis = isl_mat_identity(bset->ctx, 1 + dim); 138 if (1) 139 tab = isl_tab_compute_reduced_basis(tab); 140 if (!tab) 141 goto error; 142 B = isl_mat_copy(tab->basis); 143 if (!B) 144 goto error; 145 146 level = 0; 147 init = 1; 148 149 while (level >= 0) { 150 int empty = 0; 151 if (init) { 152 res = isl_tab_min(tab, B->row[1 + level], 153 bset->ctx->one, &min->el[level], NULL, 0); 154 if (res == isl_lp_empty) 155 empty = 1; 156 if (res == isl_lp_error || res == isl_lp_unbounded) 157 goto error; 158 isl_seq_neg(B->row[1 + level] + 1, 159 B->row[1 + level] + 1, dim); 160 res = isl_tab_min(tab, B->row[1 + level], 161 bset->ctx->one, &max->el[level], NULL, 0); 162 isl_seq_neg(B->row[1 + level] + 1, 163 B->row[1 + level] + 1, dim); 164 isl_int_neg(max->el[level], max->el[level]); 165 if (res == isl_lp_empty) 166 empty = 1; 167 if (res == isl_lp_error || res == isl_lp_unbounded) 168 goto error; 169 snap[level] = isl_tab_snap(tab); 170 } else 171 isl_int_add_ui(min->el[level], min->el[level], 1); 172 173 if (empty || isl_int_gt(min->el[level], max->el[level])) { 174 level--; 175 init = 0; 176 if (level >= 0) 177 if (isl_tab_rollback(tab, snap[level]) < 0) 178 goto error; 179 continue; 180 } 181 if (level == dim - 1 && callback->add == increment_counter) { 182 if (increment_range(callback, 183 min->el[level], max->el[level])) 184 goto error; 185 level--; 186 init = 0; 187 if (level >= 0) 188 if (isl_tab_rollback(tab, snap[level]) < 0) 189 goto error; 190 continue; 191 } 192 isl_int_neg(B->row[1 + level][0], min->el[level]); 193 if (isl_tab_add_valid_eq(tab, B->row[1 + level]) < 0) 194 goto error; 195 isl_int_set_si(B->row[1 + level][0], 0); 196 if (level < dim - 1) { 197 ++level; 198 init = 1; 199 continue; 200 } 201 if (add_solution(tab, callback) < 0) 202 goto error; 203 init = 0; 204 if (isl_tab_rollback(tab, snap[level]) < 0) 205 goto error; 206 } 207 208 isl_tab_free(tab); 209 free(snap); 210 isl_vec_free(min); 211 isl_vec_free(max); 212 isl_basic_set_free(bset); 213 isl_mat_free(B); 214 return isl_stat_ok; 215 error: 216 isl_tab_free(tab); 217 free(snap); 218 isl_vec_free(min); 219 isl_vec_free(max); 220 isl_basic_set_free(bset); 221 isl_mat_free(B); 222 return isl_stat_error; 223 } 224 225 isl_stat isl_set_scan(__isl_take isl_set *set, 226 struct isl_scan_callback *callback) 227 { 228 int i; 229 230 if (!set || !callback) 231 goto error; 232 233 set = isl_set_cow(set); 234 set = isl_set_make_disjoint(set); 235 set = isl_set_compute_divs(set); 236 if (!set) 237 goto error; 238 239 for (i = 0; i < set->n; ++i) 240 if (isl_basic_set_scan(isl_basic_set_copy(set->p[i]), 241 callback) < 0) 242 goto error; 243 244 isl_set_free(set); 245 return isl_stat_ok; 246 error: 247 isl_set_free(set); 248 return isl_stat_error; 249 } 250 251 int isl_basic_set_count_upto(__isl_keep isl_basic_set *bset, 252 isl_int max, isl_int *count) 253 { 254 struct isl_counter cnt = { { &increment_counter } }; 255 256 if (!bset) 257 return -1; 258 259 isl_int_init(cnt.count); 260 isl_int_init(cnt.max); 261 262 isl_int_set_si(cnt.count, 0); 263 isl_int_set(cnt.max, max); 264 if (isl_basic_set_scan(isl_basic_set_copy(bset), &cnt.callback) < 0 && 265 isl_int_lt(cnt.count, cnt.max)) 266 goto error; 267 268 isl_int_set(*count, cnt.count); 269 isl_int_clear(cnt.max); 270 isl_int_clear(cnt.count); 271 272 return 0; 273 error: 274 isl_int_clear(cnt.count); 275 return -1; 276 } 277 278 int isl_set_count_upto(__isl_keep isl_set *set, isl_int max, isl_int *count) 279 { 280 struct isl_counter cnt = { { &increment_counter } }; 281 282 if (!set) 283 return -1; 284 285 isl_int_init(cnt.count); 286 isl_int_init(cnt.max); 287 288 isl_int_set_si(cnt.count, 0); 289 isl_int_set(cnt.max, max); 290 if (isl_set_scan(isl_set_copy(set), &cnt.callback) < 0 && 291 isl_int_lt(cnt.count, cnt.max)) 292 goto error; 293 294 isl_int_set(*count, cnt.count); 295 isl_int_clear(cnt.max); 296 isl_int_clear(cnt.count); 297 298 return 0; 299 error: 300 isl_int_clear(cnt.count); 301 return -1; 302 } 303 304 int isl_set_count(__isl_keep isl_set *set, isl_int *count) 305 { 306 if (!set) 307 return -1; 308 return isl_set_count_upto(set, set->ctx->zero, count); 309 } 310 311 /* Count the total number of elements in "set" (in an inefficient way) and 312 * return the result. 313 */ 314 __isl_give isl_val *isl_set_count_val(__isl_keep isl_set *set) 315 { 316 isl_val *v; 317 318 if (!set) 319 return NULL; 320 v = isl_val_zero(isl_set_get_ctx(set)); 321 v = isl_val_cow(v); 322 if (!v) 323 return NULL; 324 if (isl_set_count(set, &v->n) < 0) 325 v = isl_val_free(v); 326 return v; 327 } 328
Indexes created Mon Mar 02 05:31:46 UTC 2026