Line data Source code
1 : /*
2 : * Copyright 2008-2009 Katholieke Universiteit Leuven
3 : * Copyright 2010 INRIA Saclay
4 : * Copyright 2011 Sven Verdoolaege
5 : *
6 : * Use of this software is governed by the MIT license
7 : *
8 : * Written by Sven Verdoolaege, K.U.Leuven, Departement
9 : * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
10 : * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
11 : * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
12 : */
13 :
14 : #define xSF(TYPE,SUFFIX) TYPE ## SUFFIX
15 : #define SF(TYPE,SUFFIX) xSF(TYPE,SUFFIX)
16 :
17 : /* Given a basic map with at least two parallel constraints (as found
18 : * by the function parallel_constraints), first look for more constraints
19 : * parallel to the two constraint and replace the found list of parallel
20 : * constraints by a single constraint with as "input" part the minimum
21 : * of the input parts of the list of constraints. Then, recursively call
22 : * basic_map_partial_lexopt (possibly finding more parallel constraints)
23 : * and plug in the definition of the minimum in the result.
24 : *
25 : * As in parallel_constraints, only inequality constraints that only
26 : * involve input variables that do not occur in any other inequality
27 : * constraints are considered.
28 : *
29 : * More specifically, given a set of constraints
30 : *
31 : * a x + b_i(p) >= 0
32 : *
33 : * Replace this set by a single constraint
34 : *
35 : * a x + u >= 0
36 : *
37 : * with u a new parameter with constraints
38 : *
39 : * u <= b_i(p)
40 : *
41 : * Any solution to the new system is also a solution for the original system
42 : * since
43 : *
44 : * a x >= -u >= -b_i(p)
45 : *
46 : * Moreover, m = min_i(b_i(p)) satisfies the constraints on u and can
47 : * therefore be plugged into the solution.
48 : */
49 0 : static TYPE *SF(basic_map_partial_lexopt_symm,SUFFIX)(
50 : __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
51 : __isl_give isl_set **empty, int max, int first, int second)
52 : {
53 : int i, n, k;
54 0 : int *list = NULL;
55 : unsigned n_in, n_out, n_div;
56 : isl_ctx *ctx;
57 0 : isl_vec *var = NULL;
58 0 : isl_mat *cst = NULL;
59 : isl_space *map_space, *set_space;
60 :
61 0 : map_space = isl_basic_map_get_space(bmap);
62 0 : set_space = empty ? isl_basic_set_get_space(dom) : NULL;
63 :
64 0 : n_in = isl_basic_map_dim(bmap, isl_dim_param) +
65 0 : isl_basic_map_dim(bmap, isl_dim_in);
66 0 : n_out = isl_basic_map_dim(bmap, isl_dim_all) - n_in;
67 :
68 0 : ctx = isl_basic_map_get_ctx(bmap);
69 0 : list = isl_alloc_array(ctx, int, bmap->n_ineq);
70 0 : var = isl_vec_alloc(ctx, n_out);
71 0 : if ((bmap->n_ineq && !list) || (n_out && !var))
72 : goto error;
73 :
74 0 : list[0] = first;
75 0 : list[1] = second;
76 0 : isl_seq_cpy(var->el, bmap->ineq[first] + 1 + n_in, n_out);
77 0 : for (i = second + 1, n = 2; i < bmap->n_ineq; ++i) {
78 0 : if (isl_seq_eq(var->el, bmap->ineq[i] + 1 + n_in, n_out) &&
79 0 : all_single_occurrence(bmap, i, n_in))
80 0 : list[n++] = i;
81 : }
82 :
83 0 : cst = isl_mat_alloc(ctx, n, 1 + n_in);
84 0 : if (!cst)
85 0 : goto error;
86 :
87 0 : for (i = 0; i < n; ++i)
88 0 : isl_seq_cpy(cst->row[i], bmap->ineq[list[i]], 1 + n_in);
89 :
90 0 : bmap = isl_basic_map_cow(bmap);
91 0 : if (!bmap)
92 0 : goto error;
93 0 : for (i = n - 1; i >= 0; --i)
94 0 : if (isl_basic_map_drop_inequality(bmap, list[i]) < 0)
95 0 : goto error;
96 :
97 0 : bmap = isl_basic_map_add_dims(bmap, isl_dim_in, 1);
98 0 : bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
99 0 : k = isl_basic_map_alloc_inequality(bmap);
100 0 : if (k < 0)
101 0 : goto error;
102 0 : isl_seq_clr(bmap->ineq[k], 1 + n_in);
103 0 : isl_int_set_si(bmap->ineq[k][1 + n_in], 1);
104 0 : isl_seq_cpy(bmap->ineq[k] + 1 + n_in + 1, var->el, n_out);
105 0 : bmap = isl_basic_map_finalize(bmap);
106 :
107 0 : n_div = isl_basic_set_dim(dom, isl_dim_div);
108 0 : dom = isl_basic_set_add_dims(dom, isl_dim_set, 1);
109 0 : dom = isl_basic_set_extend_constraints(dom, 0, n);
110 0 : for (i = 0; i < n; ++i) {
111 0 : k = isl_basic_set_alloc_inequality(dom);
112 0 : if (k < 0)
113 0 : goto error;
114 0 : isl_seq_cpy(dom->ineq[k], cst->row[i], 1 + n_in);
115 0 : isl_int_set_si(dom->ineq[k][1 + n_in], -1);
116 0 : isl_seq_clr(dom->ineq[k] + 1 + n_in + 1, n_div);
117 : }
118 :
119 0 : isl_vec_free(var);
120 0 : free(list);
121 :
122 0 : return SF(basic_map_partial_lexopt_symm_core,SUFFIX)(bmap, dom, empty,
123 : max, cst, map_space, set_space);
124 : error:
125 0 : isl_space_free(map_space);
126 0 : isl_space_free(set_space);
127 0 : isl_mat_free(cst);
128 0 : isl_vec_free(var);
129 0 : free(list);
130 0 : isl_basic_set_free(dom);
131 0 : isl_basic_map_free(bmap);
132 0 : return NULL;
133 : }
134 :
135 : /* Recursive part of isl_tab_basic_map_partial_lexopt*, after detecting
136 : * equalities and removing redundant constraints.
137 : *
138 : * We first check if there are any parallel constraints (left).
139 : * If not, we are in the base case.
140 : * If there are parallel constraints, we replace them by a single
141 : * constraint in basic_map_partial_lexopt_symm_pma and then call
142 : * this function recursively to look for more parallel constraints.
143 : */
144 0 : static __isl_give TYPE *SF(basic_map_partial_lexopt,SUFFIX)(
145 : __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
146 : __isl_give isl_set **empty, int max)
147 : {
148 0 : isl_bool par = isl_bool_false;
149 : int first, second;
150 :
151 0 : if (!bmap)
152 0 : goto error;
153 :
154 0 : if (bmap->ctx->opt->pip_symmetry)
155 0 : par = parallel_constraints(bmap, &first, &second);
156 0 : if (par < 0)
157 0 : goto error;
158 0 : if (!par)
159 0 : return SF(basic_map_partial_lexopt_base,SUFFIX)(bmap, dom,
160 : empty, max);
161 :
162 0 : return SF(basic_map_partial_lexopt_symm,SUFFIX)(bmap, dom, empty, max,
163 : first, second);
164 : error:
165 0 : isl_basic_set_free(dom);
166 0 : isl_basic_map_free(bmap);
167 0 : return NULL;
168 : }
169 :
170 : /* Compute the lexicographic minimum (or maximum if "flags" includes
171 : * ISL_OPT_MAX) of "bmap" over the domain "dom" and return the result as
172 : * either a map or a piecewise multi-affine expression depending on TYPE.
173 : * If "empty" is not NULL, then *empty is assigned a set that
174 : * contains those parts of the domain where there is no solution.
175 : * If "flags" includes ISL_OPT_FULL, then "dom" is NULL and the optimum
176 : * should be computed over the domain of "bmap". "empty" is also NULL
177 : * in this case.
178 : * If "bmap" is marked as rational (ISL_BASIC_MAP_RATIONAL),
179 : * then we compute the rational optimum. Otherwise, we compute
180 : * the integral optimum.
181 : *
182 : * We perform some preprocessing. As the PILP solver does not
183 : * handle implicit equalities very well, we first make sure all
184 : * the equalities are explicitly available.
185 : *
186 : * We also add context constraints to the basic map and remove
187 : * redundant constraints. This is only needed because of the
188 : * way we handle simple symmetries. In particular, we currently look
189 : * for symmetries on the constraints, before we set up the main tableau.
190 : * It is then no good to look for symmetries on possibly redundant constraints.
191 : * If the domain was extracted from the basic map, then there is
192 : * no need to add back those constraints again.
193 : */
194 0 : __isl_give TYPE *SF(isl_tab_basic_map_partial_lexopt,SUFFIX)(
195 : __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
196 : __isl_give isl_set **empty, unsigned flags)
197 : {
198 : int max, full;
199 : isl_bool compatible;
200 :
201 0 : if (empty)
202 0 : *empty = NULL;
203 :
204 0 : full = ISL_FL_ISSET(flags, ISL_OPT_FULL);
205 0 : if (full)
206 0 : dom = extract_domain(bmap, flags);
207 0 : compatible = isl_basic_map_compatible_domain(bmap, dom);
208 0 : if (compatible < 0)
209 0 : goto error;
210 0 : if (!compatible)
211 0 : isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid,
212 : "domain does not match input", goto error);
213 :
214 0 : max = ISL_FL_ISSET(flags, ISL_OPT_MAX);
215 0 : if (isl_basic_set_dim(dom, isl_dim_all) == 0)
216 0 : return SF(basic_map_partial_lexopt,SUFFIX)(bmap, dom, empty,
217 : max);
218 :
219 0 : if (!full)
220 0 : bmap = isl_basic_map_intersect_domain(bmap,
221 : isl_basic_set_copy(dom));
222 0 : bmap = isl_basic_map_detect_equalities(bmap);
223 0 : bmap = isl_basic_map_remove_redundancies(bmap);
224 :
225 0 : return SF(basic_map_partial_lexopt,SUFFIX)(bmap, dom, empty, max);
226 : error:
227 0 : isl_basic_set_free(dom);
228 0 : isl_basic_map_free(bmap);
229 0 : return NULL;
230 : }
|
