barvinok 0.32
[barvinok.git] / doc / isl.tex
blobd32c5a246023ee391ebb12755cf3d45ac7736d1e
1 \section{\protect\isl/ interface}
3 \subsection{Library}
5 The \barvinok/ library currently supports only a few
6 functions that interface with the \isl/ library.
7 In time, this interface will grow and is set to replace
8 the \PolyLib/ interface.
9 For more information on the \isl/ data structures, see
10 the \isl/ user manual.
12 \begin{verbatim}
13 __isl_give isl_pw_qpolynomial *isl_set_card(__isl_take isl_set *set);
14 __isl_give isl_union_pw_qpolynomial *isl_union_set_card(
15 __isl_take isl_union_set *uset);
16 \end{verbatim}
17 Compute the number of elements in an \ai[\tt]{isl\_set}
18 or \ai[\tt]{isl\_union\_set}.
19 The resulting \ai[\tt]{isl\_pw\_qpolynomial}
20 or \ai[\tt]{isl\_union\_pw\_qpolynomial} has purely parametric cells.
22 \begin{verbatim}
23 __isl_give isl_pw_qpolynomial *isl_map_card(__isl_take isl_map *map);
24 __isl_give isl_union_pw_qpolynomial *isl_union_map_card(
25 __isl_take isl_union_map *umap);
26 \end{verbatim}
27 Compute a closed form expression for the number of image elements
28 associated to any element in the domain of the given \ai[\tt]{isl\_map}
29 or \ai[\tt]{isl\_union\_map}.
30 The union of the cells in the resulting \ai[\tt]{isl\_pw\_qpolynomial}
31 is equal to the domain of the input \ai[\tt]{isl\_map}.
33 \begin{verbatim}
34 __isl_give isl_pw_qpolynomial *isl_pw_qpolynomial_sum(
35 __isl_take isl_pw_qpolynomial *pwqp);
36 __isl_give isl_union_pw_qpolynomial *isl_union_pw_qpolynomial_sum(
37 __isl_take isl_union_pw_qpolynomial *upwqp);
38 \end{verbatim}
39 Compute the sum of the given piecewise quasipolynomial over
40 all integer points in the domain. The result is a piecewise
41 quasipolynomial that only involves the parameters.
42 If, however, the domain of the piecewise quasipolynomial wraps
43 a relation, then the sum is computed over all integer points
44 in the range of that relation and the domain of the relation
45 becomes the domain of the result.
47 \begin{verbatim}
48 __isl_give isl_pw_qpolynomial *isl_map_apply_pw_qpolynomial(
49 __isl_take isl_map *map, __isl_take isl_pw_qpolynomial *pwqp);
50 __isl_give isl_union_pw_qpolynomial *isl_union_map_apply_union_pw_qpolynomial(
51 __isl_take isl_union_map *umap,
52 __isl_take isl_union_pw_qpolynomial *upwqp);
53 \end{verbatim}
54 Compose the given map with the given piecewise quasipolynomial.
55 That is, compute the sum over all elements in the intersection
56 of the range of the map and the domain of the piecewise quasipolynomial
57 as a function of an element in the domain of the map.
59 \subsection{Calculator}
61 The \ai[\tt]{iscc} calculator offers an interface to some
62 of the functionality provided by the \isl/ and \barvinok/
63 libraries.
64 The supported operations are shown in \autoref{t:iscc}.
65 Note that when an operation requires an argument of a certain
66 type, a binary list with the first element of the required type
67 may also be used instead.
68 Here are some examples:
69 \begin{verbatim}
70 P := [n, m] -> { [i,j] : 0 <= i <= n and i <= j <= m };
71 card P;
73 f := [n,m] -> { [i,j] -> i*j + n*i*i*j : i,j >= 0 and 5i + 27j <= n+m };
74 sum f;
75 s := sum f;
76 s @ [n,m] -> { [] : 0 <= n,m <= 20 };
78 f := [n] -> { [i] -> 2*n*i - n*n + 3*n - 1/2*i*i - 3/2*i-1 :
79 (exists j : 0 <= i < 4*n-1 and 0 <= j < n and
80 2*n-1 <= i+j <= 4*n-2 and i <= 2*n-1 ) };
81 ub f;
82 u := (ub f)[0];
83 u @ [n] -> { [] : 0 <= n <= 10 };
85 m := [n] -> { [i,j] -> [i+1,j+1] : 1 <= i,j < n;
86 [i,j] -> [i+1,j-1] : 1 <= i < n and 2 <= j <= n };
87 m^+;
88 (m^+)[0];
90 codegen [N] -> { A[i] -> [i,0] : 0 <= i <= N; B[i] -> [i,1] : 1 <= i <= N };
92 { [k] -> [i] : 1 <= i <= k } . { [n] -> 2 * n : n >= 1 };
94 { [m] -> [c] : 1 <= c <= m } . { [k] -> max((3 * k + k^2)) : k >= 1 };
95 \end{verbatim}
97 \bottomcaption{{\tt iscc} operations. The variables
98 have the following types,
99 $s$: set,
100 $m$: map,
101 $q$: piecewise quasipolynomial,
102 $f$: piecewise quasipolynomial fold,
103 $l$: list,
104 $i$: integer,
105 $b$: boolean,
106 $S$: string,
107 $o$: object of any type
109 \label{t:iscc}
110 \tablehead{
111 \hline
112 Syntax & Meaning
114 \hline
116 \tabletail{
117 \multicolumn{2}{r}{\small\sl continued on next page}
120 \tablelasttail{}
121 \begin{supertabular}{lp{0.7\textwidth}}
122 $s_2$ := \ai[\tt]{aff} $s_1$ & affine hull of $s_1$
124 $m_2$ := \ai[\tt]{aff} $m_1$ & affine hull of $m_1$
126 $q$ := \ai[\tt]{card} $s$ &
127 number of elements in the set $s$
129 $q$ := \ai[\tt]{card} $m$ &
130 number of elements in the image of a domain element
132 $s_2$ := \ai[\tt]{coalesce} $s_1$ &
133 simplify the representation of set $s_1$ by trying
134 to combine pairs of basic sets into a single
135 basic set
137 $m_2$ := \ai[\tt]{coalesce} $m_1$ &
138 simplify the representation of map $m_1$ by trying
139 to combine pairs of basic maps into a single
140 basic map
142 $q_2$ := \ai[\tt]{coalesce} $q_1$ &
143 simplify the representation of $q_1$ by trying
144 to combine pairs of basic sets in the domain
145 of $q_1$ into a single basic set
147 $f_2$ := \ai[\tt]{coalesce} $f_1$ &
148 simplify the representation of $f_1$ by trying
149 to combine pairs of basic sets in the domain
150 of $f_1$ into a single basic set
152 \ai[\tt]{codegen} $s$ &
153 generate code for the given domain.
154 This operation is only available if \ai[\tt]{CLooG}
155 support was compiled in.
157 \ai[\tt]{codegen} $m$ &
158 generate code for the given scattering function.
159 This operation is only available if \ai[\tt]{CLooG}
160 support was compiled in.
162 $s_3$ := $s_1$ \ai[\tt]{cross} $s_2$ &
163 Cartesian product of $s_1$ and $s_2$
165 $m_3$ := $m_1$ \ai[\tt]{cross} $m_2$ &
166 Cartesian product of $m_1$ and $m_2$
168 $s$ := \ai[\tt]{deltas} $m$ &
169 the set $\{\, y - x \mid x \to y \in m \,\}$
171 $s$ := \ai[\tt]{dom} $m$ &
172 domain of map $m$
174 $s$ := \ai[\tt]{dom} $q$ &
175 domain of piecewise quasipolynomial $q$
177 $s$ := \ai[\tt]{dom} $f$ &
178 domain of piecewise quasipolynomial fold $f$
180 $s$ := \ai[\tt]{ran} $m$ &
181 range of map $m$
183 $s_2$ := \ai[\tt]{lexmin} $s_1$ &
184 lexicographically minimal element of $s_1$
186 $m_2$ := \ai[\tt]{lexmin} $m_1$ &
187 lexicographically minimal image element
189 $s_2$ := \ai[\tt]{lexmax} $s_1$ &
190 lexicographically maximal element of $s_1$
192 $m_2$ := \ai[\tt]{lexmax} $m_1$ &
193 lexicographically maximal image element
195 $o$ := \ai[\tt]{read} {\tt "}{\it filename}{\tt"} &
196 read object from file
198 $s_2$ := \ai[\tt]{sample} $s_1$ &
199 a sample element of the set $s_1$
201 $m_2$ := \ai[\tt]{sample} $m_1$ &
202 a sample element of the map $m_1$
204 \ai[\tt]{source} {\tt "}{\it filename}{\tt"} &
205 read commands from file
207 $q_2$ := \ai[\tt]{sum} $q_1$ &
208 sum $q_1$ over all integer points in the domain of $q_1$,
209 or, if the domain of $q_1$ wraps a map, over all integer
210 points in the range of the wrapped map.
212 $l$ := \ai[\tt]{ub} $q$ &
213 compute an
214 upper bound on the piecewise quasipolynomial $q$ over
215 all integer points in the domain of $q$
216 and return a list containing the upper bound
217 and a boolean that is true if the upper bound
218 is known to be tight.
219 If the domain of $q$ wraps a map, then the upper
220 bound is computed over all integer points in
221 the range of the wrapped map instead.
223 $l$ := \ai[\tt]{vertices} $s$ &
224 a list of vertices of the rational polytope defined by the same constraints
225 as $s$
227 $s$ := \ai[\tt]{wrap} $m$ &
228 wrap the map in a set
230 $m$ := \ai[\tt]{unwrap} $s$ &
231 unwrap the map from the set
233 $s_3$ := $s_1$ \ai{$+$} $s_2$ & union
235 $m_3$ := $m_1$ \ai{$+$} $m_2$ & union
237 $q_3$ := $q_1$ \ai{$+$} $q_2$ & sum
239 $f_2$ := $f_1$ \ai{$+$} $q$ & sum
241 $f_2$ := $q$ \ai{$+$} $f_1$ & sum
243 $S_3$ := $S_1$ \ai{$+$} $S_2$ & concatenation
245 $S_2$ := $o$ \ai{$+$} $S_1$ &
246 concatenation of stringification of $o$ and $S_1$
248 $S_2$ := $S_1$ \ai{$+$} $o$ &
249 concatenation of $S_1$ and stringification of $o$
251 $s_3$ := $s_1$ \ai{$-$} $s_2$ & set difference
253 $m_3$ := $m_1$ \ai{$-$} $m_2$ & set difference
255 $q_3$ := $q_1$ \ai{$-$} $q_2$ & difference
257 $s_3$ := $s_1$ \ai{$*$} $s_2$ & intersection
259 $m_3$ := $m_1$ \ai{$*$} $m_2$ & intersection
261 $q_3$ := $q_1$ \ai{$*$} $q_2$ & product
263 $m_2$ := $m_1$ \ai{$*$} $s$ & intersect domain of $m_1$ with $s$
265 $q_2$ := $q_1$ \ai{$*$} $s$ & intersect domain of $q_1$ with $s$
267 $f_2$ := $f_1$ \ai{$*$} $s$ & intersect domain of $f_1$ with $s$
269 $s_2$ := $m$($s_1$) & apply map $m$ to set $s_1$
271 $m_3$ := $m_1$ \ai[\tt]{.} $m_2$ & join of $m_1$ and $m_2$
273 $m_3$ := $m_2$($m_1)$ & join of $m_1$ and $m_2$
275 $f_3$ := $f_1$ \ai[\tt]{.} $f_2$ & join of $f_1$ and $f_2$, combining
276 the lists of quasipolynomials over shared domains
278 $q_2$ := $m$ \ai[\tt]{.} $q_1$ & join of $m$ and $q_1$, taking the sum
279 over all elements in the intersection of the range of $m$ and the domain
280 of $q_1$
282 $f_2$ := $m$ \ai[\tt]{.} $f_1$ & join of $m$ and $f_1$, computing a bound
283 over all elements in the intersection of the range of $m$ and the domain
284 of $f_1$
286 $m$ := $s_1$ \ai[\tt]{->} $s_2$ & universal map with domain $s_1$
287 and range $s_2$
289 $q_2$ := $q_1$ \ai{@} $s$ &
290 evaluate the piecewise quasipolynomial $q_1$ in each element
291 of the set $s$ and return a piecewise quasipolynomial
292 mapping each of the individual elements to the resulting
293 constant
295 $q$ := $f$ \ai{@} $s$ &
296 evaluate the piecewise quasipolynomial fold $f$ in each element
297 of the set $s$ and return a piecewise quasipolynomial
298 mapping each of the individual elements to the resulting
299 constant
301 $s_3$ := $s_1$ \ai[\tt]{\%} $s_2$ &
302 simplify $s_1$ in the context of $s_2$, i.e., compute
303 the gist of $s_1$ given $s_2$
305 $m_3$ := $m_1$ \ai[\tt]{\%} $m_2$ &
306 simplify $m_1$ in the context of $m_2$, i.e., compute
307 the gist of $m_1$ given $m_2$
309 $q_2$ := $q_1$ \ai[\tt]{\%} $s$ &
310 simplify $q_1$ in the context of the domain $s$, i.e., compute
311 the gist of $q_1$ given $s$
313 $f_2$ := $f_1$ \ai[\tt]{\%} $s$ &
314 simplify $f_1$ in the context of the domain $s$, i.e., compute
315 the gist of $f_1$ given $s$
317 $m_2$ := $m_1$\ai[\tt]{\^{}-1} & inverse of $m_1$
319 $l$ := $m$\ai[\tt]{\^{}+} &
320 compute an overapproximation of the transitive closure
321 of $m$ and return a list containing the overapproximation
322 and a boolean that is true if the overapproximation
323 is known to be exact
325 $o$ := $l$[$i$] &
326 the element at position $i$ in the list $l$
328 $b$ := $s_1$ \ai[\tt]{=} $s_2$ & is $s_1$ equal to $s_2$?
330 $b$ := $m_1$ \ai[\tt]{=} $m_2$ & is $m_1$ equal to $m_2$?
332 $b$ := $s_1$ \ai[\tt]{<=} $s_2$ & is $s_1$ a subset of $s_2$?
334 $b$ := $m_1$ \ai[\tt]{<=} $m_2$ & is $m_1$ a subset of $m_2$?
336 $b$ := $s_1$ \ai[\tt]{<} $s_2$ & is $s_1$ a proper subset of $s_2$?
338 $b$ := $m_1$ \ai[\tt]{<} $m_2$ & is $m_1$ a proper subset of $m_2$?
340 $b$ := $s_1$ \ai[\tt]{>=} $s_2$ & is $s_1$ a superset of $s_2$?
342 $b$ := $m_1$ \ai[\tt]{>=} $m_2$ & is $m_1$ a superset of $m_2$?
344 $b$ := $s_1$ \ai[\tt]{>} $s_2$ & is $s_1$ a proper superset of $s_2$?
346 $b$ := $m_1$ \ai[\tt]{>} $m_2$ & is $m_1$ a proper superset of $m_2$?
348 $m$ := $s_1$ \ai[\tt]{<<} $s_2$ & a map from
349 $s_1$ to $s_2$ of those elements that live in the same space and
350 such that the elements of $s_1$ are lexicographically strictly smaller
351 than those of $s_2$.
353 $m_3$ := $m_1$ \ai[\tt]{<<} $m_2$ & a map from the domain of
354 $m_1$ to the domain of $m_2$ of those elements such that their images
355 live in the same space and such that the images of the elements of
356 $m_1$ are lexicographically strictly smaller than those of $m_2$.
358 $m$ := $s_1$ \ai[\tt]{<<=} $s_2$ & a map from
359 $s_1$ to $s_2$ of those elements that live in the same space and
360 such that the elements of $s_1$ are lexicographically smaller
361 than those of $s_2$.
363 $m_3$ := $m_1$ \ai[\tt]{<<=} $m_2$ & a map from the domain of
364 $m_1$ to the domain of $m_2$ of those elements such that their images
365 live in the same space and such that the images of the elements of
366 $m_1$ are lexicographically smaller than those of $m_2$.
368 $m$ := $s_1$ \ai[\tt]{>>} $s_2$ & a map from
369 $s_1$ to $s_2$ of those elements that live in the same space and
370 such that the elements of $s_1$ are lexicographically strictly greater
371 than those of $s_2$.
373 $m_3$ := $m_1$ \ai[\tt]{>>} $m_2$ & a map from the domain of
374 $m_1$ to the domain of $m_2$ of those elements such that their images
375 live in the same space and such that the images of the elements of
376 $m_1$ are lexicographically strictly greater than those of $m_2$.
378 $m$ := $s_1$ \ai[\tt]{>>=} $s_2$ & a map from
379 $s_1$ to $s_2$ of those elements that live in the same space and
380 such that the elements of $s_1$ are lexicographically greater
381 than those of $s_2$.
383 $m_3$ := $m_1$ \ai[\tt]{>>=} $m_2$ & a map from the domain of
384 $m_1$ to the domain of $m_2$ of those elements such that their images
385 live in the same space and such that the images of the elements of
386 $m_1$ are lexicographically greater than those of $m_2$.
388 \end{supertabular}