Line data Source code
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 0 : static isl_stat increment_counter(struct isl_scan_callback *cb,
26 : __isl_take isl_vec *sample)
27 : {
28 0 : struct isl_counter *cnt = (struct isl_counter *)cb;
29 :
30 0 : isl_int_add_ui(cnt->count, cnt->count, 1);
31 :
32 0 : isl_vec_free(sample);
33 :
34 0 : if (isl_int_is_zero(cnt->max) || isl_int_lt(cnt->count, cnt->max))
35 0 : return isl_stat_ok;
36 0 : return isl_stat_error;
37 : }
38 :
39 0 : static int increment_range(struct isl_scan_callback *cb, isl_int min, isl_int max)
40 : {
41 0 : struct isl_counter *cnt = (struct isl_counter *)cb;
42 :
43 0 : isl_int_add(cnt->count, cnt->count, max);
44 0 : isl_int_sub(cnt->count, cnt->count, min);
45 0 : isl_int_add_ui(cnt->count, cnt->count, 1);
46 :
47 0 : if (isl_int_is_zero(cnt->max) || isl_int_lt(cnt->count, cnt->max))
48 0 : return 0;
49 0 : isl_int_set(cnt->count, cnt->max);
50 0 : return -1;
51 : }
52 :
53 : /* Call callback->add with the current sample value of the tableau "tab".
54 : */
55 0 : static int add_solution(struct isl_tab *tab, struct isl_scan_callback *callback)
56 : {
57 : struct isl_vec *sample;
58 :
59 0 : if (!tab)
60 0 : return -1;
61 0 : sample = isl_tab_get_sample_value(tab);
62 0 : if (!sample)
63 0 : return -1;
64 :
65 0 : return callback->add(callback, sample);
66 : }
67 :
68 0 : 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 0 : sample = isl_vec_alloc(bset->ctx, 1);
74 0 : isl_basic_set_free(bset);
75 :
76 0 : if (!sample)
77 0 : return isl_stat_error;
78 :
79 0 : isl_int_set_si(sample->el[0], 1);
80 :
81 0 : 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 0 : isl_stat isl_basic_set_scan(__isl_take isl_basic_set *bset,
103 : struct isl_scan_callback *callback)
104 : {
105 : unsigned dim;
106 0 : struct isl_mat *B = NULL;
107 0 : 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 0 : if (!bset)
116 0 : return isl_stat_error;
117 :
118 0 : dim = isl_basic_set_total_dim(bset);
119 0 : if (dim == 0)
120 0 : return scan_0D(bset, callback);
121 :
122 0 : min = isl_vec_alloc(bset->ctx, dim);
123 0 : max = isl_vec_alloc(bset->ctx, dim);
124 0 : snap = isl_alloc_array(bset->ctx, struct isl_tab_undo *, dim);
125 :
126 0 : if (!min || !max || !snap)
127 : goto error;
128 :
129 0 : tab = isl_tab_from_basic_set(bset, 0);
130 0 : if (!tab)
131 0 : goto error;
132 0 : if (isl_tab_extend_cons(tab, dim + 1) < 0)
133 0 : goto error;
134 :
135 0 : tab->basis = isl_mat_identity(bset->ctx, 1 + dim);
136 : if (1)
137 0 : tab = isl_tab_compute_reduced_basis(tab);
138 0 : if (!tab)
139 0 : goto error;
140 0 : B = isl_mat_copy(tab->basis);
141 0 : if (!B)
142 0 : goto error;
143 :
144 0 : level = 0;
145 0 : init = 1;
146 :
147 0 : while (level >= 0) {
148 0 : int empty = 0;
149 0 : if (init) {
150 0 : res = isl_tab_min(tab, B->row[1 + level],
151 0 : bset->ctx->one, &min->el[level], NULL, 0);
152 0 : if (res == isl_lp_empty)
153 0 : empty = 1;
154 0 : if (res == isl_lp_error || res == isl_lp_unbounded)
155 : goto error;
156 0 : isl_seq_neg(B->row[1 + level] + 1,
157 0 : B->row[1 + level] + 1, dim);
158 0 : res = isl_tab_min(tab, B->row[1 + level],
159 0 : bset->ctx->one, &max->el[level], NULL, 0);
160 0 : isl_seq_neg(B->row[1 + level] + 1,
161 0 : B->row[1 + level] + 1, dim);
162 0 : isl_int_neg(max->el[level], max->el[level]);
163 0 : if (res == isl_lp_empty)
164 0 : empty = 1;
165 0 : if (res == isl_lp_error || res == isl_lp_unbounded)
166 : goto error;
167 0 : snap[level] = isl_tab_snap(tab);
168 : } else
169 0 : isl_int_add_ui(min->el[level], min->el[level], 1);
170 :
171 0 : if (empty || isl_int_gt(min->el[level], max->el[level])) {
172 0 : level--;
173 0 : init = 0;
174 0 : if (level >= 0)
175 0 : if (isl_tab_rollback(tab, snap[level]) < 0)
176 0 : goto error;
177 0 : continue;
178 : }
179 0 : if (level == dim - 1 && callback->add == increment_counter) {
180 0 : if (increment_range(callback,
181 0 : min->el[level], max->el[level]))
182 0 : goto error;
183 0 : level--;
184 0 : init = 0;
185 0 : if (level >= 0)
186 0 : if (isl_tab_rollback(tab, snap[level]) < 0)
187 0 : goto error;
188 0 : continue;
189 : }
190 0 : isl_int_neg(B->row[1 + level][0], min->el[level]);
191 0 : if (isl_tab_add_valid_eq(tab, B->row[1 + level]) < 0)
192 0 : goto error;
193 0 : isl_int_set_si(B->row[1 + level][0], 0);
194 0 : if (level < dim - 1) {
195 0 : ++level;
196 0 : init = 1;
197 0 : continue;
198 : }
199 0 : if (add_solution(tab, callback) < 0)
200 0 : goto error;
201 0 : init = 0;
202 0 : if (isl_tab_rollback(tab, snap[level]) < 0)
203 0 : goto error;
204 : }
205 :
206 0 : isl_tab_free(tab);
207 0 : free(snap);
208 0 : isl_vec_free(min);
209 0 : isl_vec_free(max);
210 0 : isl_basic_set_free(bset);
211 0 : isl_mat_free(B);
212 0 : return isl_stat_ok;
213 : error:
214 0 : isl_tab_free(tab);
215 0 : free(snap);
216 0 : isl_vec_free(min);
217 0 : isl_vec_free(max);
218 0 : isl_basic_set_free(bset);
219 0 : isl_mat_free(B);
220 0 : return isl_stat_error;
221 : }
222 :
223 0 : isl_stat isl_set_scan(__isl_take isl_set *set,
224 : struct isl_scan_callback *callback)
225 : {
226 : int i;
227 :
228 0 : if (!set || !callback)
229 : goto error;
230 :
231 0 : set = isl_set_cow(set);
232 0 : set = isl_set_make_disjoint(set);
233 0 : set = isl_set_compute_divs(set);
234 0 : if (!set)
235 0 : goto error;
236 :
237 0 : for (i = 0; i < set->n; ++i)
238 0 : if (isl_basic_set_scan(isl_basic_set_copy(set->p[i]),
239 : callback) < 0)
240 0 : goto error;
241 :
242 0 : isl_set_free(set);
243 0 : return isl_stat_ok;
244 : error:
245 0 : isl_set_free(set);
246 0 : return isl_stat_error;
247 : }
248 :
249 0 : int isl_basic_set_count_upto(__isl_keep isl_basic_set *bset,
250 : isl_int max, isl_int *count)
251 : {
252 0 : struct isl_counter cnt = { { &increment_counter } };
253 :
254 0 : if (!bset)
255 0 : return -1;
256 :
257 0 : isl_int_init(cnt.count);
258 0 : isl_int_init(cnt.max);
259 :
260 0 : isl_int_set_si(cnt.count, 0);
261 0 : isl_int_set(cnt.max, max);
262 0 : if (isl_basic_set_scan(isl_basic_set_copy(bset), &cnt.callback) < 0 &&
263 0 : isl_int_lt(cnt.count, cnt.max))
264 0 : goto error;
265 :
266 0 : isl_int_set(*count, cnt.count);
267 0 : isl_int_clear(cnt.max);
268 0 : isl_int_clear(cnt.count);
269 :
270 0 : return 0;
271 : error:
272 0 : isl_int_clear(cnt.count);
273 0 : return -1;
274 : }
275 :
276 0 : int isl_set_count_upto(__isl_keep isl_set *set, isl_int max, isl_int *count)
277 : {
278 0 : struct isl_counter cnt = { { &increment_counter } };
279 :
280 0 : if (!set)
281 0 : return -1;
282 :
283 0 : isl_int_init(cnt.count);
284 0 : isl_int_init(cnt.max);
285 :
286 0 : isl_int_set_si(cnt.count, 0);
287 0 : isl_int_set(cnt.max, max);
288 0 : if (isl_set_scan(isl_set_copy(set), &cnt.callback) < 0 &&
289 0 : isl_int_lt(cnt.count, cnt.max))
290 0 : goto error;
291 :
292 0 : isl_int_set(*count, cnt.count);
293 0 : isl_int_clear(cnt.max);
294 0 : isl_int_clear(cnt.count);
295 :
296 0 : return 0;
297 : error:
298 0 : isl_int_clear(cnt.count);
299 0 : return -1;
300 : }
301 :
302 0 : int isl_set_count(__isl_keep isl_set *set, isl_int *count)
303 : {
304 0 : if (!set)
305 0 : return -1;
306 0 : return isl_set_count_upto(set, set->ctx->zero, count);
307 : }
308 :
309 : /* Count the total number of elements in "set" (in an inefficient way) and
310 : * return the result.
311 : */
312 0 : __isl_give isl_val *isl_set_count_val(__isl_keep isl_set *set)
313 : {
314 : isl_val *v;
315 :
316 0 : if (!set)
317 0 : return NULL;
318 0 : v = isl_val_zero(isl_set_get_ctx(set));
319 0 : v = isl_val_cow(v);
320 0 : if (!v)
321 0 : return NULL;
322 0 : if (isl_set_count(set, &v->n) < 0)
323 0 : v = isl_val_free(v);
324 0 : return v;
325 : }
|
