diff --git a/mlir/include/mlir-c/Presburger.h b/mlir/include/mlir-c/Presburger.h new file mode 100644 index 0000000000000..3146f1ec205d8 --- /dev/null +++ b/mlir/include/mlir-c/Presburger.h @@ -0,0 +1,532 @@ +//===-- mlir-c/Presburger.h - C API to Presburger library ---------*- 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 +// +//===----------------------------------------------------------------------===// +// +// This header declares the C interface to Presburger library. +// +//===----------------------------------------------------------------------===// + +#ifndef MLIR_C_PRESBURGER_H +#define MLIR_C_PRESBURGER_H +#include "mlir-c/Support.h" + +#ifdef __cplusplus +extern "C" { +#endif + +enum MlirPresburgerVariableKind { + Symbol, + Local, + Domain, + Range, + SetDim = Range +}; + +enum MlirPresburgerBoundType { EQ, LB, UB }; + +enum MlirPresburgerOptimumKind { Empty, Unbounded, Bounded }; + +struct MlirOptionalInt64 { + bool hasValue; + int64_t value; +}; + +typedef struct MlirOptionalInt64 MlirOptionalInt64; + +struct MlirOptionalVectorInt64 { + bool hasValue; + const int64_t *data; + int64_t size; +}; + +typedef struct MlirOptionalVectorInt64 MlirOptionalVectorInt64; + +struct MlirMaybeOptimum { + enum MlirPresburgerOptimumKind kind; + MlirOptionalVectorInt64 vector; +}; + +typedef struct MlirMaybeOptimum MlirMaybeOptimum; + +#define DEFINE_C_API_STRUCT(name, storage) \ + struct name { \ + storage *ptr; \ + }; \ + typedef struct name name +DEFINE_C_API_STRUCT(MlirPresburgerIntegerRelation, void); +#undef DEFINE_C_API_STRUCT + +//===----------------------------------------------------------------------===// +// IntegerRelation creation/destruction and basic metadata operations +//===----------------------------------------------------------------------===// + +/// Constructs a relation reserving memory for the specified number +/// of constraints and variables. +MLIR_CAPI_EXPORTED MlirPresburgerIntegerRelation +mlirPresburgerIntegerRelationCreate(unsigned numReservedInequalities, + unsigned numReservedEqualities, + unsigned numReservedCols); + +/// Constructs an IntegerRelation from a packed 2D matrix of tableau +/// coefficients in row-major order. The first `numDomainVars` columns are +/// considered domain and the remaining `numRangeVars` columns are domain +/// variables. +MLIR_CAPI_EXPORTED MlirPresburgerIntegerRelation +mlirPresburgerIntegerRelationCreateFromCoefficients( + const int64_t *inequalityCoefficients, unsigned numInequalities, + const int64_t *equalityCoefficients, unsigned numEqualities, + unsigned numDomainVars, unsigned numRangeVars, + unsigned numExtraReservedInequalities = 0, + unsigned numExtraReservedEqualities = 0, unsigned numExtraReservedCols = 0); + +/// Destroys an IntegerRelation. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationDestroy(MlirPresburgerIntegerRelation relation); + +//===----------------------------------------------------------------------===// +// IntegerRelation binary operations +//===----------------------------------------------------------------------===// + +/// Appends constraints from `lhs` into `rhs`. This is equivalent to an +/// intersection with no simplification of any sort attempted. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationAppend(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Return the intersection of the two relations. +/// If there are locals, they will be merged. +MLIR_CAPI_EXPORTED MlirPresburgerIntegerRelation +mlirPresburgerIntegerRelationIntersect(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Return whether `lhs` and `rhs` are equal. This is integer-exact +/// and somewhat expensive, since it uses the integer emptiness check +/// (see IntegerRelation::findIntegerSample()). +MLIR_CAPI_EXPORTED bool +mlirPresburgerIntegerRelationIsEqual(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Perform a quick equality check on `lhs` and `rhs`. The relations are +/// equal if the check return true, but may or may not be equal if the check +/// returns false. The equality check is performed in a plain manner, by +/// comparing if all the equalities and inequalities in `lhs` and `rhs` +/// are the same. +MLIR_CAPI_EXPORTED bool mlirPresburgerIntegerRelationIsObviouslyEqual( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs); + +/// Return whether `lhs` is a subset of the `rhs` IntegerRelation. This is +/// integer-exact and somewhat expensive, since it uses the integer emptiness. +MLIR_CAPI_EXPORTED bool +mlirPresburgerIntegerRelationIsSubsetOf(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Merge and align symbol variables of `lhs` and `rhs` with respect to +/// identifiers. After this operation the symbol variables of both relations +/// have the same identifiers in the same order. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationMergeAndAlignSymbols( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs); + +/// Adds additional local vars to the sets such that they both have the union +/// of the local vars in each set, without changing the set of points that +/// lie in `lhs` and `rhs`. +/// +/// While taking union, if a local var in `rhs` has a division +/// representation which is a duplicate of division representation, of another +/// local var, it is not added to the final union of local vars and is instead +/// merged. The new ordering of local vars is: +/// +/// [Local vars of `lhs`] [Non-merged local vars of `rhs`] +/// +/// The relative ordering of local vars is same as before. +/// +/// After merging, if the `i^th` local variable in one set has a known +/// division representation, then the `i^th` local variable in the other set +/// either has the same division representation or no known division +/// representation. +/// +/// The spaces of both relations should be compatible. +/// +/// Returns the number of non-merged local vars of `rhs`, i.e. the number of +/// locals that have been added to `lhs`. +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationMergeLocalVars(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Let the relation `lhs` be R1, and the relation `rhs` be R2. Modifies R1 +/// to be the composition of R1 and R2: R1;R2. +/// +/// Formally, if R1: A -> B, and R2: B -> C, then this function returns a +/// relation R3: A -> C such that a point (a, c) belongs to R3 iff there +/// exists b such that (a, b) is in R1 and, (b, c) is in R2. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationCompose(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Let the relation `lhs` be R1, and the relation `rhs` be R2. Applies the +/// relation to the domain of R2. +/// +/// R1: i -> j : (0 <= i < 2, j = i) +/// R2: i -> k : (k = i floordiv 2) +/// R3: k -> j : (0 <= k < 1, 2k <= j <= 2k + 1) +/// +/// R1 = {(0, 0), (1, 1)}. R2 maps both 0 and 1 to 0. +/// So R3 = {(0, 0), (0, 1)}. +/// +/// Formally, R1.applyDomain(R2) = R2.inverse().compose(R1). +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationApplyDomain(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Let the relation `lhs` be R1, and the relation `rhs` be R2. Applies the +/// relation to the range of R2. +/// +/// Formally, R1.applyRange(R2) is the same as R1.compose(R2) but we provide +/// this for uniformity with `applyDomain`. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationApplyRange(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Given a relation `rhs: (A -> B)`, this operation merges the symbol and +/// local variables and then takes the composition of `rhs` on `lhs: (B -> +/// C)`. The resulting relation represents tuples of the form: `A -> C`. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationMergeAndCompose(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs); + +/// Updates the constraints to be the smallest bounding (enclosing) box that +/// contains the points of `lhs` set and that of `rhs`, with the symbols +/// being treated specially. For each of the dimensions, the min of the lower +/// bounds (symbolic) and the max of the upper bounds (symbolic) is computed +/// to determine such a bounding box. `rhs` is expected to have the same +/// dimensional variables as this constraint system (in the same order). +/// +/// E.g.: +/// 1) this = {0 <= d0 <= 127}, +/// other = {16 <= d0 <= 192}, +/// output = {0 <= d0 <= 192} +/// 2) this = {s0 + 5 <= d0 <= s0 + 20}, +/// other = {s0 + 1 <= d0 <= s0 + 9}, +/// output = {s0 + 1 <= d0 <= s0 + 20} +/// 3) this = {0 <= d0 <= 5, 1 <= d1 <= 9} +/// other = {2 <= d0 <= 6, 5 <= d1 <= 15}, +/// output = {0 <= d0 <= 6, 1 <= d1 <= 15} +MLIR_CAPI_EXPORTED MlirLogicalResult +mlirPresburgerIntegerRelationUnionBoundingBox( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs); + +//===----------------------------------------------------------------------===// +// IntegerRelation Tableau Inspection +//===----------------------------------------------------------------------===// + +/// Returns the value at the specified equality row and column. +MLIR_CAPI_EXPORTED int64_t mlirPresburgerIntegerRelationAtEq64( + MlirPresburgerIntegerRelation relation, unsigned row, unsigned col); + +/// Returns the value at the specified inequality row and column. +MLIR_CAPI_EXPORTED int64_t mlirPresburgerIntegerRelationAtIneq64( + MlirPresburgerIntegerRelation relation, unsigned row, unsigned col); + +/// Returns the number of inequalities and equalities. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumConstraints( + MlirPresburgerIntegerRelation relation); + +/// Returns the number of columns classified as domain variables. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumDomainVars( + MlirPresburgerIntegerRelation relation); + +/// Returns the number of columns classified as range variables. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumRangeVars( + MlirPresburgerIntegerRelation relation); + +/// Returns the number of columns classified as symbol variables. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumSymbolVars( + MlirPresburgerIntegerRelation relation); + +/// Returns the number of columns classified as local variables. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumLocalVars( + MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationNumDimVars(MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumDimAndSymbolVars( + MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationNumVars(MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationNumCols(MlirPresburgerIntegerRelation relation); + +/// Returns the number of equality constraints. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumEqualities( + MlirPresburgerIntegerRelation relation); + +/// Returns the number of inequality constraints. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumInequalities( + MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumReservedEqualities( + MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationNumReservedInequalities( + MlirPresburgerIntegerRelation relation); + +/// Get the number of vars of the specified kind. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationGetNumVarKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind); + +/// Return the index at which the specified kind of vars starts. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationGetVarKindOffset( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind); + +/// Return the index at Which the specified kind of vars ends. +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationGetVarKindEnd( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind); + +/// Get the number of elements of the specified kind in the range +/// [varStart, varLimit). +MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationGetVarKindOverLap( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned varStart, unsigned varLimit); + +/// Return the VarKind of the var at the specified position. +MLIR_CAPI_EXPORTED MlirPresburgerVariableKind +mlirPresburgerIntegerRelationGetVarKindAt( + MlirPresburgerIntegerRelation relation, unsigned pos); + +/// Returns the constant bound for the pos^th variable if there is one. +MLIR_CAPI_EXPORTED MlirOptionalInt64 +mlirPresburgerIntegerRelationGetConstantBound64( + MlirPresburgerIntegerRelation relation, MlirPresburgerBoundType type, + unsigned pos); + +/// Check whether all local ids have a division representation. +MLIR_CAPI_EXPORTED bool mlirPresburgerIntegerRelationHasOnlyDivLocals( + MlirPresburgerIntegerRelation relation); + +// Verify whether the relation is full-dimensional, i.e., +// no equality holds for the relation. +// +// If there are no variables, it always returns true. +// If there is at least one variable and the relation is empty, it returns +// false. +MLIR_CAPI_EXPORTED bool +mlirPresburgerIntegerRelationIsFullDim(MlirPresburgerIntegerRelation relation); + +/// Find an integer sample point satisfying the constraints using a +/// branch and bound algorithm with generalized basis reduction, with some +/// additional processing using Simplex for unbounded sets. +/// +/// Returns an integer sample point if one exists, or an empty Optional +/// otherwise. The returned value also includes values of local ids. +MLIR_CAPI_EXPORTED MlirOptionalVectorInt64 +mlirPresburgerIntegerRelationFindIntegerSample( + MlirPresburgerIntegerRelation relation); + +/// Compute an overapproximation of the number of integer points in the +/// relation. Symbol vars currently not supported. If the computed +/// overapproximation is infinite, an empty optional is returned. +MLIR_CAPI_EXPORTED MlirOptionalInt64 mlirPresburgerIntegerRelationComputeVolume( + MlirPresburgerIntegerRelation relation); + +/// Returns true if the given point satisfies the constraints, or false +/// otherwise. Takes the values of all vars including locals. +MLIR_CAPI_EXPORTED bool mlirPresburgerIntegerRelationContainsPoint( + MlirPresburgerIntegerRelation relation, const int64_t *point, int64_t size); + +//===----------------------------------------------------------------------===// +// IntegerRelation Tableau Manipulation +//===----------------------------------------------------------------------===// + +/// Insert `num` variables of the specified kind at position `pos`. +/// Positions are relative to the kind of variable. The coefficient columns +/// corresponding to the added variables are initialized to zero. Return the +/// absolute column position (i.e., not relative to the kind of variable) +/// of the first added variable. +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationInsertVar(MlirPresburgerIntegerRelation relation, + MlirPresburgerVariableKind kind, + unsigned pos, unsigned num = 1); + +/// Append `num` variables of the specified kind after the last variable +/// of that kind. The coefficient columns corresponding to the added variables +/// are initialized to zero. Return the absolute column position (i.e., not +/// relative to the kind of variable) of the first appended variable. +MLIR_CAPI_EXPORTED unsigned +mlirPresburgerIntegerRelationAppendVar(MlirPresburgerIntegerRelation relation, + MlirPresburgerVariableKind kind, + unsigned num = 1); + +/// Adds an equality with the given coefficients. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationAddEquality(MlirPresburgerIntegerRelation relation, + const int64_t *coeff, + int64_t coeffSize); + +/// Adds an inequality with the given coefficients. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationAddInequality( + MlirPresburgerIntegerRelation relation, const int64_t *coeff, + int64_t coeffSize); + +/// Eliminate the `posB^th` local variable, replacing every instance of it +/// with the `posA^th` local variable. This should be used when the two +/// local variables are known to always take the same values. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationEliminateRedundantLocalVar( + MlirPresburgerIntegerRelation relation, unsigned posA, unsigned posB); + +/// Removes variables of the specified kind with the specified pos (or +/// within the specified range) from the system. The specified location is +/// relative to the first variable of the specified kind. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveVarKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned pos); +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveVarRangeKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned varStart, unsigned varLimit); + +/// Removes the specified variable from the system. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationRemoveVar(MlirPresburgerIntegerRelation relation, + unsigned pos); + +/// Remove the (in)equalities at specified position. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveEquality( + MlirPresburgerIntegerRelation relation, unsigned pos); +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveInequality( + MlirPresburgerIntegerRelation relation, unsigned pos); + +/// Remove the (in)equalities at positions [start, end). +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveEqualityRange( + MlirPresburgerIntegerRelation relation, unsigned start, unsigned end); +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveInequalityRange( + MlirPresburgerIntegerRelation relation, unsigned start, unsigned end); + +/// Returns lexicographically minimal integer point. +MLIR_CAPI_EXPORTED MlirMaybeOptimum +mlirPresburgerIntegerRelationFindIntegerLexMin( + MlirPresburgerIntegerRelation relation); + +/// Swap the posA^th variable with the posB^th variable. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationSwapVar(MlirPresburgerIntegerRelation relation, + unsigned posA, unsigned posB); + +/// Removes all equalities and inequalities. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationClearConstraints( + MlirPresburgerIntegerRelation relation); + +/// Sets the `values.size()` variables starting at `po`s to the specified +/// values and removes them. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationSetAndEliminate( + MlirPresburgerIntegerRelation relation, unsigned pos, const int64_t *values, + unsigned valuesSize); + +/// Removes constraints that are independent of (i.e., do not have a +/// coefficient) variables in the range [pos, pos + num). +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationRemoveIndependentConstraints( + MlirPresburgerIntegerRelation relation, unsigned pos, unsigned num); + +/// Returns true if the set can be trivially detected as being +/// hyper-rectangular on the specified contiguous set of variables. +MLIR_CAPI_EXPORTED bool mlirPresburgerIntegerRelationIsHyperRectangular( + MlirPresburgerIntegerRelation relation, unsigned pos, unsigned num); + +/// Removes duplicate constraints, trivially true constraints, and constraints +/// that can be detected as redundant as a result of differing only in their +/// constant term part. A constraint of the form >= 0 +/// is considered trivially true. This method is a linear time method on the +/// constraints, does a single scan, and updates in place. It also normalizes +/// constraints by their GCD and performs GCD tightening on inequalities. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveTrivialRedundancy( + MlirPresburgerIntegerRelation relation); + +/// A more expensive check than `removeTrivialRedundancy` to detect redundant +/// inequalities. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationRemoveRedundantInequalities( + MlirPresburgerIntegerRelation relation); + +/// Removes redundant constraints using Simplex. Although the algorithm can +/// theoretically take exponential time in the worst case (rare), it is known +/// to perform much better in the average case. If V is the number of vertices +/// in the polytope and C is the number of constraints, the algorithm takes +/// O(VC) time. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveRedundantConstraints( + MlirPresburgerIntegerRelation relation); + +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveDuplicateDivs( + MlirPresburgerIntegerRelation relation); + +/// Simplify the constraint system by removing canonicalizing constraints and +/// removing redundant constraints. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationSimplify(MlirPresburgerIntegerRelation relation); + +/// Converts variables of kind srcKind in the range [varStart, varLimit) to +/// variables of kind dstKind. If `pos` is given, the variables are placed at +/// position `pos` of dstKind, otherwise they are placed after all the other +/// variables of kind dstKind. The internal ordering among the moved variables +/// is preserved. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationConvertVarKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind srcKind, + unsigned varStart, unsigned varLimit, MlirPresburgerVariableKind dstKind, + unsigned pos); +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationConvertVarKindNoPos( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind srcKind, + unsigned varStart, unsigned varLimit, MlirPresburgerVariableKind dstKind); +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationConvertToLocal( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned varStart, unsigned varLimit); + +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationRemoveTrivialEqualities( + MlirPresburgerIntegerRelation relation); + +/// Invert the relation i.e., swap its domain and range. +/// +/// Formally, let the relation `this` be R: A -> B, then this operation +/// modifies R to be B -> A. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationInverse(MlirPresburgerIntegerRelation relation); + +/// Adds a constant bound for the specified variable. +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationAddBound(MlirPresburgerIntegerRelation relation, + MlirPresburgerBoundType type, + unsigned pos, int64_t value); + +/// Adds a constant bound for the specified expression. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationAddBoundExpr( + MlirPresburgerIntegerRelation relation, MlirPresburgerBoundType type, + const int64_t *expr, int64_t exprSize, int64_t value); + +/// Tries to fold the specified variable to a constant using a trivial +/// equality detection; if successful, the constant is substituted for the +/// variable everywhere in the constraint system and then removed from the +/// system. +MLIR_CAPI_EXPORTED MlirLogicalResult +mlirPresburgerIntegerRelationConstantFoldVar( + MlirPresburgerIntegerRelation relation, unsigned pos); + +/// This method calls `constantFoldVar` for the specified range of variables, +/// `num` variables starting at position `pos`. +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationConstantFoldVarRange( + MlirPresburgerIntegerRelation relation, unsigned pos, unsigned num); + +//===----------------------------------------------------------------------===// +// IntegerRelation Dump +//===----------------------------------------------------------------------===// +MLIR_CAPI_EXPORTED void +mlirPresburgerIntegerRelationDump(MlirPresburgerIntegerRelation relation); + +#ifdef __cplusplus +} +#endif +#endif // MLIR_C_PRESBURGER_H \ No newline at end of file diff --git a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h index a27fc8c37eeda..b58e2be164ec8 100644 --- a/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h +++ b/mlir/include/mlir/Analysis/Presburger/IntegerRelation.h @@ -753,6 +753,15 @@ class IntegerRelation { // false. bool isFullDim(); + void *getAsOpaquePointer() const { + return const_cast(this); + } + + static IntegerRelation *getFromOpaquePointer(const void *pointer) { + return const_cast( + reinterpret_cast(pointer)); + } + void print(raw_ostream &os) const; void dump() const; diff --git a/mlir/include/mlir/CAPI/Presburger.h b/mlir/include/mlir/CAPI/Presburger.h new file mode 100644 index 0000000000000..8d9a2d59a31a6 --- /dev/null +++ b/mlir/include/mlir/CAPI/Presburger.h @@ -0,0 +1,25 @@ +//===- Presburger.h - C API Utils for Presburger library --------*- 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 +// +//===----------------------------------------------------------------------===// +// +// This file contains declarations of implementation details of the C API for +// Presburger library. This file should not be included from C++ code other than +// C API implementation nor from C code. +// +//===----------------------------------------------------------------------===// + +#ifndef MLIR_CAPI_PRESBURGER_H +#define MLIR_CAPI_PRESBURGER_H + +#include "mlir-c/Presburger.h" +#include "mlir/Analysis/Presburger/IntegerRelation.h" +#include "mlir/CAPI/Wrap.h" + +DEFINE_C_API_PTR_METHODS(MlirPresburgerIntegerRelation, + mlir::presburger::IntegerRelation) + +#endif /* MLIR_CAPI_PRESBURGER_H */ \ No newline at end of file diff --git a/mlir/lib/Bindings/Python/Presburger.cpp b/mlir/lib/Bindings/Python/Presburger.cpp new file mode 100644 index 0000000000000..504b8bb9756d2 --- /dev/null +++ b/mlir/lib/Bindings/Python/Presburger.cpp @@ -0,0 +1,767 @@ +//===- Presburger.cpp - Presburger library --------------------------------===// +// +// 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 +// +//===----------------------------------------------------------------------===// + +#include "mlir-c/Presburger.h" +#include "mlir-c/Bindings/Python/Interop.h" +#include "llvm/ADT/ScopeExit.h" +#include +#include + +namespace py = pybind11; + +static bool isSignedIntegerFormat(std::string_view format) { + if (format.empty()) + return false; + char code = format[0]; + return code == 'i' || code == 'b' || code == 'h' || code == 'l' || + code == 'q'; +} + +namespace { +struct PyPresburgerIntegerRelation { + PyPresburgerIntegerRelation(MlirPresburgerIntegerRelation relation) + : relation(relation) {} + PyPresburgerIntegerRelation(const PyPresburgerIntegerRelation &other) = + default; + PyPresburgerIntegerRelation(PyPresburgerIntegerRelation &&other) noexcept + : relation(other.relation) { + other.relation.ptr = nullptr; + } + virtual ~PyPresburgerIntegerRelation() { + if (relation.ptr) { + mlirPresburgerIntegerRelationDestroy(relation); + relation.ptr = {nullptr}; + } + } + static std::unique_ptr + getFromNumConstrainsAndVars(uint64_t numReservedInequalities, + uint64_t numReservedEqualities, + uint64_t numReservedCols); + static std::unique_ptr + getFromBuffers(py::buffer inequalitiesCoefficients, + py::buffer equalityCoefficients, unsigned numDomainVars, + unsigned numRangeVars); + py::object getCapsule(); + static void bind(py::module &module); + MlirPresburgerIntegerRelation relation{nullptr}; +}; + +/// A utility that enables accessing/modifying the underlying coefficients +/// easier. +struct PyPresburgerTableau { + enum class Kind { Equalities, Inequalities }; + PyPresburgerTableau(MlirPresburgerIntegerRelation relation, Kind kind) + : relation(relation), kind(kind) {} + static void bind(py::module &module); + int64_t at64(int64_t row, int64_t col) const { + if (kind == Kind::Equalities) + return mlirPresburgerIntegerRelationAtEq64(relation, row, col); + return mlirPresburgerIntegerRelationAtIneq64(relation, row, col); + } + MlirPresburgerIntegerRelation relation; + Kind kind; +}; + +struct PyPresburgerMaybeOptimum { + PyPresburgerMaybeOptimum(MlirMaybeOptimum optimum) + : kind(optimum.kind), integerPoint(optimum.vector.data), + integerPointSize(optimum.vector.size) {} + ~PyPresburgerMaybeOptimum() { + if (integerPoint) { + delete[] integerPoint; + integerPoint = nullptr; + } + } + static void bind(py::module &module); + MlirPresburgerOptimumKind kind; + const int64_t *integerPoint{nullptr}; + int64_t integerPointSize; +}; +} // namespace + +std::unique_ptr +PyPresburgerIntegerRelation::getFromBuffers(py::buffer inequalitiesCoefficients, + py::buffer equalityCoefficients, + unsigned numDomainVars, + unsigned numRangeVars) { + // Request a contiguous view. In exotic cases, this will cause a copy. + int flags = PyBUF_ND; + flags |= PyBUF_FORMAT; + // Get the view of the inequality coefficients. + std::unique_ptr ineqView = std::make_unique(); + if (PyObject_GetBuffer(inequalitiesCoefficients.ptr(), ineqView.get(), + flags) != 0) + throw py::error_already_set(); + auto freeIneqBuffer = llvm::make_scope_exit([&]() { + if (ineqView) + PyBuffer_Release(ineqView.get()); + }); + if (!PyBuffer_IsContiguous(ineqView.get(), 'A')) + throw std::invalid_argument("Contiguous buffer is required."); + if (!isSignedIntegerFormat(ineqView->format) || ineqView->itemsize != 8) + throw std::invalid_argument( + std::string("IntegerRelation can only be created from a buffer of " + "i64 values but got buffer with format: ") + + std::string(ineqView->format)); + if (ineqView->ndim != 2) + throw std::invalid_argument( + std::string("expected 2d inequality coefficients but got rank ") + + std::to_string(ineqView->ndim)); + unsigned numInequalities = ineqView->shape[0]; + // Get the view of the eequality coefficients. + std::unique_ptr eqView = std::make_unique(); + if (PyObject_GetBuffer(equalityCoefficients.ptr(), eqView.get(), flags) != 0) + throw py::error_already_set(); + auto freeEqBuffer = llvm::make_scope_exit([&]() { + if (eqView) + PyBuffer_Release(eqView.get()); + }); + if (!PyBuffer_IsContiguous(eqView.get(), 'A')) + throw std::invalid_argument("Contiguous buffer is required."); + if (!isSignedIntegerFormat(eqView->format) || eqView->itemsize != 8) + throw std::invalid_argument( + std::string("IntegerRelation can only be created from a buffer of " + "i64 values but got buffer with format: ") + + std::string(eqView->format)); + if (eqView->ndim != 2) + throw std::invalid_argument( + std::string("expected 2d equality coefficients but got rank ") + + std::to_string(eqView->ndim)); + unsigned numEqualities = eqView->shape[0]; + if (eqView->shape[1] != numDomainVars + numRangeVars + 1 || + eqView->shape[1] != ineqView->shape[1]) + throw std::invalid_argument( + "expected number of columns of inequality and equality coefficient " + "matrices to equal numRangeVars + numDomainVars + 1"); + MlirPresburgerIntegerRelation relation = + mlirPresburgerIntegerRelationCreateFromCoefficients( + reinterpret_cast(ineqView->buf), numInequalities, + reinterpret_cast(eqView->buf), numEqualities, + numDomainVars, numRangeVars); + return std::make_unique(relation); +} + +std::unique_ptr +PyPresburgerIntegerRelation::getFromNumConstrainsAndVars( + uint64_t numReservedInequalities, uint64_t numReservedEqualities, + uint64_t numReservedCols) { + MlirPresburgerIntegerRelation relation = mlirPresburgerIntegerRelationCreate( + numReservedInequalities, numReservedEqualities, numReservedCols); + return std::make_unique(relation); +} + +py::object PyPresburgerIntegerRelation::getCapsule() { + throw std::invalid_argument("unimplemented"); +} + +void PyPresburgerTableau::bind(py::module &m) { + py::class_(m, "IntegerRelationTableau", + py::module_local()) + .def("__getitem__", [](PyPresburgerTableau &self, + const py::tuple &index) { + return self.at64(index[0].cast(), index[1].cast()); + }); +} + +void PyPresburgerMaybeOptimum::bind(py::module &m) { + py::class_(m, "IntegerRelationMaybeOptimum", + py::module_local()) + .def("is_empty", + [](PyPresburgerMaybeOptimum &self) { + return self.kind == MlirPresburgerOptimumKind::Empty; + }) + .def("is_unbounded", + [](PyPresburgerMaybeOptimum &self) { + return self.kind == MlirPresburgerOptimumKind::Unbounded; + }) + .def("is_bounded", + [](PyPresburgerMaybeOptimum &self) { + return self.kind == MlirPresburgerOptimumKind::Bounded; + }) + .def("get_integer_point", [](PyPresburgerMaybeOptimum &self) { + if (self.kind != MlirPresburgerOptimumKind::Bounded) + return std::vector(); + std::vector r{self.integerPoint, + self.integerPoint + self.integerPointSize}; + return r; + }); +} + +void PyPresburgerIntegerRelation::bind(py::module &m) { + py::class_(m, "IntegerRelation", + py::module_local()) + .def(py::init<>(&PyPresburgerIntegerRelation::getFromBuffers), + py::arg("inequalities_coefficients"), + py::arg("equalities_coefficients"), py::arg("num_domain_vars"), + py::arg("num_range_vars")) + .def( + py::init<>(&PyPresburgerIntegerRelation::getFromNumConstrainsAndVars), + py::arg("num_reserved_inequalities"), + py::arg("num_reserved_equalities"), py::arg("num_reserved_cols")) + .def_property_readonly(MLIR_PYTHON_CAPI_PTR_ATTR, + &PyPresburgerIntegerRelation::getCapsule) + .def("__eq__", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationIsEqual(self.relation, + other.relation); + }) + .def( + "append", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationAppend(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "intersect", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + PyPresburgerIntegerRelation intersection( + mlirPresburgerIntegerRelationIntersect(self.relation, + other.relation)); + return intersection; + }, + py::arg("other")) + .def( + "is_equal", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationIsEqual(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "is_obviously_equal", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationIsObviouslyEqual( + self.relation, other.relation); + }, + py::arg("other")) + .def( + "is_subset_of", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationIsSubsetOf(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "merge_and_align_symbols", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationMergeAndAlignSymbols( + self.relation, other.relation); + }, + py::arg("other")) + .def( + "merge_local_vars", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationMergeLocalVars(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "compose", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationCompose(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "apply_domain", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationApplyDomain(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "apply_range", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationApplyRange(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "merge_and_composite", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + return mlirPresburgerIntegerRelationMergeAndCompose(self.relation, + other.relation); + }, + py::arg("other")) + .def( + "union_bounding_box", + [](PyPresburgerIntegerRelation &self, + PyPresburgerIntegerRelation &other) { + auto r = mlirPresburgerIntegerRelationUnionBoundingBox( + self.relation, other.relation); + return mlirLogicalResultIsSuccess(r); + }, + py::arg("other")) + .def( + "inequalities", + [](PyPresburgerIntegerRelation &self) { + PyPresburgerTableau tableau( + self.relation, PyPresburgerTableau::Kind::Inequalities); + return tableau; + }, + py::keep_alive<0, 1>()) + .def( + "equalities", + [](PyPresburgerIntegerRelation &self) { + PyPresburgerTableau tableau(self.relation, + PyPresburgerTableau::Kind::Equalities); + return tableau; + }, + py::keep_alive<0, 1>()) + .def("get_equality", + [](PyPresburgerIntegerRelation &self, int64_t row) { + unsigned numCol = + mlirPresburgerIntegerRelationNumCols(self.relation); + std::vector result(numCol); + for (unsigned i = 0; i < numCol; i++) + result[i] = + mlirPresburgerIntegerRelationAtEq64(self.relation, row, i); + return result; + }) + .def("get_inequality", + [](PyPresburgerIntegerRelation &self, int64_t row) { + unsigned numCol = + mlirPresburgerIntegerRelationNumCols(self.relation); + std::vector result(numCol); + for (unsigned i = 0; i < numCol; i++) + result[i] = + mlirPresburgerIntegerRelationAtIneq64(self.relation, row, i); + return result; + }) + .def( + "get_num_vars_of_kind", + [](PyPresburgerIntegerRelation &self, + MlirPresburgerVariableKind kind) { + return mlirPresburgerIntegerRelationGetNumVarKind(self.relation, + kind); + }, + py::arg("kind")) + .def( + "get_var_kind_offset", + [](PyPresburgerIntegerRelation &self, + MlirPresburgerVariableKind kind) { + return mlirPresburgerIntegerRelationGetVarKindOffset(self.relation, + kind); + }, + py::arg("kind")) + .def( + "get_var_kind_end", + [](PyPresburgerIntegerRelation &self, + MlirPresburgerVariableKind kind) { + return mlirPresburgerIntegerRelationGetVarKindEnd(self.relation, + kind); + }, + py::arg("kind")) + .def( + "get_var_kind_overlap", + [](PyPresburgerIntegerRelation &self, MlirPresburgerVariableKind kind, + int64_t varStart, int64_t varLimit) { + return mlirPresburgerIntegerRelationGetVarKindOverLap( + self.relation, kind, varStart, varLimit); + }, + py::arg("kind"), py::arg("start"), py::arg("limit")) + .def( + "get_var_kind_at", + [](PyPresburgerIntegerRelation &self, uint64_t pos) { + return mlirPresburgerIntegerRelationGetVarKindAt(self.relation, + pos); + }, + py::arg("pos")) + .def( + "get_constant_bound", + [](PyPresburgerIntegerRelation &self, MlirPresburgerBoundType type, + uint64_t pos) -> std::optional { + auto r = mlirPresburgerIntegerRelationGetConstantBound64( + self.relation, type, pos); + if (!r.hasValue) + return std::nullopt; + return r.value; + }, + py::arg("bound_type"), py::arg("pos")) + .def("is_full_dim", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationIsFullDim(self.relation); + }) + .def( + "contains_point", + [](PyPresburgerIntegerRelation &self, std::vector &point) { + return mlirPresburgerIntegerRelationContainsPoint( + self.relation, point.data(), point.size()); + }, + py::arg("point")) + .def("has_only_div_locals", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationHasOnlyDivLocals( + self.relation); + }) + .def("remove_trivial_equalities", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationRemoveTrivialEqualities( + self.relation); + }) + .def( + "insert_var", + [](PyPresburgerIntegerRelation &self, MlirPresburgerVariableKind kind, + uint64_t pos, uint64_t num) { + return mlirPresburgerIntegerRelationInsertVar(self.relation, kind, + pos, num); + }, + py::arg("kind"), py::arg("pos"), py::arg("num") = 1) + .def( + "append_var", + [](PyPresburgerIntegerRelation &self, MlirPresburgerVariableKind kind, + uint64_t num) { + return mlirPresburgerIntegerRelationAppendVar(self.relation, kind, + num); + }, + py::arg("kind"), py::arg("num") = 1) + .def( + "add_equality", + [](PyPresburgerIntegerRelation &self, + const std::vector &eq) { + return mlirPresburgerIntegerRelationAddEquality( + self.relation, eq.data(), eq.size()); + }, + py::arg("coefficients")) + .def( + "add_inequality", + [](PyPresburgerIntegerRelation &self, + const std::vector &inEq) { + return mlirPresburgerIntegerRelationAddInequality( + self.relation, inEq.data(), inEq.size()); + }, + py::arg("coefficients")) + .def( + "eliminate_redundant_local_var", + [](PyPresburgerIntegerRelation &self, uint64_t posA, uint64_t posB) { + return mlirPresburgerIntegerRelationEliminateRedundantLocalVar( + self.relation, posA, posB); + }, + py::arg("pos_a"), py::arg("pos_b")) + .def( + "remove_var_of_kind", + [](PyPresburgerIntegerRelation &self, MlirPresburgerVariableKind kind, + uint64_t pos) { + return mlirPresburgerIntegerRelationRemoveVarKind(self.relation, + kind, pos); + }, + py::arg("kind"), py::arg("pos")) + .def( + "remove_var_range_of_kind", + [](PyPresburgerIntegerRelation &self, MlirPresburgerVariableKind kind, + uint64_t varStart, uint64_t varLimit) { + return mlirPresburgerIntegerRelationRemoveVarRangeKind( + self.relation, kind, varStart, varLimit); + }, + py::arg("kind"), py::arg("start"), py::arg("limit")) + .def( + "remove_var", + [](PyPresburgerIntegerRelation &self, uint64_t pos) { + return mlirPresburgerIntegerRelationRemoveVar(self.relation, pos); + }, + py::arg("pos")) + .def( + "remove_equality", + [](PyPresburgerIntegerRelation &self, uint64_t pos) { + return mlirPresburgerIntegerRelationRemoveEquality(self.relation, + pos); + }, + py::arg("pos")) + .def( + "remove_inequality", + [](PyPresburgerIntegerRelation &self, uint64_t pos) { + return mlirPresburgerIntegerRelationRemoveInequality(self.relation, + pos); + }, + py::arg("pos")) + .def( + "remove_equality_range", + [](PyPresburgerIntegerRelation &self, uint64_t start, uint64_t end) { + return mlirPresburgerIntegerRelationRemoveEqualityRange( + self.relation, start, end); + }, + py::arg("start"), py::arg("end")) + .def( + "remove_inequality_range", + [](PyPresburgerIntegerRelation &self, uint64_t start, uint64_t end) { + return mlirPresburgerIntegerRelationRemoveInequalityRange( + self.relation, start, end); + }, + py::arg("start"), py::arg("end")) + .def( + "find_integer_lex_min", + [](PyPresburgerIntegerRelation &self) { + auto r = + mlirPresburgerIntegerRelationFindIntegerLexMin(self.relation); + auto mayBeOptimum = std::make_unique(r); + return mayBeOptimum.release(); + }, + py::return_value_policy::take_ownership) + .def("find_integer_sample", + [](PyPresburgerIntegerRelation &self) + -> std::optional> { + auto r = + mlirPresburgerIntegerRelationFindIntegerSample(self.relation); + if (!r.hasValue) + return std::nullopt; + std::vector integerSample{r.data, r.data + r.size}; + return integerSample; + }) + .def("compute_volume", + [](PyPresburgerIntegerRelation &self) -> std::optional { + auto r = mlirPresburgerIntegerRelationComputeVolume(self.relation); + if (!r.hasValue) + return std::nullopt; + return r.value; + }) + .def( + "swap_var", + [](PyPresburgerIntegerRelation &self, uint64_t posA, uint64_t posB) { + return mlirPresburgerIntegerRelationSwapVar(self.relation, posA, + posB); + }, + py::arg("pos_a"), py::arg("pos_b")) + .def("clear_constraints", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationClearConstraints( + self.relation); + }) + .def( + "set_and_eliminate", + [](PyPresburgerIntegerRelation &self, uint64_t pos, + std::vector &values) { + return mlirPresburgerIntegerRelationSetAndEliminate( + self.relation, pos, values.data(), values.size()); + }, + py::arg("pos"), py::arg("values")) + .def( + "remove_independent_constraints", + [](PyPresburgerIntegerRelation &self, uint64_t pos, uint64_t num) { + return mlirPresburgerIntegerRelationRemoveIndependentConstraints( + self.relation, pos, num); + }, + py::arg("pos"), py::arg("num")) + .def( + "is_hyper_rectangular", + [](PyPresburgerIntegerRelation &self, uint64_t pos, uint64_t num) { + return mlirPresburgerIntegerRelationIsHyperRectangular( + self.relation, pos, num); + }, + py::arg("pos"), py::arg("num")) + .def("remove_trivial_redundancy", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationRemoveTrivialRedundancy( + self.relation); + }) + .def("remove_redundant_inequalities", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationRemoveRedundantInequalities( + self.relation); + }) + .def("remove_redundant_constraints", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationRemoveRedundantConstraints( + self.relation); + }) + .def("remove_duplicate_divs", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationRemoveDuplicateDivs( + self.relation); + }) + .def("simplify", + [](PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationSimplify(self.relation); + }) + .def( + "convert_var_kind", + [](PyPresburgerIntegerRelation &self, + MlirPresburgerVariableKind srcKind, uint64_t vatStart, + uint64_t varLimit, MlirPresburgerVariableKind dstKind, + py::object &pos) { + if (pos.is_none()) + return mlirPresburgerIntegerRelationConvertVarKindNoPos( + self.relation, srcKind, vatStart, varLimit, dstKind); + return mlirPresburgerIntegerRelationConvertVarKind( + self.relation, srcKind, vatStart, varLimit, dstKind, + pos.cast()); + }, + py::arg("src_kind"), py::arg("start"), py::arg("limit"), + py::arg("dst_kind"), py::arg("pos") = py::none()) + .def( + "convert_to_local", + [](PyPresburgerIntegerRelation &self, + MlirPresburgerVariableKind srcKind, uint64_t vatStart, + uint64_t varLimit) { + return mlirPresburgerIntegerRelationConvertVarKindNoPos( + self.relation, srcKind, vatStart, varLimit, + MlirPresburgerVariableKind::Local); + }, + py::arg("src_kind"), py::arg("start"), py::arg("limit")) + .def( + "add_bound", + [](PyPresburgerIntegerRelation &self, MlirPresburgerBoundType type, + uint64_t pos, int64_t value) { + return mlirPresburgerIntegerRelationAddBound(self.relation, type, + pos, value); + }, + py::arg("bound_type"), py::arg("pos"), py::arg("value")) + .def( + "add_bound", + [](PyPresburgerIntegerRelation &self, MlirPresburgerBoundType type, + std::vector &expr, int64_t value) { + return mlirPresburgerIntegerRelationAddBoundExpr( + self.relation, type, expr.data(), expr.size(), value); + }, + py::arg("bound_type"), py::arg("expr"), py::arg("value")) + .def( + "constant_fold_var", + [](PyPresburgerIntegerRelation &self, uint64_t pos) { + auto r = mlirPresburgerIntegerRelationConstantFoldVar(self.relation, + pos); + return mlirLogicalResultIsSuccess(r); + }, + py::arg("pos")) + .def( + "constant_fold_var_range", + [](PyPresburgerIntegerRelation &self, uint64_t pos, uint64_t num) { + return mlirPresburgerIntegerRelationConstantFoldVarRange( + self.relation, pos, num); + }, + py::arg("pos"), py::arg("num")) + .def_property_readonly( + "at_eq", + [](PyPresburgerIntegerRelation &self) { + return PyPresburgerTableau(self.relation, + PyPresburgerTableau::Kind::Equalities); + }, + py::return_value_policy::reference_internal) + .def_property_readonly( + "at_ineq", + [](PyPresburgerIntegerRelation &self) { + return PyPresburgerTableau(self.relation, + PyPresburgerTableau::Kind::Inequalities); + }, + py::return_value_policy::reference_internal) + .def_property_readonly( + "num_constraints", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumConstraints(self.relation); + }) + .def_property_readonly( + "num_domain_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumDomainVars(self.relation); + }) + .def_property_readonly("num_range_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumRangeVars( + self.relation); + }) + .def_property_readonly( + "num_symbol_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumSymbolVars(self.relation); + }) + .def_property_readonly("num_local_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumLocalVars( + self.relation); + }) + .def_property_readonly("num_dim_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumDimVars( + self.relation); + }) + .def_property_readonly( + "num_dim_and_symbol_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumDimAndSymbolVars( + self.relation); + }) + .def_property_readonly("num_vars", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumVars( + self.relation); + }) + .def_property_readonly("num_columns", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumCols( + self.relation); + }) + .def_property_readonly( + "num_equalities", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumEqualities(self.relation); + }) + .def_property_readonly( + "num_inequalities", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumInequalities(self.relation); + }) + .def_property_readonly( + "num_reserved_equalities", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumReservedEqualities( + self.relation); + }) + .def_property_readonly( + "num_reserved_inequalities", + [](const PyPresburgerIntegerRelation &self) { + return mlirPresburgerIntegerRelationNumReservedInequalities( + self.relation); + }) + .def("__str__", [](const PyPresburgerIntegerRelation &self) { + mlirPresburgerIntegerRelationDump(self.relation); + return ""; + }); +} + +static inline void populateVarKindEnum(py::module &m) { + py::enum_(m, "VariableKind", py::module_local()) + .value("Symbol", MlirPresburgerVariableKind::Symbol) + .value("Local", MlirPresburgerVariableKind::Local) + .value("Domain", MlirPresburgerVariableKind::Domain) + .value("Range", MlirPresburgerVariableKind::Range) + .export_values(); +} + +static inline void populateBoundTypeEnum(py::module &m) { + py::enum_(m, "BoundType", py::module_local()) + .value("EQ", MlirPresburgerBoundType::EQ) + .value("LB", MlirPresburgerBoundType::LB) + .value("UB", MlirPresburgerBoundType::UB) + .export_values(); +} + +static void populatePresburgerModule(py::module &m) { + populateVarKindEnum(m); + populateBoundTypeEnum(m); + PyPresburgerTableau::bind(m); + PyPresburgerMaybeOptimum::bind(m); + PyPresburgerIntegerRelation::bind(m); +} +// ----------------------------------------------------------------------------- +// Module initialization. +// ----------------------------------------------------------------------------- +PYBIND11_MODULE(_mlirPresburger, m) { + m.doc() = "MLIR Presburger utilities"; + populatePresburgerModule(m); +} \ No newline at end of file diff --git a/mlir/lib/CAPI/CMakeLists.txt b/mlir/lib/CAPI/CMakeLists.txt index 6c438508425b7..56888798e9229 100644 --- a/mlir/lib/CAPI/CMakeLists.txt +++ b/mlir/lib/CAPI/CMakeLists.txt @@ -15,6 +15,7 @@ add_subdirectory(IR) add_subdirectory(RegisterEverything) add_subdirectory(Transforms) add_subdirectory(Target) +add_subdirectory(Presburger) if(MLIR_ENABLE_EXECUTION_ENGINE) add_subdirectory(ExecutionEngine) diff --git a/mlir/lib/CAPI/Presburger/CMakeLists.txt b/mlir/lib/CAPI/Presburger/CMakeLists.txt new file mode 100644 index 0000000000000..956006233dda5 --- /dev/null +++ b/mlir/lib/CAPI/Presburger/CMakeLists.txt @@ -0,0 +1,6 @@ +add_mlir_upstream_c_api_library(MLIRCAPIPresburger + Presburger.cpp + + LINK_LIBS PUBLIC + MLIRPresburger + ) \ No newline at end of file diff --git a/mlir/lib/CAPI/Presburger/Presburger.cpp b/mlir/lib/CAPI/Presburger/Presburger.cpp new file mode 100644 index 0000000000000..06ea5d50bc230 --- /dev/null +++ b/mlir/lib/CAPI/Presburger/Presburger.cpp @@ -0,0 +1,499 @@ +//===- Presburger.cpp - C Interface for Presburger library ----------------===// +// +// 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 +// +//===----------------------------------------------------------------------===// + +#include "mlir/CAPI/Presburger.h" +#include "mlir-c/Presburger.h" +#include "mlir-c/Support.h" +#include "mlir/Analysis/Presburger/IntegerRelation.h" + +using namespace mlir; +using namespace mlir::presburger; + +//===----------------------------------------------------------------------===// +// IntegerRelation creation/destruction and basic metadata operations +//===----------------------------------------------------------------------===// + +MlirPresburgerIntegerRelation +mlirPresburgerIntegerRelationCreate(unsigned numReservedInequalities, + unsigned numReservedEqualities, + unsigned numReservedCols) { + auto space = PresburgerSpace::getRelationSpace(); + IntegerRelation *relation = new IntegerRelation( + numReservedInequalities, numReservedEqualities, numReservedCols, space); + return wrap(relation); +} + +MlirPresburgerIntegerRelation +mlirPresburgerIntegerRelationCreateFromCoefficients( + const int64_t *inequalityCoefficients, unsigned numInequalities, + const int64_t *equalityCoefficients, unsigned numEqualities, + unsigned numDomainVars, unsigned numRangeVars, + unsigned numExtraReservedInequalities, unsigned numExtraReservedEqualities, + unsigned numExtraReservedCols) { + auto space = PresburgerSpace::getRelationSpace(numDomainVars, numRangeVars); + IntegerRelation *relation = + new IntegerRelation(numInequalities + numExtraReservedInequalities, + numEqualities + numExtraReservedInequalities, + numDomainVars + numRangeVars + 1, space); + unsigned numCols = numRangeVars + numDomainVars + 1; + for (const int64_t *rowPtr = inequalityCoefficients; + rowPtr < inequalityCoefficients + numCols * numInequalities; + rowPtr += numCols) { + llvm::ArrayRef coef(rowPtr, rowPtr + numCols); + relation->addInequality(coef); + } + for (const int64_t *rowPtr = equalityCoefficients; + rowPtr < equalityCoefficients + numCols * numEqualities; + rowPtr += numCols) { + llvm::ArrayRef coef(rowPtr, rowPtr + numCols); + relation->addEquality(coef); + } + return wrap(relation); +} + +void mlirPresburgerIntegerRelationDestroy( + MlirPresburgerIntegerRelation relation) { + if (relation.ptr) + delete reinterpret_cast(relation.ptr); +} + +//===----------------------------------------------------------------------===// +// IntegerRelation binary operations +//===----------------------------------------------------------------------===// + +void mlirPresburgerIntegerRelationAppend(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->append(*unwrap(rhs)); +} + +MlirPresburgerIntegerRelation +mlirPresburgerIntegerRelationIntersect(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs) { + auto result = + std::make_unique(unwrap(lhs)->intersect(*(unwrap(rhs)))); + return wrap(result.release()); +} + +bool mlirPresburgerIntegerRelationIsEqual(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->isEqual(*(unwrap(rhs))); +} + +bool mlirPresburgerIntegerRelationIsObviouslyEqual( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->isObviouslyEqual(*(unwrap(rhs))); +} + +bool mlirPresburgerIntegerRelationIsSubsetOf( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->isSubsetOf(*(unwrap(rhs))); +} + +void mlirPresburgerIntegerRelationCompose(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->compose(*unwrap(rhs)); +} + +void mlirPresburgerIntegerRelationApplyDomain( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->applyDomain(*unwrap(rhs)); +} + +void mlirPresburgerIntegerRelationApplyRange( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->applyRange(*unwrap(rhs)); +} + +void mlirPresburgerIntegerRelationMergeAndCompose( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->mergeAndCompose(*unwrap(rhs)); +} + +void mlirPresburgerIntegerRelationMergeAndAlignSymbols( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->mergeAndAlignSymbols(*unwrap(rhs)); +} + +unsigned +mlirPresburgerIntegerRelationMergeLocalVars(MlirPresburgerIntegerRelation lhs, + MlirPresburgerIntegerRelation rhs) { + return unwrap(lhs)->mergeLocalVars(*unwrap(rhs)); +} + +MlirLogicalResult mlirPresburgerIntegerRelationUnionBoundingBox( + MlirPresburgerIntegerRelation lhs, MlirPresburgerIntegerRelation rhs) { + auto r = unwrap(lhs)->unionBoundingBox(*unwrap(rhs)); + if (failed(r)) + return MlirLogicalResult{0}; + return MlirLogicalResult{1}; +} + +//===----------------------------------------------------------------------===// +// IntegerRelation Tableau Inspection +//===----------------------------------------------------------------------===// + +unsigned mlirPresburgerIntegerRelationNumConstraints( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumConstraints(); +} + +unsigned mlirPresburgerIntegerRelationNumDomainVars( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumDomainVars(); +} + +unsigned mlirPresburgerIntegerRelationNumRangeVars( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumRangeVars(); +} + +unsigned mlirPresburgerIntegerRelationNumSymbolVars( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumSymbolVars(); +} + +unsigned mlirPresburgerIntegerRelationNumLocalVars( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumLocalVars(); +} + +unsigned mlirPresburgerIntegerRelationNumDimVars( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumDimVars(); +} + +unsigned mlirPresburgerIntegerRelationNumDimAndSymbolVars( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumDimAndSymbolVars(); +} + +unsigned +mlirPresburgerIntegerRelationNumVars(MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumVars(); +} + +unsigned +mlirPresburgerIntegerRelationNumCols(MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumCols(); +} + +unsigned mlirPresburgerIntegerRelationNumEqualities( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumEqualities(); +} + +unsigned mlirPresburgerIntegerRelationNumInequalities( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumInequalities(); +} + +unsigned mlirPresburgerIntegerRelationNumReservedEqualities( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumReservedEqualities(); +} + +unsigned mlirPresburgerIntegerRelationNumReservedInequalities( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->getNumReservedInequalities(); +} + +int64_t +mlirPresburgerIntegerRelationAtEq64(MlirPresburgerIntegerRelation relation, + unsigned row, unsigned col) { + return unwrap(relation)->atEq64(row, col); +} + +int64_t +mlirPresburgerIntegerRelationAtIneq64(MlirPresburgerIntegerRelation relation, + unsigned row, unsigned col) { + return unwrap(relation)->atIneq64(row, col); +} + +unsigned mlirPresburgerIntegerRelationGetNumVarKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind) { + return unwrap(relation)->getNumVarKind(static_cast(kind)); +} + +unsigned mlirPresburgerIntegerRelationGetVarKindOffset( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind) { + return unwrap(relation)->getVarKindOffset(static_cast(kind)); +} + +unsigned mlirPresburgerIntegerRelationGetVarKindEnd( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind) { + return unwrap(relation)->getVarKindEnd(static_cast(kind)); +} + +unsigned mlirPresburgerIntegerRelationGetVarKindOverLap( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned varStart, unsigned varLimit) { + return unwrap(relation)->getVarKindOverlap(static_cast(kind), + varStart, varLimit); +} + +MlirPresburgerVariableKind mlirPresburgerIntegerRelationGetVarKindAt( + MlirPresburgerIntegerRelation relation, unsigned pos) { + return static_cast( + unwrap(relation)->getVarKindAt(pos)); +} + +MlirOptionalInt64 mlirPresburgerIntegerRelationGetConstantBound64( + MlirPresburgerIntegerRelation relation, MlirPresburgerBoundType type, + unsigned pos) { + auto r = + unwrap(relation)->getConstantBound64(static_cast(type), pos); + if (r.has_value()) + return MlirOptionalInt64{true, *r}; + return MlirOptionalInt64{false, -1}; +} + +bool mlirPresburgerIntegerRelationHasOnlyDivLocals( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->hasOnlyDivLocals(); +} + +bool mlirPresburgerIntegerRelationIsFullDim( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->isFullDim(); +} + +MlirMaybeOptimum mlirPresburgerIntegerRelationFindIntegerLexMin( + MlirPresburgerIntegerRelation relation) { + auto r = unwrap(relation)->findIntegerLexMin(); + if (r.isEmpty()) { + return MlirMaybeOptimum{MlirPresburgerOptimumKind::Empty, + {false, nullptr, 8}}; + } + if (r.isUnbounded()) + return MlirMaybeOptimum{MlirPresburgerOptimumKind::Unbounded, + {false, nullptr, 8}}; + int64_t *integerPoint = std::make_unique(8).release(); + std::transform((*r).begin(), (*r).end(), integerPoint, int64fromDynamicAPInt); + return MlirMaybeOptimum{MlirPresburgerOptimumKind::Bounded, + {true, integerPoint, 8}}; +} + +MlirOptionalVectorInt64 mlirPresburgerIntegerRelationFindIntegerSample( + MlirPresburgerIntegerRelation relation) { + auto r = unwrap(relation)->findIntegerSample(); + if (!r.has_value()) + return MlirOptionalVectorInt64{false, nullptr, 8}; + int64_t *integerPoint = std::make_unique(8).release(); + std::transform((*r).begin(), (*r).end(), integerPoint, int64fromDynamicAPInt); + return MlirOptionalVectorInt64{true, integerPoint, 8}; +} + +MlirOptionalInt64 mlirPresburgerIntegerRelationComputeVolume( + MlirPresburgerIntegerRelation relation) { + auto r = unwrap(relation)->computeVolume(); + if (!r.has_value()) + return MlirOptionalInt64{false, -1}; + return MlirOptionalInt64{true, int64fromDynamicAPInt(*r)}; +} + +bool mlirPresburgerIntegerRelationContainsPoint( + MlirPresburgerIntegerRelation relation, const int64_t *point, + int64_t size) { + return unwrap(relation)->containsPoint( + ArrayRef(point, point + size)); +} + +//===----------------------------------------------------------------------===// +// IntegerRelation Tableau Manipulation +//===----------------------------------------------------------------------===// + +unsigned +mlirPresburgerIntegerRelationInsertVar(MlirPresburgerIntegerRelation relation, + MlirPresburgerVariableKind kind, + unsigned pos, unsigned num) { + return unwrap(relation)->insertVar(static_cast(kind), pos, num); +} + +unsigned +mlirPresburgerIntegerRelationAppendVar(MlirPresburgerIntegerRelation relation, + MlirPresburgerVariableKind kind, + unsigned num) { + return unwrap(relation)->appendVar(static_cast(kind), num); +} + +void mlirPresburgerIntegerRelationAddEquality( + MlirPresburgerIntegerRelation relation, const int64_t *coeff, + int64_t coeffSize) { + unwrap(relation)->addEquality(ArrayRef(coeff, coeff + coeffSize)); +} + +/// Adds an inequality with the given coefficients. +void mlirPresburgerIntegerRelationAddInequality( + MlirPresburgerIntegerRelation relation, const int64_t *coeff, + int64_t coeffSize) { + unwrap(relation)->addInequality(ArrayRef(coeff, coeff + coeffSize)); +} + +void mlirPresburgerIntegerRelationEliminateRedundantLocalVar( + MlirPresburgerIntegerRelation relation, unsigned posA, unsigned posB) { + return unwrap(relation)->eliminateRedundantLocalVar(posA, posB); +} + +void mlirPresburgerIntegerRelationRemoveVarKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned pos) { + return unwrap(relation)->removeVar(static_cast(kind), pos); +} + +void mlirPresburgerIntegerRelationRemoveVarRangeKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned varStart, unsigned varLimit) { + return unwrap(relation)->removeVarRange(static_cast(kind), varStart, + varLimit); +} + +void mlirPresburgerIntegerRelationRemoveVar( + MlirPresburgerIntegerRelation relation, unsigned pos) { + return unwrap(relation)->removeVar(pos); +} + +void mlirPresburgerIntegerRelationRemoveEquality( + MlirPresburgerIntegerRelation relation, unsigned pos) { + return unwrap(relation)->removeEquality(pos); +} + +void mlirPresburgerIntegerRelationRemoveInequality( + MlirPresburgerIntegerRelation relation, unsigned pos) { + return unwrap(relation)->removeInequality(pos); +} + +void mlirPresburgerIntegerRelationRemoveEqualityRange( + MlirPresburgerIntegerRelation relation, unsigned start, unsigned end) { + return unwrap(relation)->removeEqualityRange(start, end); +} + +void mlirPresburgerIntegerRelationRemoveInequalityRange( + MlirPresburgerIntegerRelation relation, unsigned start, unsigned end) { + return unwrap(relation)->removeInequalityRange(start, end); +} + +void mlirPresburgerIntegerRelationSwapVar( + MlirPresburgerIntegerRelation relation, unsigned posA, unsigned posB) { + return unwrap(relation)->swapVar(posA, posB); +} + +void mlirPresburgerIntegerRelationClearConstraints( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->clearConstraints(); +} + +/// Sets the `values.size()` variables starting at `po`s to the specified +/// values and removes them. +void mlirPresburgerIntegerRelationSetAndEliminate( + MlirPresburgerIntegerRelation relation, unsigned pos, const int64_t *values, + unsigned valuesSize) { + return unwrap(relation)->setAndEliminate( + pos, ArrayRef(values, values + valuesSize)); +} + +void mlirPresburgerIntegerRelationRemoveIndependentConstraints( + MlirPresburgerIntegerRelation relation, unsigned pos, unsigned num) { + return unwrap(relation)->removeIndependentConstraints(pos, num); +} + +bool mlirPresburgerIntegerRelationIsHyperRectangular( + MlirPresburgerIntegerRelation relation, unsigned pos, unsigned num) { + return unwrap(relation)->isHyperRectangular(pos, num); +} + +void mlirPresburgerIntegerRelationRemoveTrivialRedundancy( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->removeTrivialRedundancy(); +} + +void mlirPresburgerIntegerRelationRemoveRedundantInequalities( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->removeRedundantInequalities(); +} + +void mlirPresburgerIntegerRelationRemoveRedundantConstraints( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->removeRedundantConstraints(); +} + +void mlirPresburgerIntegerRelationRemoveDuplicateDivs( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->removeDuplicateDivs(); +} + +void mlirPresburgerIntegerRelationSimplify( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->simplify(); +} + +void mlirPresburgerIntegerRelationConvertVarKind( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind srcKind, + unsigned varStart, unsigned varLimit, MlirPresburgerVariableKind dstKind, + unsigned pos) { + return unwrap(relation)->convertVarKind(static_cast(srcKind), + varStart, varLimit, + static_cast(dstKind), pos); +} +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationConvertVarKindNoPos( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind srcKind, + unsigned varStart, unsigned varLimit, MlirPresburgerVariableKind dstKind) { + mlirPresburgerIntegerRelationConvertVarKind( + relation, srcKind, varStart, varLimit, dstKind, + mlirPresburgerIntegerRelationGetNumVarKind(relation, dstKind)); +} +MLIR_CAPI_EXPORTED void mlirPresburgerIntegerRelationConvertToLocal( + MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind, + unsigned varStart, unsigned varLimit) { + mlirPresburgerIntegerRelationConvertVarKindNoPos( + relation, kind, varStart, varLimit, MlirPresburgerVariableKind::Local); +} + +void mlirPresburgerIntegerRelationInverse( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->inverse(); +} + +void mlirPresburgerIntegerRelationRemoveTrivialEqualities( + MlirPresburgerIntegerRelation relation) { + return unwrap(relation)->removeTrivialEqualities(); +} + +void mlirPresburgerIntegerRelationAddBound( + MlirPresburgerIntegerRelation relation, MlirPresburgerBoundType type, + unsigned pos, int64_t value) { + return unwrap(relation)->addBound(static_cast(type), pos, value); +} + +void mlirPresburgerIntegerRelationAddBoundExpr( + MlirPresburgerIntegerRelation relation, MlirPresburgerBoundType type, + const int64_t *expr, int64_t exprSize, int64_t value) { + return unwrap(relation)->addBound(static_cast(type), + ArrayRef(expr, expr + exprSize), + value); +} + +MlirLogicalResult mlirPresburgerIntegerRelationConstantFoldVar( + MlirPresburgerIntegerRelation relation, unsigned pos) { + auto r = unwrap(relation)->constantFoldVar(pos); + if (failed(r)) + return MlirLogicalResult{0}; + return MlirLogicalResult{1}; +} + +void mlirPresburgerIntegerRelationConstantFoldVarRange( + MlirPresburgerIntegerRelation relation, unsigned pos, unsigned num) { + return unwrap(relation)->constantFoldVarRange(pos, num); +} + +//===----------------------------------------------------------------------===// +// IntegerRelation Dump +//===----------------------------------------------------------------------===// + +void mlirPresburgerIntegerRelationDump(MlirPresburgerIntegerRelation relation) { + unwrap(relation)->dump(); +} \ No newline at end of file diff --git a/mlir/python/CMakeLists.txt b/mlir/python/CMakeLists.txt index 23187f256455b..f47cbddc7e371 100644 --- a/mlir/python/CMakeLists.txt +++ b/mlir/python/CMakeLists.txt @@ -48,6 +48,13 @@ declare_mlir_python_sources(MLIRPythonSources.ExecutionEngine runtime/*.py ) +declare_mlir_python_sources(MLIRPythonSources.Presburger + ROOT_DIR "${CMAKE_CURRENT_SOURCE_DIR}/mlir" + ADD_TO_PARENT MLIRPythonSources + SOURCES + presburger.py + ) + declare_mlir_python_sources(MLIRPythonCAPI.HeaderSources ROOT_DIR "${MLIR_SOURCE_DIR}/include" SOURCES_GLOB "mlir-c/*.h" @@ -666,6 +673,18 @@ declare_mlir_python_extension(MLIRPythonExtension.TransformInterpreter MLIRCAPITransformDialectTransforms ) +declare_mlir_python_extension(MLIRPythonExtension.Presburger + MODULE_NAME _mlirPresburger + ADD_TO_PARENT MLIRPythonSources.Presburger + ROOT_DIR "${PYTHON_SOURCE_DIR}" + SOURCES + Presburger.cpp + PRIVATE_LINK_LIBS + LLVMSupport + EMBED_CAPI_LINK_LIBS + MLIRCAPIPresburger +) + # TODO: Figure out how to put this in the test tree. # This should not be included in the main Python extension. However, # putting it into MLIRPythonTestSources along with the dialect declaration diff --git a/mlir/python/mlir/presburger.py b/mlir/python/mlir/presburger.py new file mode 100644 index 0000000000000..f4235c4ed75d5 --- /dev/null +++ b/mlir/python/mlir/presburger.py @@ -0,0 +1,6 @@ +# 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 + +# Simply a wrapper around the extension module of the same name. +from ._mlir_libs._mlirPresburger import * \ No newline at end of file diff --git a/mlir/test/python/presburger.py b/mlir/test/python/presburger.py new file mode 100644 index 0000000000000..290ae9badc9aa --- /dev/null +++ b/mlir/test/python/presburger.py @@ -0,0 +1,108 @@ +from mlir import presburger +import numpy as np + +""" +Test the following integer relation + +x + 2y = 8 +x - y <= 1 +y >= 3 +""" +# eqs = np.asarray([[1, 2, -8]], dtype=np.int64) +# ineqs = np.asarray([[1, -1, -1]], dtype=np.int64) +# relation = presburger.IntegerRelation(ineqs, eqs, 2, 0) +# print(relation) +# relation.add_inequality([0, 1, -3]) +# print(relation) +# t = relation.equalities() +# print(t) +# print(relation.num_constraints) +# print(relation.num_inequalities) +# print(relation.num_equalities) +# print(relation.num_domain_vars) +# print(relation.num_range_vars) +# print(relation.num_symbol_vars) +# print(relation.num_local_vars) +# print(relation.num_columns) + +# eq_first_row = relation.get_equality(0) +# print(eq_first_row) +# ineq_second_row = relation.get_inequality(1) +# print(ineq_second_row) + +# eq_coefficients = relation.equalities() +# print(eq_coefficients[0, 1]) +# ineq_coefficients = relation.inequalities() +# print(ineq_coefficients[1, 1]) + +""" +Test intersection + +Relation A + +x + y <= 6 + +Relation B + +x>=2 +""" +# print("-------") +# eqs_a = np.asarray([[0, 0, 0]], dtype=np.int64) +# ineqs_a = np.asarray([[-1, -1, 6]], dtype=np.int64) +# relation_a = presburger.IntegerRelation(ineqs_a, eqs_a, 2, 0) +# print(relation_a) + +# eqs_b = np.asarray([[0, 0, 0]], dtype=np.int64) +# ineqs_b = np.asarray([[1, 0, -2]], dtype=np.int64) +# relation_b = presburger.IntegerRelation(ineqs_b, eqs_b, 2, 0) +# print(relation_b) + +# a_b_intersection = relation_a.intersect(relation_b) +# print(a_b_intersection) + +# print(a_b_intersection.num_vars) +# print(a_b_intersection.get_var_kind_at(1)) + +""" +y = 2x +x <= 5 +0 <= x + +""" +# eqs = np.asarray([[-2, 1, 0]], dtype=np.int64) +# ineqs = np.asarray([[-1, 0, 5], [1, 0, 0]], dtype=np.int64) +# relation = presburger.IntegerRelation(ineqs, eqs, 1, 1) +# print(relation) +# print(relation.num_vars) +# t = relation.get_var_kind_at(1) +# print(t, type(t)) +# print(relation.append_var(presburger.VariableKind.Range)) +# print(relation) + + +""" +x+y = 20 +x <= 20 +x >= 6 +y <= 14 +y >= 5 +""" + +eqs = np.asarray([[1, 1, -20]], dtype=np.int64) +ineqs = np.asarray([[-1, 0, 20], [1, 0, -6], [0, 1, -5], [0, -1, 14]], dtype=np.int64) +relation = presburger.IntegerRelation(ineqs, eqs, 2, 0) +print(relation) +lex_min = relation.find_integer_lex_min() + +print(lex_min) +print(lex_min.is_unbounded()) +print(lex_min.is_bounded()) +print(lex_min.get_integer_point()) + +integer_sample = relation.find_integer_sample() +print(integer_sample) + +int_volume = relation.compute_volume() +print(int_volume) + +print(relation.contains_point([23, 7])) \ No newline at end of file