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 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.
  46
  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.
  58
  59 \subsection{Calculator}
  60
  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;
  72
  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 };
  77
  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 };
  84
  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];
  89
  90 codegen [N] -> { A[i] -> [i,0] : 0 <= i <= N; B[i] -> [i,1] : 1 <= i <= N };
  91
  92 { [k] -> [i] : 1 <= i <= k } . { [n] -> 2 * n : n >= 1 };
  93
  94 { [m] -> [c] : 1 <= c <= m } . { [k] -> max((3 * k + k^2)) : k >= 1 };
  95 \end{verbatim}
  96
  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 $o$: object of any type
 107 }
 108 \label{t:iscc}
 109 \tablehead{
 110 \hline
 111 Syntax & Meaning
 112 \\
 113 \hline
 114 }
 115 \tabletail{
 116 \multicolumn{2}{r}{\small\sl continued on next page}
 117 \\
 118 }
 119 \tablelasttail{}
 120 \begin{supertabular}{lp{0.7\textwidth}}
 121 $s_2$ := \ai[\tt]{aff} $s_1$ & affine hull of $s_1$
 122 \\
 123 $m_2$ := \ai[\tt]{aff} $m_1$ & affine hull of $m_1$
 124 \\
 125 $q$ := \ai[\tt]{card} $s$ &
 126 number of elements in the set $s$
 127 \\
 128 $q$ := \ai[\tt]{card} $m$ &
 129 number of elements in the image of a domain element
 130 \\
 131 $s_2$ := \ai[\tt]{coalesce} $s_1$ &
 132 simplify the representation of set $s_1$ by trying
 133 to combine pairs of basic sets into a single
 134 basic set
 135 \\
 136 $m_2$ := \ai[\tt]{coalesce} $m_1$ &
 137 simplify the representation of map $m_1$ by trying
 138 to combine pairs of basic maps into a single
 139 basic map
 140 \\
 141 $q_2$ := \ai[\tt]{coalesce} $q_1$ &
 142 simplify the representation of $q_1$ by trying
 143 to combine pairs of basic sets in the domain
 144 of $q_1$ into a single basic set
 145 \\
 146 $f_2$ := \ai[\tt]{coalesce} $f_1$ &
 147 simplify the representation of $f_1$ by trying
 148 to combine pairs of basic sets in the domain
 149 of $f_1$ into a single basic set
 150 \\
 151 \ai[\tt]{codegen} $s$ &
 152 generate code for the given domain.
 153 This operation is only available if \ai[\tt]{CLooG}
 154 support was compiled in.
 155 \\
 156 \ai[\tt]{codegen} $m$ &
 157 generate code for the given scattering function.
 158 This operation is only available if \ai[\tt]{CLooG}
 159 support was compiled in.
 160 \\
 161 $s_3$ := $s_1$ \ai[\tt]{cross} $s_2$ &
 162 Cartesian product of $s_1$ and $s_2$
 163 \\
 164 $m_3$ := $m_1$ \ai[\tt]{cross} $m_2$ &
 165 Cartesian product of $m_1$ and $m_2$
 166 \\
 167 $s$ := \ai[\tt]{deltas} $m$ &
 168 the set $\{\, y - x \mid x \to y \in m \,\}$
 169 \\
 170 $s$ := \ai[\tt]{dom} $m$ &
 171 domain of map $m$
 172 \\
 173 $s$ := \ai[\tt]{dom} $q$ &
 174 domain of piecewise quasipolynomial $q$
 175 \\
 176 $s$ := \ai[\tt]{dom} $f$ &
 177 domain of piecewise quasipolynomial fold $f$
 178 \\
 179 $s$ := \ai[\tt]{ran} $m$ &
 180 range of map $m$
 181 \\
 182 $s_2$ := \ai[\tt]{lexmin} $s_1$ &
 183 lexicographically minimal element of $s_1$
 184 \\
 185 $m_2$ := \ai[\tt]{lexmin} $m_1$ &
 186 lexicographically minimal image element
 187 \\
 188 $s_2$ := \ai[\tt]{lexmax} $s_1$ &
 189 lexicographically maximal element of $s_1$
 190 \\
 191 $m_2$ := \ai[\tt]{lexmax} $m_1$ &
 192 lexicographically maximal image element
 193 \\
 194 $o$ := \ai[\tt]{read} {\tt "}{\it filename}{\tt"} &
 195 read object from file
 196 \\
 197 $s_2$ := \ai[\tt]{sample} $s_1$ &
 198 a sample element of the set $s_1$
 199 \\
 200 $m_2$ := \ai[\tt]{sample} $m_1$ &
 201 a sample element of the map $m_1$
 202 \\
 203 $q_2$ := \ai[\tt]{sum} $q_1$ &
 204 sum $q_1$ over all integer points in the domain of $q_1$,
 205 or, if the domain of $q_1$ wraps a map, over all integer
 206 points in the range of the wrapped map.
 207 \\
 208 $l$ := \ai[\tt]{ub} $q$ &
 209 compute an
 210 upper bound on the piecewise quasipolynomial $q$ over
 211 all integer points in the domain of $q$
 212 and return a list containing the upper bound
 213 and a boolean that is true if the upper bound
 214 is known to be tight.
 215 If the domain of $q$ wraps a map, then the upper
 216 bound is computed over all integer points in
 217 the range of the wrapped map instead.
 218 \\
 219 $l$ := \ai[\tt]{vertices} $s$ &
 220 a list of vertices of the rational polytope defined by the same constraints
 221 as $s$
 222 \\
 223 $s$ := \ai[\tt]{wrap} $m$ &
 224 wrap the map in a set
 225 \\
 226 $m$ := \ai[\tt]{unwrap} $s$ &
 227 unwrap the map from the set
 228 \\
 229 $s_3$ := $s_1$ \ai{$+$} $s_2$ & union
 230 \\
 231 $m_3$ := $m_1$ \ai{$+$} $m_2$ & union
 232 \\
 233 $q_3$ := $q_1$ \ai{$+$} $q_2$ & sum
 234 \\
 235 $f_2$ := $f_1$ \ai{$+$} $q$ & sum
 236 \\
 237 $f_2$ := $q$ \ai{$+$} $f_1$ & sum
 238 \\
 239 $s_3$ := $s_1$ \ai{$-$} $s_2$ & set difference
 240 \\
 241 $m_3$ := $m_1$ \ai{$-$} $m_2$ & set difference
 242 \\
 243 $q_3$ := $q_1$ \ai{$-$} $q_2$ & difference
 244 \\
 245 $s_3$ := $s_1$ \ai{$*$} $s_2$ & intersection
 246 \\
 247 $m_3$ := $m_1$ \ai{$*$} $m_2$ & intersection
 248 \\
 249 $q_3$ := $q_1$ \ai{$*$} $q_2$ & product
 250 \\
 251 $m_2$ := $m_1$ \ai{$*$} $s$ & intersect domain of $m_1$ with $s$
 252 \\
 253 $q_2$ := $q_1$ \ai{$*$} $s$ & intersect domain of $q_1$ with $s$
 254 \\
 255 $f_2$ := $f_1$ \ai{$*$} $s$ & intersect domain of $f_1$ with $s$
 256 \\
 257 $s_2$ := $m$($s_1$) & apply map $m$ to set $s_1$
 258 \\
 259 $m_3$ := $m_1$ \ai[\tt]{.} $m_2$ & join of $m_1$ and $m_2$
 260 \\
 261 $m_3$ := $m_2$($m_1)$ & join of $m_1$ and $m_2$
 262 \\
 263 $f_3$ := $f_1$ \ai[\tt]{.} $f_2$ & join of $f_1$ and $f_2$, combining
 264 the lists of quasipolynomials over shared domains
 265 \\
 266 $q_2$ := $m$ \ai[\tt]{.} $q_1$ & join of $m$ and $q_1$, taking the sum
 267 over all elements in the intersection of the range of $m$ and the domain
 268 of $q_1$
 269 \\
 270 $f_2$ := $m$ \ai[\tt]{.} $f_1$ & join of $m$ and $f_1$, computing a bound
 271 over all elements in the intersection of the range of $m$ and the domain
 272 of $f_1$
 273 \\
 274 $m$ := $s_1$ \ai[\tt]{->} $s_2$ & universal map with domain $s_1$
 275 and range $s_2$
 276 \\
 277 $q_2$ := $q_1$ \ai{@} $s$ &
 278 evaluate the piecewise quasipolynomial $q_1$ in each element
 279 of the set $s$ and return a piecewise quasipolynomial
 280 mapping each of the individual elements to the resulting
 281 constant
 282 \\
 283 $q$ := $f$ \ai{@} $s$ &
 284 evaluate the piecewise quasipolynomial fold $f$ in each element
 285 of the set $s$ and return a piecewise quasipolynomial
 286 mapping each of the individual elements to the resulting
 287 constant
 288 \\
 289 $s_3$ := $s_1$ \ai[\tt]{\%} $s_2$ &
 290 simplify $s_1$ in the context of $s_2$, i.e., compute
 291 the gist of $s_1$ given $s_2$
 292 \\
 293 $m_3$ := $m_1$ \ai[\tt]{\%} $m_2$ &
 294 simplify $m_1$ in the context of $m_2$, i.e., compute
 295 the gist of $m_1$ given $m_2$
 296 \\
 297 $q_2$ := $q_1$ \ai[\tt]{\%} $s$ &
 298 simplify $q_1$ in the context of the domain $s$, i.e., compute
 299 the gist of $q_1$ given $s$
 300 \\
 301 $f_2$ := $f_1$ \ai[\tt]{\%} $s$ &
 302 simplify $f_1$ in the context of the domain $s$, i.e., compute
 303 the gist of $f_1$ given $s$
 304 \\
 305 $m_2$ := $m_1$\ai[\tt]{\^{}-1} & inverse of $m_1$
 306 \\
 307 $l$ := $m$\ai[\tt]{\^{}+} &
 308 compute an overapproximation of the transitive closure
 309 of $m$ and return a list containing the overapproximation
 310 and a boolean that is true if the overapproximation
 311 is known to be exact
 312 \\
 313 $o$ := $l$[$i$] &
 314 the element at position $i$ in the list $l$
 315 \\
 316 $b$ := $s_1$ \ai[\tt]{=} $s_2$ & is $s_1$ equal to $s_2$?
 317 \\
 318 $b$ := $m_1$ \ai[\tt]{=} $m_2$ & is $m_1$ equal to $m_2$?
 319 \\
 320 $b$ := $s_1$ \ai[\tt]{<=} $s_2$ & is $s_1$ a subset of $s_2$?
 321 \\
 322 $b$ := $m_1$ \ai[\tt]{<=} $m_2$ & is $m_1$ a subset of $m_2$?
 323 \\
 324 $b$ := $s_1$ \ai[\tt]{<} $s_2$ & is $s_1$ a proper subset of $s_2$?
 325 \\
 326 $b$ := $m_1$ \ai[\tt]{<} $m_2$ & is $m_1$ a proper subset of $m_2$?
 327 \\
 328 $b$ := $s_1$ \ai[\tt]{>=} $s_2$ & is $s_1$ a superset of $s_2$?
 329 \\
 330 $b$ := $m_1$ \ai[\tt]{>=} $m_2$ & is $m_1$ a superset of $m_2$?
 331 \\
 332 $b$ := $s_1$ \ai[\tt]{>} $s_2$ & is $s_1$ a proper superset of $s_2$?
 333 \\
 334 $b$ := $m_1$ \ai[\tt]{>} $m_2$ & is $m_1$ a proper superset of $m_2$?
 335 \\
 336 \end{supertabular}