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

//===- IntegerRelation.h - MLIR IntegerRelation 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
//
//===----------------------------------------------------------------------===//
//
// A class to represent a relation over integer tuples. A relation is
// represented as a constraint system over a space of tuples of integer valued
// variables supporting symbolic variables and existential quantification.
//
//===----------------------------------------------------------------------===//

#ifndef MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H
#define MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H

#include "mlir/Analysis/Presburger/Fraction.h"
#include "mlir/Analysis/Presburger/Matrix.h"
#include "mlir/Analysis/Presburger/PresburgerSpace.h"
#include "mlir/Analysis/Presburger/Utils.h"
#include "llvm/ADT/DynamicAPInt.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/LogicalResult.h"
#include <optional>

namespace mlir {
namespace presburger {
DynamicAPInt;
failure;
int64fromDynamicAPInt;
LogicalResult;
SmallVectorImpl;
success;

class IntegerRelation;
class IntegerPolyhedron;
class PresburgerSet;
class PresburgerRelation;
struct SymbolicLexOpt;

/// The type of bound: equal, lower bound or upper bound.
enum class BoundType { … };

/// An IntegerRelation represents the set of points from a PresburgerSpace that
/// satisfy a list of affine constraints. Affine constraints can be inequalities
/// or equalities in the form:
///
/// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0
/// Equality  : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0
///
/// where c_0, c_1, ..., c_n are integers and n is the total number of
/// variables in the space.
///
/// Such a relation corresponds to the set of integer points lying in a convex
/// polyhedron. For example, consider the relation:
///         (x) -> (y) : (1 <= x <= 7, x = 2y)
/// These can be thought of as points in the polyhedron:
///         (x, y) : (1 <= x <= 7, x = 2y)
/// This relation contains the pairs (2, 1), (4, 2), and (6, 3).
///
/// Since IntegerRelation makes a distinction between dimensions, VarKind::Range
/// and VarKind::Domain should be used to refer to dimension variables.
class IntegerRelation { … };

/// An IntegerPolyhedron represents the set of points from a PresburgerSpace
/// that satisfy a list of affine constraints. Affine constraints can be
/// inequalities or equalities in the form:
///
/// Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0
/// Equality  : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0
///
/// where c_0, c_1, ..., c_n are integers and n is the total number of
/// variables in the space.
///
/// An IntegerPolyhedron is similar to an IntegerRelation but it does not make a
/// distinction between Domain and Range variables. Internally,
/// IntegerPolyhedron is implemented as a IntegerRelation with zero domain vars.
///
/// Since IntegerPolyhedron does not make a distinction between kinds of
/// dimensions, VarKind::SetDim should be used to refer to dimension
/// variables.
class IntegerPolyhedron : public IntegerRelation { … };

} // namespace presburger
} // namespace mlir

#endif // MLIR_ANALYSIS_PRESBURGER_INTEGERRELATION_H