328 lines · c
1/*2 * Copyright 2008-2009 Katholieke Universiteit Leuven3 *4 * Use of this software is governed by the MIT license5 *6 * Written by Sven Verdoolaege, K.U.Leuven, Departement7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium8 */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 19struct isl_counter {20 struct isl_scan_callback callback;21 isl_int count;22 isl_int max;23};24 25static 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 39static 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 */55static 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 68static 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 scan88 * the set in the directions of this basis.89 * We basically perform a depth first search, where in each level i90 * we compute the range in the i-th basis vector direction, given91 * fixed values in the directions of the previous basis vector.92 * We then add an equality to the tableau fixing the value in the93 * direction of the current basis vector to each value in the range94 * in turn and then continue to the next level.95 *96 * The search is implemented iteratively. "level" identifies the current97 * basis vector. "init" is true if we want the first value at the current98 * level and false if we want the next value.99 * Solutions are added in the leaves of the search tree, i.e., after100 * we have fixed a value in each direction of the basis.101 */102isl_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 } else171 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;215error: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 225isl_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;246error:247 isl_set_free(set);248 return isl_stat_error;249}250 251int 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;273error:274 isl_int_clear(cnt.count);275 return -1;276}277 278int 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;299error:300 isl_int_clear(cnt.count);301 return -1;302}303 304int 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) and312 * 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