iscc: add dependence analysis operations

[barvinok.git] / doc / isl.tex

\section{\protect\isl/ interface}

\let\llt\prec
\let\lle\preccurlyeq
\let\lgt\succ

\subsection{Library}

The \barvinok/ library currently supports only a few
functions that interface with the \isl/ library.
In time, this interface will grow and is set to replace
the \PolyLib/ interface.
For more information on the \isl/ data structures, see
the \isl/ user manual.

\begin{verbatim}
__isl_give isl_pw_qpolynomial *isl_set_card(__isl_take isl_set *set);
__isl_give isl_union_pw_qpolynomial *isl_union_set_card(
        __isl_take isl_union_set *uset);
\end{verbatim}
Compute the number of elements in an \ai[\tt]{isl\_set}
or \ai[\tt]{isl\_union\_set}.
The resulting \ai[\tt]{isl\_pw\_qpolynomial}
or \ai[\tt]{isl\_union\_pw\_qpolynomial} has purely parametric cells.

\begin{verbatim}
__isl_give isl_pw_qpolynomial *isl_map_card(__isl_take isl_map *map);
__isl_give isl_union_pw_qpolynomial *isl_union_map_card(
        __isl_take isl_union_map *umap);
\end{verbatim}
Compute a closed form expression for the number of image elements
associated to any element in the domain of the given \ai[\tt]{isl\_map}
or \ai[\tt]{isl\_union\_map}.
The union of the cells in the resulting \ai[\tt]{isl\_pw\_qpolynomial}
is equal to the domain of the input \ai[\tt]{isl\_map}.

\begin{verbatim}
__isl_give isl_pw_qpolynomial *isl_pw_qpolynomial_sum(
        __isl_take isl_pw_qpolynomial *pwqp);
__isl_give isl_union_pw_qpolynomial *isl_union_pw_qpolynomial_sum(
        __isl_take isl_union_pw_qpolynomial *upwqp);
\end{verbatim}
Compute the sum of the given piecewise quasipolynomial over
all integer points in the domain.  The result is a piecewise
quasipolynomial that only involves the parameters.
If, however, the domain of the piecewise quasipolynomial wraps
a relation, then the sum is computed over all integer points
in the range of that relation and the domain of the relation
becomes the domain of the result.

\begin{verbatim}
__isl_give isl_pw_qpolynomial *isl_map_apply_pw_qpolynomial(
        __isl_take isl_map *map, __isl_take isl_pw_qpolynomial *pwqp);
__isl_give isl_union_pw_qpolynomial *isl_union_map_apply_union_pw_qpolynomial(
        __isl_take isl_union_map *umap,
        __isl_take isl_union_pw_qpolynomial *upwqp);
\end{verbatim}
Compose the given map with the given piecewise quasipolynomial.
That is, compute the sum over all elements in the intersection
of the range of the map and the domain of the piecewise quasipolynomial
as a function of an element in the domain of the map.

\subsection{Calculator}

The \ai[\tt]{iscc} calculator offers an interface to some
of the functionality provided by the \isl/ and \barvinok/
libraries.
The supported operations are shown in \autoref{t:iscc}.
Note that when an operation requires an argument of a certain
type, a binary list with the first element of the required type
may also be used instead.
Here are some examples:
\begin{verbatim}
P := [n, m] -> { [i,j] : 0 <= i <= n and i <= j <= m };
card P;

f := [n,m] -> { [i,j] -> i*j + n*i*i*j : i,j >= 0 and 5i + 27j <= n+m };
sum f;
s := sum f;
s @ [n,m] -> { [] : 0 <= n,m <= 20 };

f := [n] -> { [i] -> 2*n*i - n*n + 3*n - 1/2*i*i - 3/2*i-1 :
                (exists j : 0 <= i < 4*n-1 and 0 <= j < n and
                            2*n-1 <= i+j <= 4*n-2 and i <= 2*n-1 ) };
ub f;
u := (ub f)[0];
u @ [n] -> { [] : 0 <= n <= 10 };

m := [n] -> { [i,j] -> [i+1,j+1] : 1 <= i,j < n;
              [i,j] -> [i+1,j-1] : 1 <= i < n and 2 <= j <= n };
m^+;
(m^+)[0];

codegen [N] -> { A[i] -> [i,0] : 0 <= i <= N; B[i] -> [i,1] : 1 <= i <= N };

{ [k] -> [i] : 1 <= i <= k } . { [n] -> 2 * n : n >= 1 };

{ [m] -> [c] : 1 <= c <= m } . { [k] -> max((3 * k + k^2)) : k >= 1 };
\end{verbatim}

