[Mlir-commits] [mlir] [Python] Develop python bindings for Presburger library (PR #113233)
Sagar Shelke
llvmlistbot at llvm.org
Wed Nov 20 17:42:59 PST 2024
https://github.com/shelkesagar29 updated https://github.com/llvm/llvm-project/pull/113233
>From 7c46e14a3383ff314d76188c1a6d97b210face36 Mon Sep 17 00:00:00 2001
From: Sagar Shelke <shelkesagar29 at yahoo.com>
Date: Thu, 17 Oct 2024 23:29:01 +0000
Subject: [PATCH] [presburger] Develope python bindings for presburger c++
library
This MR is work in progress.
---
mlir/include/mlir-c/Presburger.h | 532 +++++++++++++
.../Analysis/Presburger/IntegerRelation.h | 18 +
mlir/include/mlir/CAPI/Presburger.h | 25 +
mlir/lib/Bindings/Python/Presburger.cpp | 753 ++++++++++++++++++
mlir/lib/CAPI/CMakeLists.txt | 1 +
mlir/lib/CAPI/Presburger/CMakeLists.txt | 6 +
mlir/lib/CAPI/Presburger/Presburger.cpp | 499 ++++++++++++
mlir/python/CMakeLists.txt | 19 +
mlir/python/mlir/presburger.py | 6 +
mlir/test/python/presburger.py | 108 +++
10 files changed, 1967 insertions(+)
create mode 100644 mlir/include/mlir-c/Presburger.h
create mode 100644 mlir/include/mlir/CAPI/Presburger.h
create mode 100644 mlir/lib/Bindings/Python/Presburger.cpp
create mode 100644 mlir/lib/CAPI/Presburger/CMakeLists.txt
create mode 100644 mlir/lib/CAPI/Presburger/Presburger.cpp
create mode 100644 mlir/python/mlir/presburger.py
create mode 100644 mlir/test/python/presburger.py
diff --git a/mlir/include/mlir-c/Presburger.h b/mlir/include/mlir-c/Presburger.h
new file mode 100644
index 00000000000000..3146f1ec205d8d
--- /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 <non-negative constant> >= 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 a27fc8c37eeda1..e79a866f4bab46 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<IntegerRelation *>(this);
+ }
+
+ static IntegerRelation *getFromOpaquePointer(const void *pointer) {
+ return const_cast<IntegerRelation *>(
+ reinterpret_cast<const IntegerRelation *>(pointer));
+ }
+
void print(raw_ostream &os) const;
void dump() const;
@@ -979,6 +988,15 @@ class IntegerPolyhedron : public IntegerRelation {
/// Return the set difference of this set and the given set, i.e.,
/// return `this \ set`.
PresburgerSet subtract(const PresburgerSet &other) const;
+
+ void *getAsOpaquePointer() const {
+ return const_cast<IntegerPolyhedron *>(this);
+ }
+
+ static IntegerPolyhedron *getFromOpaquePointer(const void *pointer) {
+ return const_cast<IntegerPolyhedron *>(
+ reinterpret_cast<const IntegerPolyhedron *>(pointer));
+ }
};
} // namespace presburger
diff --git a/mlir/include/mlir/CAPI/Presburger.h b/mlir/include/mlir/CAPI/Presburger.h
new file mode 100644
index 00000000000000..8d9a2d59a31a61
--- /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 00000000000000..e0d903f603a6e3
--- /dev/null
+++ b/mlir/lib/Bindings/Python/Presburger.cpp
@@ -0,0 +1,753 @@
+//===- 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 <pybind11/detail/common.h>
+#include <pybind11/pybind11.h>
+
+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<PyPresburgerIntegerRelation>
+ getFromNumConstrainsAndVars(uint64_t numReservedInequalities,
+ uint64_t numReservedEqualities,
+ uint64_t numReservedCols);
+ static std::unique_ptr<PyPresburgerIntegerRelation>
+ 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>
+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<Py_buffer> ineqView = std::make_unique<Py_buffer>();
+ 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<Py_buffer> eqView = std::make_unique<Py_buffer>();
+ 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<const int64_t *>(ineqView->buf), numInequalities,
+ reinterpret_cast<const int64_t *>(eqView->buf), numEqualities,
+ numDomainVars, numRangeVars);
+ return std::make_unique<PyPresburgerIntegerRelation>(relation);
+}
+
+std::unique_ptr<PyPresburgerIntegerRelation>
+PyPresburgerIntegerRelation::getFromNumConstrainsAndVars(
+ uint64_t numReservedInequalities, uint64_t numReservedEqualities,
+ uint64_t numReservedCols) {
+ MlirPresburgerIntegerRelation relation = mlirPresburgerIntegerRelationCreate(
+ numReservedInequalities, numReservedEqualities, numReservedCols);
+ return std::make_unique<PyPresburgerIntegerRelation>(relation);
+}
+
+py::object PyPresburgerIntegerRelation::getCapsule() {
+ throw std::invalid_argument("unimplemented");
+}
+
+void PyPresburgerTableau::bind(py::module &m) {
+ py::class_<PyPresburgerTableau>(m, "IntegerRelationTableau",
+ py::module_local())
+ .def("__getitem__", [](PyPresburgerTableau &self,
+ const py::tuple &index) {
+ return self.at64(index[0].cast<int64_t>(), index[1].cast<int64_t>());
+ });
+}
+
+void PyPresburgerMaybeOptimum::bind(py::module &m) {
+ py::class_<PyPresburgerMaybeOptimum>(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<int64_t>();
+ std::vector<int64_t> r{self.integerPoint,
+ self.integerPoint + self.integerPointSize};
+ return r;
+ });
+}
+
+void PyPresburgerIntegerRelation::bind(py::module &m) {
+ py::class_<PyPresburgerIntegerRelation>(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<int64_t> 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<int64_t> 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<int64_t> {
+ 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<int64_t> &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<int64_t> &eq) {
+ return mlirPresburgerIntegerRelationAddEquality(
+ self.relation, eq.data(), eq.size());
+ },
+ py::arg("coefficients"))
+ .def(
+ "add_inequality",
+ [](PyPresburgerIntegerRelation &self,
+ const std::vector<int64_t> &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<PyPresburgerMaybeOptimum>(r);
+ return mayBeOptimum.release();
+ },
+ py::return_value_policy::take_ownership)
+ .def("find_integer_sample",
+ [](PyPresburgerIntegerRelation &self)
+ -> std::optional<std::vector<int64_t>> {
+ auto r =
+ mlirPresburgerIntegerRelationFindIntegerSample(self.relation);
+ if (!r.hasValue)
+ return std::nullopt;
+ std::vector<int64_t> integerSample{r.data, r.data + r.size};
+ return integerSample;
+ })
+ .def("compute_volume",
+ [](PyPresburgerIntegerRelation &self) -> std::optional<int64_t> {
+ 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<int64_t> &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<uint64_t>());
+ },
+ 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<int64_t> &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(
+ "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_<MlirPresburgerVariableKind>(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_<MlirPresburgerBoundType>(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 6c438508425b7c..56888798e92292 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 00000000000000..956006233dda5b
--- /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 00000000000000..06ea5d50bc2302
--- /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<int64_t> coef(rowPtr, rowPtr + numCols);
+ relation->addInequality(coef);
+ }
+ for (const int64_t *rowPtr = equalityCoefficients;
+ rowPtr < equalityCoefficients + numCols * numEqualities;
+ rowPtr += numCols) {
+ llvm::ArrayRef<int64_t> coef(rowPtr, rowPtr + numCols);
+ relation->addEquality(coef);
+ }
+ return wrap(relation);
+}
+
+void mlirPresburgerIntegerRelationDestroy(
+ MlirPresburgerIntegerRelation relation) {
+ if (relation.ptr)
+ delete reinterpret_cast<IntegerRelation *>(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<IntegerRelation>(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<VarKind>(kind));
+}
+
+unsigned mlirPresburgerIntegerRelationGetVarKindOffset(
+ MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind) {
+ return unwrap(relation)->getVarKindOffset(static_cast<VarKind>(kind));
+}
+
+unsigned mlirPresburgerIntegerRelationGetVarKindEnd(
+ MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind) {
+ return unwrap(relation)->getVarKindEnd(static_cast<VarKind>(kind));
+}
+
+unsigned mlirPresburgerIntegerRelationGetVarKindOverLap(
+ MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind,
+ unsigned varStart, unsigned varLimit) {
+ return unwrap(relation)->getVarKindOverlap(static_cast<VarKind>(kind),
+ varStart, varLimit);
+}
+
+MlirPresburgerVariableKind mlirPresburgerIntegerRelationGetVarKindAt(
+ MlirPresburgerIntegerRelation relation, unsigned pos) {
+ return static_cast<MlirPresburgerVariableKind>(
+ unwrap(relation)->getVarKindAt(pos));
+}
+
+MlirOptionalInt64 mlirPresburgerIntegerRelationGetConstantBound64(
+ MlirPresburgerIntegerRelation relation, MlirPresburgerBoundType type,
+ unsigned pos) {
+ auto r =
+ unwrap(relation)->getConstantBound64(static_cast<BoundType>(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<int64_t[]>(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<int64_t[]>(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<int64_t>(point, point + size));
+}
+
+//===----------------------------------------------------------------------===//
+// IntegerRelation Tableau Manipulation
+//===----------------------------------------------------------------------===//
+
+unsigned
+mlirPresburgerIntegerRelationInsertVar(MlirPresburgerIntegerRelation relation,
+ MlirPresburgerVariableKind kind,
+ unsigned pos, unsigned num) {
+ return unwrap(relation)->insertVar(static_cast<VarKind>(kind), pos, num);
+}
+
+unsigned
+mlirPresburgerIntegerRelationAppendVar(MlirPresburgerIntegerRelation relation,
+ MlirPresburgerVariableKind kind,
+ unsigned num) {
+ return unwrap(relation)->appendVar(static_cast<VarKind>(kind), num);
+}
+
+void mlirPresburgerIntegerRelationAddEquality(
+ MlirPresburgerIntegerRelation relation, const int64_t *coeff,
+ int64_t coeffSize) {
+ unwrap(relation)->addEquality(ArrayRef<int64_t>(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<int64_t>(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<VarKind>(kind), pos);
+}
+
+void mlirPresburgerIntegerRelationRemoveVarRangeKind(
+ MlirPresburgerIntegerRelation relation, MlirPresburgerVariableKind kind,
+ unsigned varStart, unsigned varLimit) {
+ return unwrap(relation)->removeVarRange(static_cast<VarKind>(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<int64_t>(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<VarKind>(srcKind),
+ varStart, varLimit,
+ static_cast<VarKind>(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<BoundType>(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<BoundType>(type),
+ ArrayRef<int64_t>(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 23187f256455bb..f47cbddc7e371f 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 00000000000000..f4235c4ed75d5e
--- /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 00000000000000..290ae9badc9aa0
--- /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
More information about the Mlir-commits
mailing list