llvm/mlir/include/mlir/Analysis/Presburger/PresburgerSpace.h

//===- PresburgerSpace.h - MLIR PresburgerSpace Class -----------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
// Classes representing space information like number of variables and kind of
// variables.
//
//===----------------------------------------------------------------------===//

#ifndef MLIR_ANALYSIS_PRESBURGER_PRESBURGERSPACE_H
#define MLIR_ANALYSIS_PRESBURGER_PRESBURGERSPACE_H

#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/PointerLikeTypeTraits.h"
#include "llvm/Support/TypeName.h"
#include "llvm/Support/raw_ostream.h"

namespace mlir {
namespace presburger {
ArrayRef;
SmallVector;

/// Kind of variable. Implementation wise SetDims are treated as Range
/// vars, and spaces with no distinction between dimension vars are treated
/// as relations with zero domain vars.
enum class VarKind { … };

/// An Identifier stores a pointer to an object, such as a Value or an
/// Operation. Identifiers are intended to be attached to a variable in a
/// PresburgerSpace and can be used to check if two variables correspond to the
/// same object.
///
/// Take for example the following code:
///
/// for i = 0 to 100
///   for j = 0 to 100
///     S0: A[j] = 0
///   for k = 0 to 100
///     S1: A[k] = 1
///
/// If we represent the space of iteration variables surrounding S0, S1 we have:
/// space(S0): {d0, d1}
/// space(S1): {d0, d1}
///
/// Since the variables are in different spaces, without an identifier, there
/// is no way to distinguish if the variables in the two spaces correspond to
/// different SSA values in the program. So, we attach an Identifier
/// corresponding to the loop iteration variable to them. Now,
///
/// space(S0) = {d0(id = i), d1(id = j)}
/// space(S1) = {d0(id = i), d1(id = k)}.
///
/// Using the identifier, we can check that the first iteration variable in
/// both the spaces correspond to the same variable in the program, while they
/// are different for second iteration variable.
///
/// The equality of Identifiers is checked by comparing the stored pointers.
/// Checking equality asserts that the type of the equal identifiers is same.
/// Identifiers storing null pointers are treated as having no attachment and
/// are considered unequal to any other identifier, including other identifiers
/// with no attachments.
///
/// The type of the pointer stored must have an `llvm::PointerLikeTypeTraits`
/// specialization.
class Identifier { … };

/// PresburgerSpace is the space of all possible values of a tuple of integer
/// valued variables/variables. Each variable has one of the three types:
///
/// Dimension: Ordinary variables over which the space is represented.
///
/// Symbol: Symbol variables correspond to fixed but unknown values.
/// Mathematically, a space with symbolic variables is like a
/// family of spaces indexed by the symbolic variables.
///
/// Local: Local variables correspond to existentially quantified variables.
/// For example, consider the space: `(x, exists q)` where x is a dimension
/// variable and q is a local variable. Let us put the constraints:
///       `1 <= x <= 7, x = 2q`
/// on this space to get the set:
///       `(x) : (exists q : q <= x <= 7, x = 2q)`.
/// An assignment to symbolic and dimension variables is valid if there
/// exists some assignment to the local variable `q` satisfying these
/// constraints. For this example, the set is equivalent to {2, 4, 6}.
/// Mathematically, existential quantification can be thought of as the result
/// of projection. In this example, `q` is existentially quantified. This can be
/// thought of as the result of projecting out `q` from the previous example,
/// i.e. we obtained {2, 4, 6} by projecting out the second dimension from
/// {(2, 1), (4, 2), (6, 2)}.
///
/// Dimension variables are further divided into Domain and Range variables
/// to support building relations.
///
/// Variables are stored in the following order:
///       [Domain, Range, Symbols, Locals]
///
/// A space with no distinction between types of dimension variables can
/// be implemented as a space with zero domain. VarKind::SetDim should be used
/// to refer to dimensions in such spaces.
///
/// Compatibility of two spaces implies that number of variables of each kind
/// other than Locals are equal. Equality of two spaces implies that number of
/// variables of each kind are equal.
///
/// PresburgerSpace optionally also supports attaching an Identifier with each
/// non-local variable in the space. This is disabled by default. `resetIds` is
/// used to enable/reset these identifiers. The user can identify each variable
/// in the space as corresponding to some Identifier. Some example use cases
/// are described in the `Identifier` documentation above. The type attached to
/// the Identifier can be different for different variables in the space.
class PresburgerSpace { … };

} // namespace presburger
} // namespace mlir

#endif // MLIR_ANALYSIS_PRESBURGER_PRESBURGERSPACE_H