\bottomcaption{{\tt iscc} operations.  The variables
have the following types,
$s$: set,
$m$: map,
$q$: piecewise quasipolynomial,
$f$: piecewise quasipolynomial fold,
$l$: list,
$i$: integer,
$b$: boolean,
$S$: string,
$o$: object of any type
}
\label{t:iscc}
\tablehead{
\hline
Syntax & Meaning
\\
\hline
}
\tabletail{
\multicolumn{2}{r}{\small\sl continued on next page}
\\
}
\tablelasttail{}
\begin{supertabular}{p{0.35\textwidth}p{0.6\textwidth}}
$s_2$ := \ai[\tt]{aff} $s_1$ & affine hull of $s_1$
\\
$m_2$ := \ai[\tt]{aff} $m_1$ & affine hull of $m_1$
\\
$q$ := \ai[\tt]{card} $s$ &
number of elements in the set $s$
\\
$q$ := \ai[\tt]{card} $m$ &
number of elements in the image of a domain element
\\
$s_2$ := \ai[\tt]{coalesce} $s_1$ &
simplify the representation of set $s_1$ by trying
to combine pairs of basic sets into a single
basic set
\\
$m_2$ := \ai[\tt]{coalesce} $m_1$ &
simplify the representation of map $m_1$ by trying
to combine pairs of basic maps into a single
basic map
\\
$q_2$ := \ai[\tt]{coalesce} $q_1$ &
simplify the representation of $q_1$ by trying
to combine pairs of basic sets in the domain
of $q_1$ into a single basic set
\\
$f_2$ := \ai[\tt]{coalesce} $f_1$ &
simplify the representation of $f_1$ by trying
to combine pairs of basic sets in the domain
of $f_1$ into a single basic set
\\
\ai[\tt]{codegen} $s$ &
generate code for the given domain.
This operation is only available if \ai[\tt]{CLooG}
support was compiled in.
\\
\ai[\tt]{codegen} $m$ &
generate code for the given scattering function.
This operation is only available if \ai[\tt]{CLooG}
support was compiled in.
\\
$s_3$ := $s_1$ \ai[\tt]{cross} $s_2$ &
Cartesian product of $s_1$ and $s_2$
\\
$m_3$ := $m_1$ \ai[\tt]{cross} $m_2$ &
Cartesian product of $m_1$ and $m_2$
\\
$s$ := \ai[\tt]{deltas} $m$ &
the set $\{\, y - x \mid x \to y \in m \,\}$
\\
$s$ := \ai[\tt]{dom} $m$ &
domain of map $m$
\\
$s$ := \ai[\tt]{dom} $q$ &
domain of piecewise quasipolynomial $q$
\\
$s$ := \ai[\tt]{dom} $f$ &
domain of piecewise quasipolynomial fold $f$
\\
$s$ := \ai[\tt]{ran} $m$ &
range of map $m$
\\
$s_2$ := \ai[\tt]{lexmin} $s_1$ &
lexicographically minimal element of $s_1$
\\
$m_2$ := \ai[\tt]{lexmin} $m_1$ &
lexicographically minimal image element
\\
$s_2$ := \ai[\tt]{lexmax} $s_1$ &
lexicographically maximal element of $s_1$
\\
$m_2$ := \ai[\tt]{lexmax} $m_1$ &
lexicographically maximal image element
\\
$o$ := \ai[\tt]{read} {\tt "}{\it filename}{\tt"} &
read object from file
\\
$s_2$ := \ai[\tt]{sample} $s_1$ &
a sample element of the set $s_1$
\\
$m_2$ := \ai[\tt]{sample} $m_1$ &
a sample element of the map $m_1$
\\
\ai[\tt]{source} {\tt "}{\it filename}{\tt"} &
read commands from file
\\
$q_2$ := \ai[\tt]{sum} $q_1$ &
sum $q_1$ over all integer points in the domain of $q_1$,
or, if the domain of $q_1$ wraps a map, over all integer
points in the range of the wrapped map.
\\
$l$ := \ai[\tt]{ub} $q$ &
compute an
upper bound on the piecewise quasipolynomial $q$ over
all integer points in the domain of $q$
and return a list containing the upper bound
and a boolean that is true if the upper bound
is known to be tight.
If the domain of $q$ wraps a map, then the upper
bound is computed over all integer points in
the range of the wrapped map instead.
\\
$l$ := \ai[\tt]{vertices} $s$ &
a list of vertices of the rational polytope defined by the same constraints
as $s$
\\
$s$ := \ai[\tt]{wrap} $m$ &
wrap the map in a set
\\
$m$ := \ai[\tt]{unwrap} $s$ &
unwrap the map from the set
\\
$m_4$ := \ai[\tt]{any} $m_1$ \ai[\tt]{before} $m_2$ \ai[\tt]{under} $m_3$ &
compute a map from any element $x$ in the domain of $m_1$
to any element $y$ in the domain of $m_2$
such that their images $m_1(x)$ and $m_2(y)$ overlap
and such that $m_3(x) \llt m_3(y)$.
\\
$l$ := \ai[\tt]{last} $m_1$ \ai[\tt]{before} $m_2$ \ai[\tt]{under} $m_3$ &
compute a map that contains for any element $y$ in the domain of $m_2$
a mapping from the lexicographically last element $x$ in the domain of $m_1$
(according to the schedule $m_3$) to $y$
such that $m_1(x)$ and $m_2(y)$ overlap and such that $m_3(x) \llt m_3(y)$.
Return a list containing this map and the set of elements in the domain of
$m_2$ for which there is no corresponding element in the domain of $m_1$.
\\
$m_5$ := \ai[\tt]{any} $m_1$ \ai[\tt]{last} $m_2$ \ai[\tt]{before} $m_3$
\ai[\tt]{under} $m_4$ &
compute a map that contains for any element $y$ in the domain of $m_3$
a mapping from the lexicographically last element $x$ in the domain of $m_2$
(according to the schedule $m_4$) to $y$
such that $m_2(x)$ and $m_3(y)$ overlap and such that $m_4(x) \llt m_4(y)$
as well as from any element $z$ in the domain of $m_1$ such that
$m_1(z)$ and $m_3(y)$ overlap, $m_4(z) \llt m_4(y)$ and such that there
is no $x$ in the domain of $m_2$ with
$m_2(x) \cap m_3(y) \ne \emptyset$ and $m_4(z) \llt m_4(x) \llt m_4(y)$.
\\
$s_3$ := $s_1$ \ai{$+$} $s_2$ & union
\\
$m_3$ := $m_1$ \ai{$+$} $m_2$ & union
\\
$q_3$ := $q_1$ \ai{$+$} $q_2$ & sum
\\
$f_2$ := $f_1$ \ai{$+$} $q$ & sum
\\
$f_2$ := $q$ \ai{$+$} $f_1$ & sum
\\
$S_3$ := $S_1$ \ai{$+$} $S_2$ & concatenation
\\
$S_2$ := $o$ \ai{$+$} $S_1$ &
concatenation of stringification of $o$ and $S_1$
\\
$S_2$ := $S_1$ \ai{$+$} $o$ &
concatenation of $S_1$ and stringification of $o$
\\
$s_3$ := $s_1$ \ai{$-$} $s_2$ & set difference
\\
$m_3$ := $m_1$ \ai{$-$} $m_2$ & set difference
\\
$q_3$ := $q_1$ \ai{$-$} $q_2$ & difference
\\
$s_3$ := $s_1$ \ai{$*$} $s_2$ & intersection
\\
$m_3$ := $m_1$ \ai{$*$} $m_2$ & intersection
\\
$q_3$ := $q_1$ \ai{$*$} $q_2$ & product
\\
$m_2$ := $m_1$ \ai{$*$} $s$ & intersect domain of $m_1$ with $s$
\\
$q_2$ := $q_1$ \ai{$*$} $s$ & intersect domain of $q_1$ with $s$
\\
$f_2$ := $f_1$ \ai{$*$} $s$ & intersect domain of $f_1$ with $s$
\\
$s_2$ := $m$($s_1$) & apply map $m$ to set $s_1$
\\
$m_3$ := $m_1$ \ai[\tt]{.} $m_2$ & join of $m_1$ and $m_2$
\\
$m_3$ := $m_2$($m_1)$ & join of $m_1$ and $m_2$
\\
$f_3$ := $f_1$ \ai[\tt]{.} $f_2$ & join of $f_1$ and $f_2$, combining
the lists of quasipolynomials over shared domains
\\
$q_2$ := $m$ \ai[\tt]{.} $q_1$ & join of $m$ and $q_1$, taking the sum
over all elements in the intersection of the range of $m$ and the domain
of $q_1$
\\
$f_2$ := $m$ \ai[\tt]{.} $f_1$ & join of $m$ and $f_1$, computing a bound
over all elements in the intersection of the range of $m$ and the domain
of $f_1$
\\
$m$ := $s_1$ \ai[\tt]{->} $s_2$ & universal map with domain $s_1$
and range $s_2$
\\
$q_2$ := $q_1$ \ai{@} $s$ &
evaluate the piecewise quasipolynomial $q_1$ in each element
of the set $s$ and return a piecewise quasipolynomial
mapping each of the individual elements to the resulting
constant
\\
$q$ := $f$ \ai{@} $s$ &
evaluate the piecewise quasipolynomial fold $f$ in each element
of the set $s$ and return a piecewise quasipolynomial
mapping each of the individual elements to the resulting
constant
\\
$s_3$ := $s_1$ \ai[\tt]{\%} $s_2$ &
simplify $s_1$ in the context of $s_2$, i.e., compute
the gist of $s_1$ given $s_2$
\\
$m_3$ := $m_1$ \ai[\tt]{\%} $m_2$ &
simplify $m_1$ in the context of $m_2$, i.e., compute
the gist of $m_1$ given $m_2$
\\
$q_2$ := $q_1$ \ai[\tt]{\%} $s$ &
simplify $q_1$ in the context of the domain $s$, i.e., compute
the gist of $q_1$ given $s$
\\
$f_2$ := $f_1$ \ai[\tt]{\%} $s$ &
simplify $f_1$ in the context of the domain $s$, i.e., compute
the gist of $f_1$ given $s$
\\
$m_2$ := $m_1$\ai[\tt]{\^{}-1} & inverse of $m_1$
\\
$l$ := $m$\ai[\tt]{\^{}+} &
compute an overapproximation of the transitive closure
of $m$ and return a list containing the overapproximation
and a boolean that is true if the overapproximation
is known to be exact
\\
$o$ := $l$[$i$] &
the element at position $i$ in the list $l$
\\
$b$ := $s_1$ \ai[\tt]{=} $s_2$ & is $s_1$ equal to $s_2$?
\\
$b$ := $m_1$ \ai[\tt]{=} $m_2$ & is $m_1$ equal to $m_2$?
\\
$b$ := $s_1$ \ai[\tt]{<=} $s_2$ & is $s_1$ a subset of $s_2$?
\\
$b$ := $m_1$ \ai[\tt]{<=} $m_2$ & is $m_1$ a subset of $m_2$?
\\
$b$ := $s_1$ \ai[\tt]{<} $s_2$ & is $s_1$ a proper subset of $s_2$?
\\
$b$ := $m_1$ \ai[\tt]{<} $m_2$ & is $m_1$ a proper subset of $m_2$?
\\
$b$ := $s_1$ \ai[\tt]{>=} $s_2$ & is $s_1$ a superset of $s_2$?
\\
$b$ := $m_1$ \ai[\tt]{>=} $m_2$ & is $m_1$ a superset of $m_2$?
\\
$b$ := $s_1$ \ai[\tt]{>} $s_2$ & is $s_1$ a proper superset of $s_2$?
\\
$b$ := $m_1$ \ai[\tt]{>} $m_2$ & is $m_1$ a proper superset of $m_2$?
\\
$m$ := $s_1$ \ai[\tt]{<<} $s_2$ & a map from
$s_1$ to $s_2$ of those elements that live in the same space and
such that the elements of $s_1$ are lexicographically strictly smaller
than those of $s_2$.
\\
$m_3$ := $m_1$ \ai[\tt]{<<} $m_2$ & a map from the domain of
$m_1$ to the domain of $m_2$ of those elements such that their images
live in the same space and such that the images of the elements of
$m_1$ are lexicographically strictly smaller than those of $m_2$.
\\
$m$ := $s_1$ \ai[\tt]{<<=} $s_2$ & a map from
$s_1$ to $s_2$ of those elements that live in the same space and
such that the elements of $s_1$ are lexicographically smaller
than those of $s_2$.
\\
$m_3$ := $m_1$ \ai[\tt]{<<=} $m_2$ & a map from the domain of
$m_1$ to the domain of $m_2$ of those elements such that their images
live in the same space and such that the images of the elements of
$m_1$ are lexicographically smaller than those of $m_2$.
\\
$m$ := $s_1$ \ai[\tt]{>>} $s_2$ & a map from
$s_1$ to $s_2$ of those elements that live in the same space and
such that the elements of $s_1$ are lexicographically strictly greater
than those of $s_2$.
\\
$m_3$ := $m_1$ \ai[\tt]{>>} $m_2$ & a map from the domain of
$m_1$ to the domain of $m_2$ of those elements such that their images
live in the same space and such that the images of the elements of
$m_1$ are lexicographically strictly greater than those of $m_2$.
\\
$m$ := $s_1$ \ai[\tt]{>>=} $s_2$ & a map from
$s_1$ to $s_2$ of those elements that live in the same space and
such that the elements of $s_1$ are lexicographically greater
than those of $s_2$.
\\
$m_3$ := $m_1$ \ai[\tt]{>>=} $m_2$ & a map from the domain of
$m_1$ to the domain of $m_2$ of those elements such that their images
live in the same space and such that the images of the elements of
$m_1$ are lexicographically greater than those of $m_2$.
\\
\end{supertabular}