1 \section{\protect\isl/ interface
}
9 The
\barvinok/ library currently supports only a few
10 functions that interface with the
\isl/ library.
11 In time, this interface will grow and is set to replace
12 the
\PolyLib/ interface.
13 For more information on the
\isl/ data structures, see
14 the
\isl/ user manual.
17 __isl_give isl_pw_qpolynomial *isl_basic_set_card(
18 __isl_take isl_basic_set *bset);
19 __isl_give isl_pw_qpolynomial *isl_set_card(__isl_take isl_set *set);
20 __isl_give isl_union_pw_qpolynomial *isl_union_set_card(
21 __isl_take isl_union_set *uset);
23 Compute the number of elements in an
\ai[\tt]{isl
\_basic\_set},
24 \ai[\tt]{isl
\_set} or
\ai[\tt]{isl
\_union\_set}.
25 The resulting
\ai[\tt]{isl
\_pw\_qpolynomial}
26 or
\ai[\tt]{isl
\_union\_pw\_qpolynomial} has purely parametric cells.
29 __isl_give isl_pw_qpolynomial *isl_basic_map_card(
30 __isl_take isl_basic_map *bmap);
31 __isl_give isl_pw_qpolynomial *isl_map_card(__isl_take isl_map *map);
32 __isl_give isl_union_pw_qpolynomial *isl_union_map_card(
33 __isl_take isl_union_map *umap);
35 Compute a closed form expression for the number of image elements
36 associated to any element in the domain of the given
\ai[\tt]{isl
\_basic\_map},
37 \ai[\tt]{isl
\_map} or
\ai[\tt]{isl
\_union\_map}.
38 The union of the cells in the resulting
\ai[\tt]{isl
\_pw\_qpolynomial}
39 is equal to the domain of the input
\ai[\tt]{isl
\_map}.
42 __isl_give isl_pw_qpolynomial *isl_pw_qpolynomial_sum(
43 __isl_take isl_pw_qpolynomial *pwqp);
44 __isl_give isl_union_pw_qpolynomial *isl_union_pw_qpolynomial_sum(
45 __isl_take isl_union_pw_qpolynomial *upwqp);
47 Compute the sum of the given piecewise quasipolynomial over
48 all integer points in the domain. The result is a piecewise
49 quasipolynomial that only involves the parameters.
50 If, however, the domain of the piecewise quasipolynomial wraps
51 a relation, then the sum is computed over all integer points
52 in the range of that relation and the domain of the relation
53 becomes the domain of the result.
56 __isl_give isl_pw_qpolynomial *isl_set_apply_pw_qpolynomial(
57 __isl_take isl_set *set, __isl_take isl_pw_qpolynomial *pwqp);
58 __isl_give isl_union_pw_qpolynomial *isl_union_set_apply_union_pw_qpolynomial(
59 __isl_take isl_union_set *uset,
60 __isl_take isl_union_pw_qpolynomial *upwqp);
62 Compute the sum of the given piecewise quasipolynomial over
63 all integer points in the intersection of the domain and the given set.
66 __isl_give isl_pw_qpolynomial *isl_map_apply_pw_qpolynomial(
67 __isl_take isl_map *map, __isl_take isl_pw_qpolynomial *pwqp);
68 __isl_give isl_union_pw_qpolynomial *isl_union_map_apply_union_pw_qpolynomial(
69 __isl_take isl_union_map *umap,
70 __isl_take isl_union_pw_qpolynomial *upwqp);
72 Compose the given map with the given piecewise quasipolynomial.
73 That is, compute the sum over all elements in the intersection
74 of the range of the map and the domain of the piecewise quasipolynomial
75 as a function of an element in the domain of the map.
77 \subsection{Calculator
}
79 The
\ai[\tt]{iscc
} calculator offers an interface to some
80 of the functionality provided by the
\isl/,
\cloog/ and
\barvinok/
82 The language used by
\ai[\tt]{iscc
} is extremely simple. The calculator
83 supports operations on constants and dynamically typed variables and
84 assignments (
\ai[\tt]{:=
}) to those variables. If the result of an expression
85 is not used inside another expression and not assigned to a variable,
86 then this result is printed on the screen. The operators are overloaded
87 based on the types of the arguments, which may be sets, relations,
88 piecewise quasipolynomials, piecewise quasipolynomial folds, lists,
90 The supported operations are shown in
\autoref{t:iscc
}.
91 Note that when an operation requires an argument of a certain
92 type, a binary list with the first element of the required type
93 may also be used instead.
95 \subsubsection{Sets and Iteration Domains
}
98 \begin{lstlisting
}[escapechar=@
]{}
99 for (i =
1; i <= n; ++i)
100 for (j =
1; j <= i; ++j)
103 \caption{A loop nest
}
108 \begin{tikzpicture
}[>=stealth,x=
0.7cm,y=-
0.7cm
]
109 \draw[thick
] (
1,
1)--(
5,
5)--(
1,
5)--(
1,
1);
110 \draw[->
] (-
0.6,
0) to (
5.6,
0) node
[anchor=south east
] {$j$
};
111 \draw[->
] (
0,-
0.6) to (
0,
5.6) node
[anchor=south east
] {$i$
};
112 \draw[help lines,step=
0.7cm
] (-
0.6,
5.6) grid (
5.6,-
0.6);
113 \foreach \i in
{1,...,
5}{
114 \foreach \j in
{1,...,
\i}{
115 \fill (
\j,
\i) circle (
2pt);
119 \caption{The iteration domain of the loop nest in
\autoref{f:loop nest
}}
120 \label{f:iteration domain
}
123 Within the polyhedral model for analysis and transformation of
124 static affine programs, the most basic kind of set is the
125 \defindex{iteration domain
}.
126 The iteration domain represents the iterations of a statement in a loop nest.
127 Take, for example, the loop nest in
\autoref{f:loop nest
}
128 and assume first that
\lstinline{n
} has a fixed value, say
5.
129 The pairs of values of
\lstinline{i
} and
\lstinline{j
} for
130 which statement
\lstinline{S
} is executed are shown graphically
131 in
\autoref{f:iteration domain
}.
132 Mathematically, this set of pairs can be represented as
135 (i,j)
\in \ZZ^
2 \mid 1 \le i
\le 5 \wedge 1 \le j
\le i
138 and the
\isl/ notation is very similar:
139 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
140 { [i,j
] :
1 <= i <=
5 and
1 <= j <= i
}
143 the coordinates are separated by commas and enclosed in square
144 brackets. This description of the space in which the set lives
145 is followed by a colon and the constraints on the coordinates.
146 Assuming the iterators are incremented by one in every iterations
147 of the loop, a lower and upper bound on each loop iterator
148 can be read off from the initialization and the test.
149 Note that in an
\iscc/ set,
150 the coordinates are assumed to be integer by default.
151 For an iteration domain to be representable by such a set,
152 the iterators therefore need to be integers.
154 The constraints of a set need to be affine, i.e., linear plus constant term.
155 These affine constraint may be combined through conjunctions (
\texttt{and
}),
156 disjunctions (
\texttt{or
}), projections (
\texttt{exists
}) and
157 negations (
\texttt{not
}).
158 Note that the formula is immediately converted
159 into
\indac{DNF
}, so it may sometimes be more efficient
160 to construct a set from smaller sets by applying
161 basic operations such as intersection (
{\tt *
}),
162 union (
{\tt +
}) and difference (
{\tt -
}).
163 For example, the following square with its diagonal removed,
166 (i,j)
\mid 0 \le i,j
\le 10 \wedge \lnot (i = j)
169 can be constructed as
170 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
171 { [i,j
] :
0 <= i,j <=
10 } -
{ [i,i
] }
174 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
175 { [i,j
] :
0 <= i,j <=
10 and not (i = j)
}
177 Note that an occurrence of a relational operator in a set description
178 may define several constraints, one for each pair of arguments.
179 The elements in a list of arguments are separated by a comma.
180 If there are no constraints on the coordinates, i.e., in case of
181 a universe set, the colon may be omitted as well.
183 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
186 represents the entire (unnamed) zero-dimensional space,
187 and should not be confused with
188 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
191 which represents the empty set.
193 Returning to the iteration domain of the loop nest
194 in
\autoref{f:loop nest
}, we usually do not want to analyze
195 such a program for a specific value of
\lstinline{n
},
196 but instead for all possible values of
\lstinline{n
} at once.
197 A generic description of the iteration domain can be obtained
198 through the introduction of a (free) parameter, as in
199 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
200 [n
] ->
{ [i,j
] :
1 <= i <= n and
1 <= j <= i
}
202 The optional parameters should
203 be declared by placing them in a comma delimited list inside
\lstinline!
[]!
204 (followed by an ``
\lstinline!->!'') in front of the main set description.
205 The parameters are global and are identified by their names,
206 so the order inside the list is arbitrary.
207 This should be contrasted to the coordinates of a space, the names of
208 which are only relevant within the description of the set and which
209 are instead identified by their positions.
211 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
212 [n
] ->
{ [i,j
] :
1 <= i <= n and
1 <= j <= i
}
215 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
216 [n
] ->
{ [a,b
] :
1 <= a <= n and
1 <= b <= a
}
218 but it is not equal to
219 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
220 [n
] ->
{ [j,i
] :
1 <= i <= n and
1 <= j <= i
}
222 (because the order of the coordinates has changed)
224 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
225 [m
] ->
{ [i,j
] :
1 <= i <= m and
1 <= j <= i
}
227 (because it involves a different parameter).
229 To plug in a particular value for a parameter, the user should
230 take the
\ai{intersection
} (
\ai[\tt]{*
}) with a (typically universal) set that
231 assigns a particular value to the parameter.
233 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
234 S :=
[n
] ->
{ [i,j
] :
1 <= i <= n and
1 <= j <= i
};
235 S *
[n
] ->
{ [i,j
] : n =
5 };
237 It should be noted, though, that the result is not the same
238 as simply replacing
\lstinline{n
} by
5 as the result of the above
239 sequence will still have the global parameter
\lstinline{n
} set to
5.
240 To avoid this assignment, the user should instead compute
241 the
\ai{gist
} (
\ai[\tt]{\%
}) of the original set in the context
242 of setting
\lstinline{n
} to
5.
243 That is, the result of the sequence below is
\lstinline{True
}.
244 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
245 S1 :=
{ [i,j
] :
1 <= i <=
5 and
1 <= j <= i
};
246 S2 :=
[n
] ->
{ [i,j
] :
1 <= i <= n and
1 <= j <= i
};
247 (S2
% [n] -> { [i,j] : n = 5}) = S1;
251 \begin{lstlisting
}[escapechar=@
]{}
252 for (i =
1; i <= n; i +=
3)
255 \caption{A loop with non-unit stride
}
259 If a loop has a non-unit stride as in
\autoref{f:stride
}
260 then affine constraints on the coordinates and the parameters
261 are not sufficient to represent the iteration domain.
262 What is needed is a way to express that the value of
263 \lstinline{i
} is equal to
1 plus
3 times some integer and
264 this is where existentially quantified variables can be used.
265 Existentially quantified variables are introduced by the
266 \ai[\tt]{exists
} keyword and followed by a colon.
267 They can only be used within a single disjunct.
268 As an example, the iteration domain of the loop in
\autoref{f:stride
}
269 can be represented as
270 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
271 [n
] ->
{ [i
] : exists a :
1 <= i <= n and i =
1 +
3 a
}
275 \begin{lstlisting
}[escapechar=@
]{}
276 for (i =
1; i <= n; ++i)
277 if ((i +
1)
% 5 <= 2)
280 \caption{A loop with a modulo condition
}
284 Existentially quantified variables are also useful to represent
285 modulo constraints. Consider for example the loop in
286 \autoref{f:modulo
}. The iterator values
\lstinline!i! for which
287 the statement
\lstinline!S! is executed lie between
288 1 and
\lstinline!n! and are such that the remainder of
289 \lstinline!i +
1! on division by
5 is less than or equal to
2.
290 The constraint $(i +
1)
\bmod 5 \le 2$ can be written
291 as $(i +
1) -
5 \floor{\frac{i+
1}5} \le 2$, where
292 $f =
\floor{\frac{i+
1}5}$ is the greatest integer part of $
\frac{i+
1}5$.
293 That is, $f$ is the unique integer value satisfying the constraints
294 $
5 f
\le i +
1$ and $
5 f
\ge (i+
1) -
4$.
295 The iteration domain of the statement in
\autoref{f:modulo
}
296 can therefore be represented as
297 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
298 [n
] ->
{ [i
] : exists f :
1 <= i <= n and (i +
1) -
5 f <=
2 and
299 (i +
1) -
4 <=
5 f <= i +
1 }
301 Since greatest integer parts occur relatively frequently, there is
302 a special notation for them in
\isl/ using
\lstinline!
[]!.
303 The above set can therefore also be represented as
304 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
305 [n
] ->
{ [i
] :
1 <= i <= n and (i +
1) -
5 *
[(i +
1)/
5] <=
2 }
307 Actually, since modulos are pretty common too,
\isl/ also has
308 a special notation for them and the set can therefore also be respresented as
309 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
310 [n
] ->
{ [i
] :
1 <= i <= n and (i +
1)
% 5 <= 2 }
312 It should be noted that
\lstinline!
[]! always rounds down
313 (towards $-
\infty$), while integer division in C truncates
314 (towards
0). When translating conditions in C containing integer
315 divisions and/or modulos to
\isl/ constraints, the user should therefore
316 make sure the sign of the dividend is positive. If not, the integer
317 division needs to be translated differently for positive and negative
321 \begin{lstlisting
}[escapechar=@
]{}
322 for (i =
0; i < n; ++i)
324 for (i =
0; i < n; ++i)
325 for (j =
0; j < n - i; ++j)
326 F: t
[j
] = f(t
[j
], t
[j+
1]);
327 for (i =
0; i < n; ++i)
330 \caption{A program with three loop nests
}
331 \label{f:three loops
}
334 Most programs involve more than one statement.
335 Although it is possible to work with different sets, each
336 representing the iteration domain of a statement,
337 it is usually more convenient to collect all iteration domains
338 in a single set. To be able to differentiate between iterations
339 of different statements with the same values for the iterators,
340 \isl/ allows spaces to be named. The name is placed in front
341 of the
\lstinline!
[]! enclosing the iterators.
342 Consider for example the program in
\autoref{f:three loops
}.
343 The program contains three statements which have been labeled
345 The iteration domain of the first statement (
\lstinline!T!)
346 can be represented as
347 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
348 [n
] ->
{ T
[i
] :
0 <= i < n
}
350 The union of all iteration domains can be represented as
351 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
354 F
[i,j
] :
0 <= i < n and
0 <= j < n - i;
358 The semicolon
\lstinline{;
} is used to express a disjunction
359 between spaces. This should be contrasted with the
\lstinline{or
}
360 keyword which expresses a disjunction between conjunctions of constraints.
361 For example, the result of the following
\iscc/ statement is
363 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
364 { [i
] : i =
3 or i =
5 } =
{ [3];
[5] };
367 \subsubsection{Maps and Access Relations
}
369 A second important concept in the polyhedral model is that
370 of an
\defindex{access relation
}.
371 An access relation connects iterations of a statement
372 to the array elements accessed by those iterations.
373 Such a binary relation can be represented by a map in
\isl/.
374 Maps are defined in similar way to sets,
375 except that the single space is replaced by a pair of spaces separated
377 As an example, consider once more the program in
\autoref{f:three loops
}.
378 In particular, consider the access
\lstinline{t
[j+
1]} in
379 statement
\lstinline{F
}.
380 The index expression maps the pair of iterations
\lstinline{i
}
381 and
\lstinline{j
} to
\lstinline{t
[j+
1]}, i.e., element
\lstinline{j+
1}
382 of a space with name
\lstinline{t
}.
383 Ignoring the loop bound constraints, this access relation can
385 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
386 { F
[i,j
] -> t
[j +
1] }
388 It is however customary to include the constraints on the iterators
389 in the access relation, resulting in
390 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
391 [n
] ->
{ F
[i,j
] -> t
[j +
1] :
0 <= i < n and
0 <= j < n - i
}
393 The constraints can be added by intersecting the domains
394 of the access relations with the iteration domains.
395 For example, the following sequence constructs the access
396 relation for all reads in the program.
397 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
400 F
[i,j
] :
0 <= i < n and
0 <= j < n - i;
411 In this sequence, the
\lstinline{*
} operator, when applied
412 to a map and a set, intersects the domain of the map with the set.
414 The notation
\lstinline{R(S)
} can be used to compute the image
415 of the set
\lstinline{S
} under the map
\lstinline{R
}.
416 For example, given the sequence above,
\lstinline!Read(
{F
[0,
1]})!
417 computes the array elements read in iteration $(
0,
1)$ of statement
418 \lstinline{F
} and is equal to
419 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
420 [n
] ->
{ t
[2] : n >=
2; t
[1] : n >=
2 }
422 That is, elements
1 and
2 of the
\lstinline{t
} array are read,
423 provided
\lstinline{n
} is at least
2.
425 Maps need not be single-valued.
426 As an example, assume that
\lstinline{A
} is a two-dimensional
427 array of size
\lstinline{n
} in both dimensions.
428 Iterations
\lstinline{i
} of
429 a statement
\lstinline{S
} may pass a pointer to an entire row
430 of
\lstinline{A
} to a function as in
\lstinline{f(A
[i
])
}.
431 Without knowing anything about
\lstinline{f
}, we would have
432 to assume that this function may access any element of the row.
433 The access relation corresponding to
\lstinline{A
[i
]} is therefore
434 \begin{lstlisting
}[columns=flexible,escapechar=@,language=
]{}
435 [n
] ->
{ S
[i
] -> A
[i,j
] :
0 <= i,j < n
}
437 This map associates
\lstinline{n
} elements of
\lstinline{A
}
438 to each iteration of
\lstinline{S
}.
440 \subsubsection{Nested Spaces
}
442 Each space may contain a nested pair of spaces. Such nested spaces
443 are extremely useful in more advanced applications.
444 As an example, suppose that during equivalence checking
445 \shortcite{Verdoolaege2009equivalence
}
446 of two programs the iterations of
\verb!S1! in one program are supposed to
447 produce the same results as the same iterations of
\verb!SA! in the other program,
448 which may be described using the following map
450 [n
] ->
{ S1
[i
] -> SA
[i
] :
0 <= i <= n
}
452 If the iterations of
\verb!S1! depend on the same iterations
453 of
\verb!S2!, i.e.,
\verb!
{S1
[i
]->S2
[i
]}!, while those of
\verb!SA!
454 depend on the next iteration of
\verb!B!, i.e.,
\verb!
{SA
[i
]->SB
[i+
1]}!,
455 then we can apply the cross product of these two dependence maps, i.e.,
457 { [S1
[i
] -> SA
[i'
]] ->
[S2
[i
] -> SB
[1+i'
]] }
459 to the original map to find
460 out which iterations of
\verb!S2! should correspond to which
461 iterations of
\verb!SB!.
463 \subsubsection{Basic Operations
}
465 Basic operations on sets and maps include intersection (
\ai[\tt]{*
}),
466 union (
\ai[\tt]{+
}), difference (
\ai[\tt]{-
}), cross product (
\ai[\tt]{cross
}),
467 sampling (
\ai[\tt]{sample
}), affine hull (
\ai[\tt]{aff
}),
468 lexicographic optimization (
\ai[\tt]{lexmin
} or
\ai[\tt]{lexmax
}),
469 subset (
\ai[\tt]{<=
}) and equality (
\ai[\tt]{=
}) tests,
470 code generation (
\ai[\tt]{codegen
})
471 and the cardinality (
\ai[\tt]{card
}).
472 Additional operations on maps include computing domain (
\ai[\tt]{dom
})
473 and range (
\ai[\tt]{ran
}), differences between image and domain (
\ai[\tt]{deltas
}),
474 join (
\ai[\tt]{.
}), inverse (
\ai[\tt]{\^
{}-
1}) and transitive closure (
\ai[\tt]{\^
{}+
}).
475 The latter may result in an overapproximation.
477 The
\ai[\tt]{card
} operation computes the number of elements in a set
478 or the number of elements in the image of a domain element of a map.
479 The operation is performed exactly and completely symbolically and
480 the result is a piecewise quasipolynomial, i.e., a subdivision of one
481 or more spaces, with a quasipolynomial associated to each cell in the subdivision.
482 As a trivial example, the result of
484 card
{ A
[i
] -> B
[j
] :
0 <= j <= i
}
486 is
\verb!
{ A
[i
] -> (
1+i) : i >=
0 }!.
487 Operations on piecewise quasipolynomials include sum (
\ai[\tt]{+
})
488 and difference (
\ai[\tt]{-
}) and the computation of an upper bound over the domain.
489 If the domain contains a pair of nested spaces, then the upper bound is computed over
490 the nested range. As another trivial example, the result of
492 ub
{ [[i
] ->
[j
]] -> j^
2 : -i <= j <= i
}
495 \verb!(
{ [i
] -> max(i^
2) : i >=
0 }, True)!.
496 The first element in this list is the actual bound in the form
497 of a piecewise quasipolynomial fold,
498 i.e., a maximum of quasipolynomials defined over cells.
499 The second indicates whether the bound is tight, i.e., whether
500 a maximum has been computed.
502 \subsubsection{Advanced Operations
}
504 While the basic
{\tt card
} operation simply counts the number of elements
505 in an affine set, it is also possible to assign a weight to each element
506 of the set and to compute the sum of those weights over all the points in the set.
507 The syntax for this weighted counting is to compute the
{\tt sum
} of
508 a piecewise quasipolynomial over its domain. As in the case of the
{\tt ub
}
509 operator, if the domain contains a pair of nested space, the sum is computed
510 over the range. As an example, the result
513 sum
{ [[i
] ->
[j
]] -> i*j :
0 <= j <= i
}
516 \verb|
{ [i
] -> (
1/
2*i^
2+
1/
2*i^
3) : i >=
0 }|.
518 After the computation of some sum or bound, the result may have to
519 be reformulated in terms of other variables. For example, during
520 inter procedural analysis, a result computed in terms of the formal
521 parameters may have to be reformulated in terms of the actual parameters.
522 {\tt iscc
} therefore allows maps and
523 piecewise quasipolynomials or folds to be composed.
524 If the map is multi-valued, then the composition maps each domain element
525 to the sum or upper bound of the values at its image elements.
527 Finally, because of its high-level representation,
{\tt iscc
} can
528 provide a dependence analysis operation taking only three maps as input,
529 the sink accesses, the potential source accesses and a schedule.
530 The result is a single dependence map.
533 \subsubsection{More Examples
}
535 P :=
[n, m
] ->
{ [i,j
] :
0 <= i <= n and i <= j <= m
};
538 f :=
[n,m
] ->
{ [i,j
] -> i*j + n*i*i*j : i,j >=
0 and
5i +
27j <= n+m
};
541 s @
[n,m
] ->
{ [] :
0 <= n,m <=
20 };
543 f :=
[n
] ->
{ [i
] ->
2*n*i - n*n +
3*n -
1/
2*i*i -
3/
2*i-
1 :
544 (exists j :
0 <= i <
4*n-
1 and
0 <= j < n and
545 2*n-
1 <= i+j <=
4*n-
2 and i <=
2*n-
1 )
};
548 u @
[n
] ->
{ [] :
0 <= n <=
10 };
550 m :=
[n
] ->
{ [i,j
] ->
[i+
1,j+
1] :
1 <= i,j < n;
551 [i,j
] ->
[i+
1,j-
1] :
1 <= i < n and
2 <= j <= n
};
555 codegen
[N
] ->
{ A
[i
] ->
[i,
0] :
0 <= i <= N; B
[i
] ->
[i,
1] :
1 <= i <= N
};
557 { [k
] ->
[i
] :
1 <= i <= k
} .
{ [n
] ->
2 * n : n >=
1 };
559 { [m
] ->
[c
] :
1 <= c <= m
} .
{ [k
] -> max((
3 * k + k^
2)) : k >=
1 };
562 \subsubsection{Comparison to other Interactive Polyhedral Tools
}
564 Two related interactive polyhedral tools are
565 the Omega calculator
\shortcite{Omega_calc
}
566 and
{\tt SPPoC
} \shortcite{Boulet2001SPPoC
}.
567 The syntax of
{\tt iscc
} was very much inspired
568 by that of the Omega calculator. However, the Omega
569 calculator only knows sets and maps. In particular,
570 it does not perform any form of counting. An earlier version
571 of
\barvinok/ came with a modified version of
572 the Omega calculator that introduced an operation
573 for counting the number of elements in a set, but it
574 would simply print the result and not allow any further
576 {\tt SPPoC
} does support counting, but only the basic
577 operation of counting the elements in a set.
578 In particular, it does not support weighted counting,
579 nor the computation of upper bounds.
580 It also only supports (single-valued) functions
581 and not generic relations like the Omega calculator and
{\tt iscc
}.
582 Internally,
{\tt SPPoC
} uses
{\tt PolyLib
},
{\tt PipLib
} and
{\tt omega
}
584 its operations. Although the first two of these libraries may have been
585 state-of-the-art at the time
{\tt SPPoC
} was created, they are
586 no longer actively maintained and have been largely
587 superseded by more recent libraries.
588 In particular,
{\tt PipLib
} effectively only supports a single
589 operation, which is now also available in both
{\tt isl
} and
{\tt PPL
}.
590 The operations on rational polyhedra in
{\tt PolyLib
} are also
591 available in
{\tt PPL
}, usually through a cleaner interface and
592 with a more efficient implementation. As to counting the elements
593 in a parametric polytope, Barvinok's algorithm,
594 implemented in the
{\tt barvinok
} library, is usually much faster
595 than the algorithm implemented in
{\tt PolyLib
}
596 \shortcite{Verdoolaege2007parametric
}.
598 the ability to work with named and nested spaces and the ability
599 of sets and maps to contain (pairs of) elements from different spaces
600 are not available in the Omega calculator and
{\tt SPPoC
}.
603 \tablecaption{{\tt iscc
} operations. The variables
604 have the following types,
607 $q$: piecewise quasipolynomial,
608 $f$: piecewise quasipolynomial fold,
613 $o$: object of any type
623 \multicolumn{2}{r
}{\small\sl continued on next page
}
627 \begin{supertabular
}{p
{0.35\textwidth}p
{0.6\textwidth}}
628 $s_2$ :=
\ai[\tt]{aff
} $s_1$ & affine hull of $s_1$
630 $m_2$ :=
\ai[\tt]{aff
} $m_1$ & affine hull of $m_1$
632 $q$ :=
\ai[\tt]{card
} $s$ &
633 number of elements in the set $s$
635 $q$ :=
\ai[\tt]{card
} $m$ &
636 number of elements in the image of a domain element
638 $s_2$ :=
\ai[\tt]{coalesce
} $s_1$ &
639 simplify the representation of set $s_1$ by trying
640 to combine pairs of basic sets into a single
643 $m_2$ :=
\ai[\tt]{coalesce
} $m_1$ &
644 simplify the representation of map $m_1$ by trying
645 to combine pairs of basic maps into a single
648 $q_2$ :=
\ai[\tt]{coalesce
} $q_1$ &
649 simplify the representation of $q_1$ by trying
650 to combine pairs of basic sets in the domain
651 of $q_1$ into a single basic set
653 $f_2$ :=
\ai[\tt]{coalesce
} $f_1$ &
654 simplify the representation of $f_1$ by trying
655 to combine pairs of basic sets in the domain
656 of $f_1$ into a single basic set
658 \ai[\tt]{codegen
} $s$ &
659 generate code for the given domain.
660 This operation is only available if
\ai[\tt]{CLooG
}
661 support was compiled in.
663 \ai[\tt]{codegen
} $m$ &
664 generate code for the given scattering function.
665 This operation is only available if
\ai[\tt]{CLooG
}
666 support was compiled in.
668 $s_2$ :=
\ai[\tt]{coefficients
} $s_1$ &
669 The set of coefficients of valid constraints for $s_1$
671 $s_2$ :=
\ai[\tt]{solutions
} $s_1$ &
672 The set of elements satisfying the constraints with coefficients in $s_1$
674 $s_3$ := $s_1$
\ai[\tt]{cross
} $s_2$ &
675 Cartesian product of $s_1$ and $s_2$
677 $m_3$ := $m_1$
\ai[\tt]{cross
} $m_2$ &
678 Cartesian product of $m_1$ and $m_2$
680 $s$ :=
\ai[\tt]{deltas
} $m$ &
681 the set $\
{\, y - x
\mid x
\to y
\in m \,\
}$
683 $m_2$ :=
\ai[\tt]{deltas
\_map} $m_1$ &
684 the map $\
{\, (x
\to y)
\to y - x
\mid x
\to y
\in m_1 \,\
}$
686 $s$ :=
\ai[\tt]{dom
} $m$ &
689 $s$ :=
\ai[\tt]{dom
} $q$ &
690 domain of piecewise quasipolynomial $q$
692 $s$ :=
\ai[\tt]{dom
} $f$ &
693 domain of piecewise quasipolynomial fold $f$
695 $s$ :=
\ai[\tt]{domain
} $m$ &
698 $s$ :=
\ai[\tt]{domain
} $q$ &
699 domain of piecewise quasipolynomial $q$
701 $s$ :=
\ai[\tt]{domain
} $f$ &
702 domain of piecewise quasipolynomial fold $f$
704 $m_2$ :=
\ai[\tt]{domain
\_map} $m_1$ &
705 a map from a wrapped copy of $m_1$ to the domain of $m_1$
707 $s$ :=
\ai[\tt]{ran
} $m$ &
710 $s$ :=
\ai[\tt]{range
} $m$ &
713 $m_2$ :=
\ai[\tt]{range
\_map} $m_1$ &
714 a map from a wrapped copy of $m_1$ to the range of $m_1$
716 $m$ :=
\ai[\tt]{identity
} $s$ &
717 identity relation on $s$
719 $s_2$ :=
\ai[\tt]{lexmin
} $s_1$ &
720 lexicographically minimal element of $s_1$
722 $m_2$ :=
\ai[\tt]{lexmin
} $m_1$ &
723 lexicographically minimal image element
725 $s_2$ :=
\ai[\tt]{lexmax
} $s_1$ &
726 lexicographically maximal element of $s_1$
728 $m_2$ :=
\ai[\tt]{lexmax
} $m_1$ &
729 lexicographically maximal image element
731 $s_2$ :=
\ai[\tt]{lift
} $s_1$ &
732 lift $s_1$ to a space with extra dimensions corresponding
733 to the existentially quantified variables in $s_1$ such
734 that
\lstinline!domain(unwrap(lift S))! is equal to
\lstinline!S!
736 $s_2$ :=
\ai[\tt]{poly
} $s_1$ & polyhedral hull of $s_1$
738 $m_2$ :=
\ai[\tt]{poly
} $m_1$ & polyhedral hull of $m_1$
740 $q_2$ :=
\ai[\tt]{poly
} $q_1$ & polynomial approximation of $q_1$
742 $q_2$ :=
\ai[\tt]{lpoly
} $q_1$ & polynomial underapproximation of $q_1$
744 $q_2$ :=
\ai[\tt]{upoly
} $q_1$ & polynomial overapproximation of $q_1$
746 $l$ :=
\ai[\tt]{pow
} $m$\ &
747 compute an overapproximation of the power
748 of $m$ and return a list containing the overapproximation
749 and a boolean that is true if the overapproximation
752 \ai[\tt]{print
} $o$ &
755 $o$ :=
\ai[\tt]{read
} {\tt "
}{\it filename
}{\tt"
} &
756 read object from file
758 $s_2$ :=
\ai[\tt]{sample
} $s_1$ &
759 a sample element of the set $s_1$
761 $m_2$ :=
\ai[\tt]{sample
} $m_1$ &
762 a sample element of the map $m_1$
764 $s_2$ :=
\ai[\tt]{scan
} $s_1$ &
765 the set $s_1$ split into individual elements,
766 provided $s_1$ contains a finite number of elements
768 $m_2$ :=
\ai[\tt]{scan
} $m_1$ &
769 the map $m_1$ split into individual elements,
770 provided $m_1$ contains a finite number of elements
772 \ai[\tt]{source
} {\tt "
}{\it filename
}{\tt"
} &
773 read commands from file
775 $q_2$ :=
\ai[\tt]{sum
} $q_1$ &
776 sum $q_1$ over all integer points in the domain of $q_1$,
777 or, if the domain of $q_1$ wraps a map, over all integer
778 points in the range of the wrapped map.
780 $S$ :=
\ai[\tt]{typeof
} $o$ &
781 a string representation of the type of $o$
783 $l$ :=
\ai[\tt]{ub
} $q$ &
785 upper bound on the piecewise quasipolynomial $q$ over
786 all integer points in the domain of $q$
787 and return a list containing the upper bound
788 and a boolean that is true if the upper bound
789 is known to be tight.
790 If the domain of $q$ wraps a map, then the upper
791 bound is computed over all integer points in
792 the range of the wrapped map instead.
794 $l$ :=
\ai[\tt]{vertices
} $s$ &
795 a list of vertices of the rational polytope defined by the same constraints
798 $s$ :=
\ai[\tt]{wrap
} $m$ &
799 wrap the map in a set
801 $m$ :=
\ai[\tt]{unwrap
} $s$ &
802 unwrap the map from the set
804 \ai[\tt]{write
} {\tt "
}{\it filename
}{\tt"
} $o$ &
807 $m_2$ :=
\ai[\tt]{zip
} $m_1$ &
808 the cross product of domain and range of $m_1$, i.e.,
809 $\
{\, (
\vec w
\to \vec y)
\to (
\vec x
\to \vec z)
810 \mid (
\vec w
\to \vec x)
\to (
\vec y
\to \vec z)
\in m_1 \,\
}$
812 $m_4$ :=
\ai[\tt]{any
} $m_1$
\ai[\tt]{before
} $m_2$
\ai[\tt]{under
} $m_3$ &
813 compute a map from any element $x$ in the domain of $m_1$
814 to any element $y$ in the domain of $m_2$
815 such that their images $m_1(x)$ and $m_2(y)$ overlap
816 and such that $m_3(x)
\llt m_3(y)$.
818 $l$ :=
\ai[\tt]{last
} $m_1$
\ai[\tt]{before
} $m_2$
\ai[\tt]{under
} $m_3$ &
819 compute a map that contains for any element $y$ in the domain of $m_2$
820 a mapping from the lexicographically last element $x$ in the domain of $m_1$
821 (according to the schedule $m_3$) to $y$
822 such that $m_1(x)$ and $m_2(y)$ overlap and such that $m_3(x)
\llt m_3(y)$.
823 Return a list containing this map and the set of elements in the domain of
824 $m_2$ for which there is no corresponding element in the domain of $m_1$.
826 $m_5$ :=
\ai[\tt]{any
} $m_1$
\ai[\tt]{last
} $m_2$
\ai[\tt]{before
} $m_3$
827 \ai[\tt]{under
} $m_4$ &
828 compute a map that contains for any element $y$ in the domain of $m_3$
829 a mapping from the lexicographically last element $x$ in the domain of $m_2$
830 (according to the schedule $m_4$) to $y$
831 such that $m_2(x)$ and $m_3(y)$ overlap and such that $m_4(x)
\llt m_4(y)$
832 as well as from any element $z$ in the domain of $m_1$ such that
833 $m_1(z)$ and $m_3(y)$ overlap, $m_4(z)
\llt m_4(y)$ and such that there
834 is no $x$ in the domain of $m_2$ with
835 $m_2(x)
\cap m_3(y)
\ne \emptyset$ and $m_4(z)
\llt m_4(x)
\llt m_4(y)$.
837 $i_3$ := $i_1$
\ai{$+$
} $i_2$ & sum
839 $s_3$ := $s_1$
\ai{$+$
} $s_2$ & union
841 $m_3$ := $m_1$
\ai{$+$
} $m_2$ & union
843 $q_3$ := $q_1$
\ai{$+$
} $q_2$ & sum
845 $f_2$ := $f_1$
\ai{$+$
} $q$ & sum
847 $f_2$ := $q$
\ai{$+$
} $f_1$ & sum
849 $S_3$ := $S_1$
\ai{$+$
} $S_2$ & concatenation
851 $S_2$ := $o$
\ai{$+$
} $S_1$ &
852 concatenation of stringification of $o$ and $S_1$
854 $S_2$ := $S_1$
\ai{$+$
} $o$ &
855 concatenation of $S_1$ and stringification of $o$
857 $i_3$ := $i_1$
\ai{$-$
} $i_2$ & difference
859 $s_3$ := $s_1$
\ai{$-$
} $s_2$ & set difference
861 $m_3$ := $m_1$
\ai{$-$
} $m_2$ & set difference
863 $q_3$ := $q_1$
\ai{$-$
} $q_2$ & difference
865 $i_3$ := $i_1$
\ai{$*$
} $i_2$ & product
867 $s_3$ := $s_1$
\ai{$*$
} $s_2$ & intersection
869 $m_3$ := $m_1$
\ai{$*$
} $m_2$ & intersection
871 $q_2$ := $i$
\ai{$*$
} $q_1$ & product
873 $q_2$ := $q_1$
\ai{$*$
} $i$ & product
875 $q_3$ := $q_1$
\ai{$*$
} $q_2$ & product
877 $f_2$ := $i$
\ai{$*$
} $f_1$ & product
879 $f_2$ := $f_1$
\ai{$*$
} $i$ & product
881 $m_2$ := $m_1$
\ai{$*$
} $s$ & intersect domain of $m_1$ with $s$
883 $q_2$ := $q_1$
\ai{$*$
} $s$ & intersect domain of $q_1$ with $s$
885 $f_2$ := $f_1$
\ai{$*$
} $s$ & intersect domain of $f_1$ with $s$
887 $s_2$ := $m$($s_1$) & apply map $m$ to set $s_1$
889 $q_2$ := $q_1$($s$) & apply $q_1$ to each element in $s$ and compute
890 the sum of the results
892 $l$ := $f$($s$) & apply $f$ to each element in $s$, compute
893 a bound of the results
894 and return a list containing the bound
895 and a boolean that is true if the bound
896 is known to be tight.
898 $m_3$ := $m_1$
\ai[\tt]{.
} $m_2$ & join of $m_1$ and $m_2$
900 $m_3$ := $m_1$
\ai[\tt]{before
} $m_2$ & join of $m_1$ and $m_2$
902 $m_3$ := $m_2$($m_1)$ & join of $m_1$ and $m_2$
904 $m_3$ := $m_2$
\ai[\tt]{after
} $m_1$ & join of $m_1$ and $m_2$
906 $f_3$ := $f_1$
\ai[\tt]{.
} $f_2$ & join of $f_1$ and $f_2$, combining
907 the lists of quasipolynomials over shared domains
909 $q_2$ := $m$
\ai[\tt]{.
} $q_1$ & join of $m$ and $q_1$, taking the sum
910 over all elements in the intersection of the range of $m$ and the domain
913 $q_2$ := $m$
\ai[\tt]{before
} $q_1$ & $q_2$ := $m$
\ai[\tt]{.
} $q_1$
915 $q_2$ := $q_1(m)$ & $q_2$ := $m$
\ai[\tt]{.
} $q_1$
917 $q_2$ := $q_1$
\ai[\tt]{after
} $m$ & $q_2$ := $m$
\ai[\tt]{.
} $q_1$
919 $l$ := $m$
\ai[\tt]{.
} $f$ & join of $m$ and $f$, computing a bound
920 over all elements in the intersection of the range of $m$ and the domain
921 of $f$ and returning a list containing the bound
922 and a boolean that is true if the bound is known to be tight.
924 $l$ := $m$
\ai[\tt]{before
} $f$ & $l$ := $m$
\ai[\tt]{.
} $f$
926 $l$ := $f(m)$ & $l$ := $m$
\ai[\tt]{.
} $f$
928 $l$ := $f$
\ai[\tt]{after
} $m$ & $l$ := $m$
\ai[\tt]{.
} $f$
930 $m$ := $s_1$
\ai[\tt]{->
} $s_2$ & universal map with domain $s_1$
933 $q_2$ := $q_1$
\ai{@
} $s$ &
934 evaluate the piecewise quasipolynomial $q_1$ in each element
935 of the set $s$ and return a piecewise quasipolynomial
936 mapping each of the individual elements to the resulting
939 $q$ := $f$
\ai{@
} $s$ &
940 evaluate the piecewise quasipolynomial fold $f$ in each element
941 of the set $s$ and return a piecewise quasipolynomial
942 mapping each of the individual elements to the resulting
945 $s_3$ := $s_1$
\ai[\tt]{\%
} $s_2$ &
946 simplify $s_1$ in the context of $s_2$, i.e., compute
947 the gist of $s_1$ given $s_2$
949 $m_3$ := $m_1$
\ai[\tt]{\%
} $m_2$ &
950 simplify $m_1$ in the context of $m_2$, i.e., compute
951 the gist of $m_1$ given $m_2$
953 $q_2$ := $q_1$
\ai[\tt]{\%
} $s$ &
954 simplify $q_1$ in the context of the domain $s$, i.e., compute
955 the gist of $q_1$ given $s$
957 $f_2$ := $f_1$
\ai[\tt]{\%
} $s$ &
958 simplify $f_1$ in the context of the domain $s$, i.e., compute
959 the gist of $f_1$ given $s$
961 $m_2$ := $m_1$
\ai[\tt]{\^
{}-
1} & inverse of $m_1$
963 $l$ := $m$
\ai[\tt]{\^
{}+
} &
964 compute an overapproximation of the transitive closure
965 of $m$ and return a list containing the overapproximation
966 and a boolean that is true if the overapproximation
970 the element at position $i$ in the list $l$
972 $b$ := $s_1$
\ai[\tt]{=
} $s_2$ & is $s_1$ equal to $s_2$?
974 $b$ := $m_1$
\ai[\tt]{=
} $m_2$ & is $m_1$ equal to $m_2$?
976 $b$ := $s_1$
\ai[\tt]{<=
} $s_2$ & is $s_1$ a subset of $s_2$?
978 $b$ := $m_1$
\ai[\tt]{<=
} $m_2$ & is $m_1$ a subset of $m_2$?
980 $b$ := $s_1$
\ai[\tt]{<
} $s_2$ & is $s_1$ a proper subset of $s_2$?
982 $b$ := $m_1$
\ai[\tt]{<
} $m_2$ & is $m_1$ a proper subset of $m_2$?
984 $b$ := $s_1$
\ai[\tt]{>=
} $s_2$ & is $s_1$ a superset of $s_2$?
986 $b$ := $m_1$
\ai[\tt]{>=
} $m_2$ & is $m_1$ a superset of $m_2$?
988 $b$ := $s_1$
\ai[\tt]{>
} $s_2$ & is $s_1$ a proper superset of $s_2$?
990 $b$ := $m_1$
\ai[\tt]{>
} $m_2$ & is $m_1$ a proper superset of $m_2$?
992 $m$ := $s_1$
\ai[\tt]{<<
} $s_2$ & a map from
993 $s_1$ to $s_2$ of those elements that live in the same space and
994 such that the elements of $s_1$ are lexicographically strictly smaller
997 $m_3$ := $m_1$
\ai[\tt]{<<
} $m_2$ & a map from the domain of
998 $m_1$ to the domain of $m_2$ of those elements such that their images
999 live in the same space and such that the images of the elements of
1000 $m_1$ are lexicographically strictly smaller than those of $m_2$.
1002 $m$ := $s_1$
\ai[\tt]{<<=
} $s_2$ & a map from
1003 $s_1$ to $s_2$ of those elements that live in the same space and
1004 such that the elements of $s_1$ are lexicographically smaller
1005 than those of $s_2$.
1007 $m_3$ := $m_1$
\ai[\tt]{<<=
} $m_2$ & a map from the domain of
1008 $m_1$ to the domain of $m_2$ of those elements such that their images
1009 live in the same space and such that the images of the elements of
1010 $m_1$ are lexicographically smaller than those of $m_2$.
1012 $m$ := $s_1$
\ai[\tt]{>>
} $s_2$ & a map from
1013 $s_1$ to $s_2$ of those elements that live in the same space and
1014 such that the elements of $s_1$ are lexicographically strictly greater
1015 than those of $s_2$.
1017 $m_3$ := $m_1$
\ai[\tt]{>>
} $m_2$ & a map from the domain of
1018 $m_1$ to the domain of $m_2$ of those elements such that their images
1019 live in the same space and such that the images of the elements of
1020 $m_1$ are lexicographically strictly greater than those of $m_2$.
1022 $m$ := $s_1$
\ai[\tt]{>>=
} $s_2$ & a map from
1023 $s_1$ to $s_2$ of those elements that live in the same space and
1024 such that the elements of $s_1$ are lexicographically greater
1025 than those of $s_2$.
1027 $m_3$ := $m_1$
\ai[\tt]{>>=
} $m_2$ & a map from the domain of
1028 $m_1$ to the domain of $m_2$ of those elements such that their images
1029 live in the same space and such that the images of the elements of
1030 $m_1$ are lexicographically greater than those of $m_2$.