doc/isl.tex

   1 \section{\protect\isl/ interface}
   2
   3 \subsection{Library}
   4
   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.
  11
  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.
  21
  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}.
  32
  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
  43 \subsection{Calculator}
  44
  45 The \ai[\tt]{iscc} calculator offers an interface to some
  46 of the functionality provided by the \isl/ and \barvinok/
  47 libraries.
  48 The supported operations are shown in \autoref{t:iscc}.
  49 Here are some examples:
  50 \begin{verbatim}
  51 P := [n, m] -> { [i,j] : 0 <= i <= n and i <= j <= m };
  52 card P;
  53
  54 f := [n,m] -> { [i,j] -> i*j + n*i*i*j : i,j >= 0 and 5i + 27j <= n+m };
  55 sum f;
  56 s := sum f;
  57 s @ [n,m] -> { [] : 0 <= n,m <= 20 };
  58
  59 f := [n] -> { [i] -> 2*n*i - n*n + 3*n - 1/2*i*i - 3/2*i-1 :
  60                 (exists j : 0 <= i < 4*n-1 and 0 <= j < n and
  61                             2*n-1 <= i+j <= 4*n-2 and i <= 2*n-1 ) };
  62 ub f;
  63 u := (ub f)[0];
  64 u @ [n] -> { [] : 0 <= n <= 10 };
  65
  66 m := [n] -> { [i,j] -> [i+1,j+1] : 1 <= i,j < n;
  67               [i,j] -> [i+1,j-1] : 1 <= i < n and 2 <= j <= n };
  68 m^+;
  69 (m^+)[0];
  70
  71 codegen [N] -> { A[i] -> [i,0] : 0 <= i <= N; B[i] -> [i,1] : 1 <= i <= N };
  72 \end{verbatim}
  73
  74 \bottomcaption{{\tt iscc} operations.  The variables
  75 have the following types,
  76 $s$: set,
  77 $m$: map,
  78 $q$: piecewise quasipolynomial,
  79 $f$: piecewise quasipolynomial fold,
  80 $l$: list,
  81 $i$: integer,
  82 $b$: boolean,
  83 $o$: object of any type
  84 }
  85 \label{t:iscc}
  86 \tablehead{
  87 \hline
  88 Syntax & Meaning
  89 \\
  90 \hline
  91 }
  92 \tabletail{
  93 \multicolumn{2}{r}{\small\sl continued on next page}
  94 \\
  95 }
  96 \tablelasttail{}
  97 \begin{supertabular}{lp{0.7\textwidth}}
  98 $s_2$ := \ai[\tt]{aff} $s_1$ & affine hull of $s_1$
  99 \\
 100 $m_2$ := \ai[\tt]{aff} $m_1$ & affine hull of $m_1$
 101 \\
 102 $q$ := \ai[\tt]{card} $s$ &
 103 number of elements in the set $s$
 104 \\
 105 $q$ := \ai[\tt]{card} $m$ &
 106 number of elements in the image of a domain element
 107 \\
 108 $s_2$ := \ai[\tt]{coalesce} $s_1$ &
 109 simplify the representation of set $s_1$ by trying
 110 to combine pairs of basic sets into a single
 111 basic set
 112 \\
 113 $m_2$ := \ai[\tt]{coalesce} $m_1$ &
 114 simplify the representation of map $m_1$ by trying
 115 to combine pairs of basic maps into a single
 116 basic map
 117 \\
 118 $q_2$ := \ai[\tt]{coalesce} $q_1$ &
 119 simplify the representation of $q_1$ by trying
 120 to combine pairs of basic sets in the domain
 121 of $q_1$ into a single basic set
 122 \\
 123 $f_2$ := \ai[\tt]{coalesce} $f_1$ &
 124 simplify the representation of $f_1$ by trying
 125 to combine pairs of basic sets in the domain
 126 of $f_1$ into a single basic set
 127 \\
 128 \ai[\tt]{codegen} $m$ &
 129 generate code for the given scattering function.
 130 This operation is only available if \ai[\tt]{CLooG}
 131 support was compiled in.
 132 \\
 133 $s_3$ := $s_1$ \ai[\tt]{cross} $s_2$ &
 134 Cartesian product of $s_1$ and $s_2$
 135 \\
 136 $m_3$ := $m_1$ \ai[\tt]{cross} $m_2$ &
 137 Cartesian product of $m_1$ and $m_2$
 138 \\
 139 $s$ := \ai[\tt]{deltas} $m$ &
 140 the set $\{\, y - x \mid x \to y \in m \,\}$
 141 \\
 142 $s$ := \ai[\tt]{dom} $m$ &
 143 domain of map $m$
 144 \\
 145 $s$ := \ai[\tt]{dom} $q$ &
 146 domain of piecewise quasipolynomial $q$
 147 \\
 148 $s$ := \ai[\tt]{dom} $f$ &
 149 domain of piecewise quasipolynomial fold $f$
 150 \\
 151 $s$ := \ai[\tt]{ran} $m$ &
 152 range of map $m$
 153 \\
 154 $s_2$ := \ai[\tt]{lexmin} $s_1$ &
 155 lexicographically minimal element of $s_1$
 156 \\
 157 $m_2$ := \ai[\tt]{lexmin} $m_1$ &
 158 lexicographically minimal image element
 159 \\
 160 $s_2$ := \ai[\tt]{lexmax} $s_1$ &
 161 lexicographically maximal element of $s_1$
 162 \\
 163 $m_2$ := \ai[\tt]{lexmax} $m_1$ &
 164 lexicographically maximal image element
 165 \\
 166 $o$ := \ai[\tt]{read} {\tt "}{\it filename}{\tt"} &
 167 read object from file
 168 \\
 169 $s_2$ := \ai[\tt]{sample} $s_1$ &
 170 a sample element of the set $s_1$
 171 \\
 172 $m_2$ := \ai[\tt]{sample} $m_1$ &
 173 a sample element of the map $m_1$
 174 \\
 175 $q_2$ := \ai[\tt]{sum} $q_1$ &
 176 sum $q_1$ over all integer points in the domain of $q_1$
 177 \\
 178 $l$ := \ai[\tt]{ub} $q$ &
 179 compute an
 180 upper bound on the piecewise quasipolynomial $q$ over
 181 all integer points in the domain of $q$
 182 and return a list containing the upper bound
 183 and a boolean that is true if the upper bound
 184 is known to be tight
 185 \\
 186 $l$ := \ai[\tt]{vertices} $s$ &
 187 a list of vertices of the rational polytope defined by the same constraints
 188 as $s$
 189 \\
 190 $s_3$ := $s_1$ \ai{$+$} $s_2$ & union
 191 \\
 192 $m_3$ := $m_1$ \ai{$+$} $m_2$ & union
 193 \\
 194 $q_3$ := $q_1$ \ai{$+$} $q_2$ & sum
 195 \\
 196 $s_3$ := $s_1$ \ai{$-$} $s_2$ & set difference
 197 \\
 198 $m_3$ := $m_1$ \ai{$-$} $m_2$ & set difference
 199 \\
 200 $q_3$ := $q_1$ \ai{$-$} $q_2$ & difference
 201 \\
 202 $s_3$ := $s_1$ \ai{$*$} $s_2$ & intersection
 203 \\
 204 $m_3$ := $m_1$ \ai{$*$} $m_2$ & intersection
 205 \\
 206 $q_3$ := $q_1$ \ai{$*$} $q_2$ & product
 207 \\
 208 $m_2$ := $m_1$ \ai{$*$} $s$ & intersect domain of $m_1$ with $s$
 209 \\
 210 $q_2$ := $q_1$ \ai{$*$} $s$ & intersect domain of $q_1$ with $s$
 211 \\
 212 $f_2$ := $f_1$ \ai{$*$} $s$ & intersect domain of $f_1$ with $s$
 213 \\
 214 $s_2$ := $m$($s_1$) & apply map $m$ to set $s_1$
 215 \\
 216 $m_3$ := $m_1$ \ai[\tt]{.} $m_2$ & join of $m_1$ and $m_2$
 217 \\
 218 $m_3$ := $m_2$($m_1)$ & join of $m_1$ and $m_2$
 219 \\
 220 $m$ := $s_1$ \ai[\tt]{->} $s_2$ & universal map with domain $s_1$
 221 and range $s_2$
 222 \\
 223 $q_2$ := $q_1$ \ai{@} $s$ &
 224 evaluate the piecewise quasipolynomial $q_1$ in each element
 225 of the set $s$ and return a piecewise quasipolynomial
 226 mapping each of the individual elements to the resulting
 227 constant
 228 \\
 229 $q$ := $f$ \ai{@} $s$ &
 230 evaluate the piecewise quasipolynomial fold $f$ in each element
 231 of the set $s$ and return a piecewise quasipolynomial
 232 mapping each of the individual elements to the resulting
 233 constant
 234 \\
 235 $s_3$ := $s_1$ \ai[\tt]{\%} $s_2$ &
 236 simplify $s_1$ in the context of $s_2$, i.e., compute
 237 the gist of $s_1$ given $s_2$
 238 \\
 239 $m_3$ := $m_1$ \ai[\tt]{\%} $m_2$ &
 240 simplify $m_1$ in the context of $m_2$, i.e., compute
 241 the gist of $m_1$ given $m_2$
 242 \\
 243 $q_2$ := $q_1$ \ai[\tt]{\%} $s$ &
 244 simplify $q_1$ in the context of the domain $s$, i.e., compute
 245 the gist of $q_1$ given $s$
 246 \\
 247 $f_2$ := $f_1$ \ai[\tt]{\%} $s$ &
 248 simplify $f_1$ in the context of the domain $s$, i.e., compute
 249 the gist of $f_1$ given $s$
 250 \\
 251 $m_2$ := $m_1$\ai[\tt]{\^{}-1} & inverse of $m_1$
 252 \\
 253 $l$ := $m$\ai[\tt]{\^{}+} &
 254 compute an overapproximation of the transitive closure
 255 of $m$ and return a list containing the overapproximation
 256 and a boolean that is true if the overapproximation
 257 is known to be exact
 258 \\
 259 $o$ := $l$[$i$] &
 260 the element at position $i$ in the list $l$
 261 \\
 262 $b$ := $s_1$ \ai[\tt]{=} $s_2$ & is $s_1$ equal to $s_2$?
 263 \\
 264 $b$ := $m_1$ \ai[\tt]{=} $m_2$ & is $m_1$ equal to $m_2$?
 265 \\
 266 $b$ := $s_1$ \ai[\tt]{<=} $s_2$ & is $s_1$ a subset of $s_2$?
 267 \\
 268 $b$ := $m_1$ \ai[\tt]{<=} $m_2$ & is $m_1$ a subset of $m_2$?
 269 \\
 270 $b$ := $s_1$ \ai[\tt]{<} $s_2$ & is $s_1$ a proper subset of $s_2$?
 271 \\
 272 $b$ := $m_1$ \ai[\tt]{<} $m_2$ & is $m_1$ a proper subset of $m_2$?
 273 \\
 274 $b$ := $s_1$ \ai[\tt]{>=} $s_2$ & is $s_1$ a superset of $s_2$?
 275 \\
 276 $b$ := $m_1$ \ai[\tt]{>=} $m_2$ & is $m_1$ a superset of $m_2$?
 277 \\
 278 $b$ := $s_1$ \ai[\tt]{>} $s_2$ & is $s_1$ a proper superset of $s_2$?
 279 \\
 280 $b$ := $m_1$ \ai[\tt]{>} $m_2$ & is $m_1$ a proper superset of $m_2$?
 281 \\
 282 \end{supertabular}