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