About `namedisl`¶

Polyhedral model¶

The polyhedral model permits precise reasoning about subsets of \(\mathbb{Z}^n\). A subset is expressed as an intersection of affine constraints:

\[\begin{split}\begin{align*} a_1 z_1+ \cdots + a_n z_n + c &\ge 0, \quad \text{or}\\ a_1 z_1+ \cdots + a_n z_n + c &= 0, \end{align*}\end{split}\]

with \(a_i,c\in\mathbb Z\) fixed coefficients and \(z_i\) the dimensions of the set.

An intersection of these hyperplanes or half-spaces is a BasicSet. Individual dimensions may be marked as ‘existentially quantified’ (or equivalently, ‘projected out’, cf. BasicSet.project_out()). In the absence of existentially quantified variables, the resulting set is convex, in their presence it is called quasi-convex.

Other dimensions may be marked as ‘parameters’ (cf. DimType.param). Observe that this has the effect of allowing size-parametric set operations, allowing operation on an infinite, symbolically-defined family of sets.

A union of BasicSets is a Set, which is not necessarily convex.

Map s (with their analogous BasicMaps) are mathematically the same as sets, but permit labeling some of their dimensions as “inputs” (cf. DimType.in_), making them suited to represent relations (such ass data access or dependency).

An Aff is a quasi-affine expression as above, with existentially quantified variables expressed in the form of modular arithmetic.

A PwAff is a piecewise quasi-affine expression, consisting of tuples (set, aff), with each Set indicating where the corresponding Aff defines the value of the expression.

`namedisl` interface guide¶

Immutability¶

Every object in namedisl should be considered immutable. Even if mutation is technically possible via Python gymnastics, the results of doing so are undefined.

All objects are hashable, with equality semantics defined as below.

Equality¶

The == operator uses the cheapest and strictest available comparison. It is mainly intended for use in hashing/ cache retrieval.

Mathematical equivalence may be available as a separate, likely more expensive operation (cf. Set.equals()).

Dimension names are required to match in order for equality to hold. To keep comparison inexpensive, dimension order in the underlying isl object (while not otherwise exposed) is also required to match for equality.

Names matter¶

Consider the sets {[i]: 0<=i<10} and {[j]: 0<=j<10} the same set. Observe

>>> import namedisl as nisl
>>> print(nisl.make_set("{[i]: 0<=i<10}") & nisl.make_set("{[j]: 0<=j<10}"))
{ [i, j] : 0 <= i <= 9 and 0 <= j <= 9 }

I.e., since i and j have different names, they are considered different dimensions.

namedisl keeps name information in Space objects that are shared when possible.

Dimension order is an implementation detail¶

With the exception of hashing and == equality, dimension order (even if it can be observed by examining the Space or through conversion to str) is an implementation detail that does not influence the result of an operation. Dimension order of internal ISL objects is not guaranteed to be stable and may change without notice.

Constructors are private¶

Object instances should be created via make_* functions. Constructors should never be directly called by user code.

About namedisl¶