[Python] Develop python bindings for Presburger library #113233
Conversation
shelkesagar29
requested review from
ftynse,
makslevental,
stellaraccident,
Groverkss and
Superty
as code owners
|
Thank you for submitting a Pull Request (PR) to the LLVM Project! This PR will be automatically labeled and the relevant teams will be notified. If you wish to, you can add reviewers by using the "Reviewers" section on this page. If this is not working for you, it is probably because you do not have write permissions for the repository. In which case you can instead tag reviewers by name in a comment by using If you have received no comments on your PR for a week, you can request a review by "ping"ing the PR by adding a comment “Ping”. The common courtesy "ping" rate is once a week. Please remember that you are asking for valuable time from other developers. If you have further questions, they may be answered by the LLVM GitHub User Guide. You can also ask questions in a comment on this PR, on the LLVM Discord or on the forums. |
|
@llvm/pr-subscribers-mlir @llvm/pr-subscribers-mlir-presburger Author: Sagar Shelke (shelkesagar29) ChangesThis MR is work in progress. Patch is 29.76 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/113233.diff 11 Files Affected:
diff --git a/llvm/include/llvm/ADT/DynamicAPInt.h b/llvm/include/llvm/ADT/DynamicAPInt.h
index ff958d48e77317..7515522edd0bf6 100644
--- a/llvm/include/llvm/ADT/DynamicAPInt.h
+++ b/llvm/include/llvm/ADT/DynamicAPInt.h
@@ -217,6 +217,13 @@ class DynamicAPInt {
raw_ostream &print(raw_ostream &OS) const;
LLVM_DUMP_METHOD void dump() const;
+
+ void *getAsOpaquePointer() const { return const_cast<DynamicAPInt *>(this); }
+
+ static DynamicAPInt *getFromOpaquePointer(const void *Pointer) {
+ return const_cast<DynamicAPInt *>(
+ reinterpret_cast<const DynamicAPInt *>(Pointer));
+ }
};
inline raw_ostream &operator<<(raw_ostream &OS, const DynamicAPInt &X) {
diff --git a/mlir/include/mlir-c/Presburger.h b/mlir/include/mlir-c/Presburger.h
new file mode 100644
index 00000000000000..dd7343c160b5c6
--- /dev/null
+++ b/mlir/include/mlir-c/Presburger.h
@@ -0,0 +1,145 @@
+#ifndef MLIR_C_PRESBURGER_H
+#define MLIR_C_PRESBURGER_H
+#include "mlir-c/AffineExpr.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+enum MlirPresburgerVariableKind {
+ Symbol,
+ Local,
+ Domain,
+ Range,
+ SetDim = Range
+};
+
+#define DEFINE_C_API_STRUCT(name, storage) \
+ struct name { \
+ storage *ptr; \
+ }; \
+ typedef struct name name
+DEFINE_C_API_STRUCT(MlirPresburgerIntegerRelation, void);
+DEFINE_C_API_STRUCT(MlirPresburgerDynamicAPInt, const 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
+//===----------------------------------------------------------------------===//
+
+/// 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);
+
+/// Return the intersection of the two relations.
+/// If there are locals, they will be merged.
+MLIR_CAPI_EXPORTED MlirPresburgerIntegerRelation
+mlirPresburgerIntegerRelationIntersect(MlirPresburgerIntegerRelation lhs,
+ MlirPresburgerIntegerRelation rhs);
+
+//===----------------------------------------------------------------------===//
+// IntegerRelation Tableau Inspection
+//===----------------------------------------------------------------------===//
+
+/// Returns the value at the specified equality row and column.
+MLIR_CAPI_EXPORTED MlirPresburgerDynamicAPInt
+mlirPresburgerIntegerRelationAtEq(unsigned i, unsigned j);
+
+/// The same, but casts to int64_t. This is unsafe and will assert-fail if the
+/// value does not fit in an int64_t.
+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 MlirPresburgerDynamicAPInt
+mlirPresburgerIntegerRelationAtIneq(MlirPresburgerIntegerRelation relation,
+ unsigned row, unsigned col);
+
+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 inequality constraints.
+MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumInequalities(
+ MlirPresburgerIntegerRelation relation);
+
+/// Returns the number of equality constraints.
+MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumEqualities(
+ 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);
+
+/// Returns the total number of columns in the tableau.
+MLIR_CAPI_EXPORTED unsigned
+mlirPresburgerIntegerRelationNumCols(MlirPresburgerIntegerRelation relation);
+
+/// Return the VarKind of the var at the specified position.
+MLIR_CAPI_EXPORTED MlirPresburgerVariableKind
+mlirPresburgerIntegerRelationGetVarKindAt(unsigned pos);
+
+MLIR_CAPI_EXPORTED void
+mlirPresburgerIntegerRelationDump(MlirPresburgerIntegerRelation relation);
+
+//===----------------------------------------------------------------------===//
+// IntegerRelation Tableau Manipulation
+//===----------------------------------------------------------------------===//
+/// Adds an equality with the given coefficients.
+MLIR_CAPI_EXPORTED void
+mlirPresburgerIntegerRelationAddEquality(const int64_t *coefficients,
+ size_t coefficientsSize);
+
+/// Adds an inequality with the given coefficients.
+MLIR_CAPI_EXPORTED void
+mlirPresburgerIntegerRelationAddInequality(const int64_t *coefficients,
+ size_t coefficientsSize);
+#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..b58e2be164ec8f 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;
diff --git a/mlir/include/mlir/CAPI/Presburger.h b/mlir/include/mlir/CAPI/Presburger.h
new file mode 100644
index 00000000000000..cc88d13b638928
--- /dev/null
+++ b/mlir/include/mlir/CAPI/Presburger.h
@@ -0,0 +1,29 @@
+#ifndef MLIR_CAPI_PRESBURGER_H
+#define MLIR_CAPI_PRESBURGER_H
+
+#include "mlir-c/Presburger.h"
+#include "mlir/Analysis/Presburger/IntegerRelation.h"
+#include "mlir/Analysis/Presburger/PresburgerSpace.h"
+#include "mlir/CAPI/Wrap.h"
+#include "llvm/ADT/DynamicAPInt.h"
+
+DEFINE_C_API_PTR_METHODS(MlirPresburgerIntegerRelation,
+ mlir::presburger::IntegerRelation)
+
+static inline MlirPresburgerDynamicAPInt wrap(llvm::DynamicAPInt *cpp) {
+ return MlirPresburgerDynamicAPInt{cpp->getAsOpaquePointer()};
+}
+
+static inline llvm::DynamicAPInt *unwrap(MlirPresburgerDynamicAPInt c) {
+ return llvm::DynamicAPInt::getFromOpaquePointer(c.ptr);
+}
+
+static inline MlirPresburgerVariableKind wrap(mlir::presburger::VarKind var) {
+ return static_cast<MlirPresburgerVariableKind>(var);
+}
+
+static inline mlir::presburger::VarKind unwarp(MlirPresburgerVariableKind var) {
+ return static_cast<mlir::presburger::VarKind>(var);
+}
+
+#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..b652f75439efa5
--- /dev/null
+++ b/mlir/lib/Bindings/Python/Presburger.cpp
@@ -0,0 +1,244 @@
+#include "mlir-c/Presburger.h"
+#include "PybindUtils.h"
+#include "mlir-c/Bindings/Python/Interop.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/ScopeExit.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/FormatVariadic.h"
+#include <pybind11/attr.h>
+#include <pybind11/pybind11.h>
+#include <stdexcept>
+
+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(PyPresburgerIntegerRelation &&other) noexcept
+ : relation(other.relation) {
+ other.relation.ptr = nullptr;
+ }
+ ~PyPresburgerIntegerRelation() {
+ if (relation.ptr) {
+ mlirPresburgerIntegerRelationDestroy(relation);
+ relation.ptr = {nullptr};
+ }
+ }
+ static PyPresburgerIntegerRelation
+ getFromBuffers(py::buffer inequalitiesCoefficients,
+ py::buffer equalityCoefficients, unsigned numDomainVars,
+ unsigned numRangeVars);
+ py::object getCapsule();
+ int64_t getNumConstraints() {
+ return mlirPresburgerIntegerRelationNumConstraints(relation);
+ }
+ int64_t getNumInequalities() {
+ return mlirPresburgerIntegerRelationNumInequalities(relation);
+ }
+ int64_t getNumEqualities() {
+ return mlirPresburgerIntegerRelationNumEqualities(relation);
+ }
+ int64_t getNumDomainVars() {
+ return mlirPresburgerIntegerRelationNumDomainVars(relation);
+ }
+ int64_t getNumRangeVars() {
+ return mlirPresburgerIntegerRelationNumRangeVars(relation);
+ }
+ int64_t getNumSymbolVars() {
+ return mlirPresburgerIntegerRelationNumSymbolVars(relation);
+ }
+ int64_t getNumLocalVars() {
+ return mlirPresburgerIntegerRelationNumLocalVars(relation);
+ }
+ int64_t getNumCols() {
+ return mlirPresburgerIntegerRelationNumCols(relation);
+ }
+ 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;
+};
+} // namespace
+
+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 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 &tableau,
+ const py::tuple &index) {
+ return tableau.at64(index[0].cast<int64_t>(), index[1].cast<int64_t>());
+ });
+}
+
+static void populatePresburgerModule(py::module &m) {
+ PyPresburgerTableau::bind(m);
+ py::class_<PyPresburgerIntegerRelation>(m, "IntegerRelation",
+ py::module_local())
+ .def(py::init<>(&PyPresburgerIntegerRelation::getFromBuffers))
+ .def_property_readonly(MLIR_PYTHON_CAPI_PTR_ATTR,
+ &PyPresburgerIntegerRelation::getCapsule)
+ .def("__eq__",
+ [](PyPresburgerIntegerRelation &relation,
+ PyPresburgerIntegerRelation &other) {
+ return mlirPresburgerIntegerRelationIsEqual(relation.relation,
+ other.relation);
+ })
+ .def(
+ "intersect",
+ [](PyPresburgerIntegerRelation &relation,
+ PyPresburgerIntegerRelation &other) {
+ PyPresburgerIntegerRelation intersection(
+ mlirPresburgerIntegerRelationIntersect(relation.relation,
+ other.relation));
+ return intersection;
+ },
+ py::keep_alive<0, 1>())
+ .def(
+ "inequalities",
+ [](PyPresburgerIntegerRelation &relation) {
+ PyPresburgerTableau tableau(
+ relation.relation, PyPresburgerTableau::Kind::Inequalities);
+ return tableau;
+ },
+ py::keep_alive<0, 1>())
+ .def(
+ "equalities",
+ [](PyPresburgerIntegerRelation &relation) {
+ PyPresburgerTableau tableau(relation.relation,
+ PyPresburgerTableau::Kind::Equalities);
+ return tableau;
+ },
+ py::keep_alive<0, 1>())
+ .def("get_equality",
+ [](PyPresburgerIntegerRelation &relation, int64_t row) {
+ unsigned numCol =
+ mlirPresburgerIntegerRelationNumCols(relation.relation);
+ std::vector<int64_t> result(numCol);
+ for (unsigned i = 0; i < numCol; i++)
+ result[i] = mlirPresburgerIntegerRelationAtEq64(
+ relation.relation, row, i);
+ return result;
+ })
+ .def("get_inequality",
+ [](PyPresburgerIntegerRelation &relation, int64_t row) {
+ unsigned numCol =
+ mlirPresburgerIntegerRelationNumCols(relation.relation);
+ std::vector<int64_t> result(numCol);
+ for (unsigned i = 0; i < numCol; i++)
+ result[i] = mlirPresburgerIntegerRelationAtIneq64(
+ relation.relation, row, i);
+ return result;
+ })
+ .def_property_readonly("num_constraints",
+ &PyPresburgerIntegerRelation::getNumConstraints)
+ .def_property_readonly("num_equalities",
+ &PyPresburgerIntegerRelation::getNumEqualities)
+ .def_property_readonly("num_inequalities",
+ &PyPresburgerIntegerRelation::getNumInequalities)
+ .def_property_readonly("num_domain_vars",
+ &PyPresburgerIntegerRelation::getNumDomainVars)
+ .def_property_readonly("num_range_vars",
+ &PyPresburgerIntegerRelation::getNumRangeVars)
+ .def_property_readonly("num_symbol_vars",
+ &PyPresburgerIntegerRelation::getNumSymbolVars)
+ .def_property_readonly("num_local_vars",
+ &PyPresburgerIntegerRelation::getNumLocalVars)
+ .def_property_readonly("num_columns",
+ &PyPresburgerIntegerRelation::getNumCols)
+ .def("__str__", [](PyPresburgerIntegerRelation &relation) {
+ mlirPresburgerIntegerRelationDump(relation.relation);
+ return "";
+ });
+}
+// -----------------------------------------------------------------------------
+// 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/...
[truncated]
|
|
@llvm/pr-subscribers-llvm-adt Author: Sagar Shelke (shelkesagar29) ChangesThis MR is work in progress. Patch is 29.76 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/113233.diff 11 Files Affected:
diff --git a/llvm/include/llvm/ADT/DynamicAPInt.h b/llvm/include/llvm/ADT/DynamicAPInt.h
index ff958d48e77317..7515522edd0bf6 100644
--- a/llvm/include/llvm/ADT/DynamicAPInt.h
+++ b/llvm/include/llvm/ADT/DynamicAPInt.h
@@ -217,6 +217,13 @@ class DynamicAPInt {
raw_ostream &print(raw_ostream &OS) const;
LLVM_DUMP_METHOD void dump() const;
+
+ void *getAsOpaquePointer() const { return const_cast<DynamicAPInt *>(this); }
+
+ static DynamicAPInt *getFromOpaquePointer(const void *Pointer) {
+ return const_cast<DynamicAPInt *>(
+ reinterpret_cast<const DynamicAPInt *>(Pointer));
+ }
};
inline raw_ostream &operator<<(raw_ostream &OS, const DynamicAPInt &X) {
diff --git a/mlir/include/mlir-c/Presburger.h b/mlir/include/mlir-c/Presburger.h
new file mode 100644
index 00000000000000..dd7343c160b5c6
--- /dev/null
+++ b/mlir/include/mlir-c/Presburger.h
@@ -0,0 +1,145 @@
+#ifndef MLIR_C_PRESBURGER_H
+#define MLIR_C_PRESBURGER_H
+#include "mlir-c/AffineExpr.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+enum MlirPresburgerVariableKind {
+ Symbol,
+ Local,
+ Domain,
+ Range,
+ SetDim = Range
+};
+
+#define DEFINE_C_API_STRUCT(name, storage) \
+ struct name { \
+ storage *ptr; \
+ }; \
+ typedef struct name name
+DEFINE_C_API_STRUCT(MlirPresburgerIntegerRelation, void);
+DEFINE_C_API_STRUCT(MlirPresburgerDynamicAPInt, const 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
+//===----------------------------------------------------------------------===//
+
+/// 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);
+
+/// Return the intersection of the two relations.
+/// If there are locals, they will be merged.
+MLIR_CAPI_EXPORTED MlirPresburgerIntegerRelation
+mlirPresburgerIntegerRelationIntersect(MlirPresburgerIntegerRelation lhs,
+ MlirPresburgerIntegerRelation rhs);
+
+//===----------------------------------------------------------------------===//
+// IntegerRelation Tableau Inspection
+//===----------------------------------------------------------------------===//
+
+/// Returns the value at the specified equality row and column.
+MLIR_CAPI_EXPORTED MlirPresburgerDynamicAPInt
+mlirPresburgerIntegerRelationAtEq(unsigned i, unsigned j);
+
+/// The same, but casts to int64_t. This is unsafe and will assert-fail if the
+/// value does not fit in an int64_t.
+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 MlirPresburgerDynamicAPInt
+mlirPresburgerIntegerRelationAtIneq(MlirPresburgerIntegerRelation relation,
+ unsigned row, unsigned col);
+
+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 inequality constraints.
+MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumInequalities(
+ MlirPresburgerIntegerRelation relation);
+
+/// Returns the number of equality constraints.
+MLIR_CAPI_EXPORTED unsigned mlirPresburgerIntegerRelationNumEqualities(
+ 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);
+
+/// Returns the total number of columns in the tableau.
+MLIR_CAPI_EXPORTED unsigned
+mlirPresburgerIntegerRelationNumCols(MlirPresburgerIntegerRelation relation);
+
+/// Return the VarKind of the var at the specified position.
+MLIR_CAPI_EXPORTED MlirPresburgerVariableKind
+mlirPresburgerIntegerRelationGetVarKindAt(unsigned pos);
+
+MLIR_CAPI_EXPORTED void
+mlirPresburgerIntegerRelationDump(MlirPresburgerIntegerRelation relation);
+
+//===----------------------------------------------------------------------===//
+// IntegerRelation Tableau Manipulation
+//===----------------------------------------------------------------------===//
+/// Adds an equality with the given coefficients.
+MLIR_CAPI_EXPORTED void
+mlirPresburgerIntegerRelationAddEquality(const int64_t *coefficients,
+ size_t coefficientsSize);
+
+/// Adds an inequality with the given coefficients.
+MLIR_CAPI_EXPORTED void
+mlirPresburgerIntegerRelationAddInequality(const int64_t *coefficients,
+ size_t coefficientsSize);
+#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..b58e2be164ec8f 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;
diff --git a/mlir/include/mlir/CAPI/Presburger.h b/mlir/include/mlir/CAPI/Presburger.h
new file mode 100644
index 00000000000000..cc88d13b638928
--- /dev/null
+++ b/mlir/include/mlir/CAPI/Presburger.h
@@ -0,0 +1,29 @@
+#ifndef MLIR_CAPI_PRESBURGER_H
+#define MLIR_CAPI_PRESBURGER_H
+
+#include "mlir-c/Presburger.h"
+#include "mlir/Analysis/Presburger/IntegerRelation.h"
+#include "mlir/Analysis/Presburger/PresburgerSpace.h"
+#include "mlir/CAPI/Wrap.h"
+#include "llvm/ADT/DynamicAPInt.h"
+
+DEFINE_C_API_PTR_METHODS(MlirPresburgerIntegerRelation,
+ mlir::presburger::IntegerRelation)
+
+static inline MlirPresburgerDynamicAPInt wrap(llvm::DynamicAPInt *cpp) {
+ return MlirPresburgerDynamicAPInt{cpp->getAsOpaquePointer()};
+}
+
+static inline llvm::DynamicAPInt *unwrap(MlirPresburgerDynamicAPInt c) {
+ return llvm::DynamicAPInt::getFromOpaquePointer(c.ptr);
+}
+
+static inline MlirPresburgerVariableKind wrap(mlir::presburger::VarKind var) {
+ return static_cast<MlirPresburgerVariableKind>(var);
+}
+
+static inline mlir::presburger::VarKind unwarp(MlirPresburgerVariableKind var) {
+ return static_cast<mlir::presburger::VarKind>(var);
+}
+
+#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..b652f75439efa5
--- /dev/null
+++ b/mlir/lib/Bindings/Python/Presburger.cpp
@@ -0,0 +1,244 @@
+#include "mlir-c/Presburger.h"
+#include "PybindUtils.h"
+#include "mlir-c/Bindings/Python/Interop.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/ScopeExit.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/FormatVariadic.h"
+#include <pybind11/attr.h>
+#include <pybind11/pybind11.h>
+#include <stdexcept>
+
+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(PyPresburgerIntegerRelation &&other) noexcept
+ : relation(other.relation) {
+ other.relation.ptr = nullptr;
+ }
+ ~PyPresburgerIntegerRelation() {
+ if (relation.ptr) {
+ mlirPresburgerIntegerRelationDestroy(relation);
+ relation.ptr = {nullptr};
+ }
+ }
+ static PyPresburgerIntegerRelation
+ getFromBuffers(py::buffer inequalitiesCoefficients,
+ py::buffer equalityCoefficients, unsigned numDomainVars,
+ unsigned numRangeVars);
+ py::object getCapsule();
+ int64_t getNumConstraints() {
+ return mlirPresburgerIntegerRelationNumConstraints(relation);
+ }
+ int64_t getNumInequalities() {
+ return mlirPresburgerIntegerRelationNumInequalities(relation);
+ }
+ int64_t getNumEqualities() {
+ return mlirPresburgerIntegerRelationNumEqualities(relation);
+ }
+ int64_t getNumDomainVars() {
+ return mlirPresburgerIntegerRelationNumDomainVars(relation);
+ }
+ int64_t getNumRangeVars() {
+ return mlirPresburgerIntegerRelationNumRangeVars(relation);
+ }
+ int64_t getNumSymbolVars() {
+ return mlirPresburgerIntegerRelationNumSymbolVars(relation);
+ }
+ int64_t getNumLocalVars() {
+ return mlirPresburgerIntegerRelationNumLocalVars(relation);
+ }
+ int64_t getNumCols() {
+ return mlirPresburgerIntegerRelationNumCols(relation);
+ }
+ 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;
+};
+} // namespace
+
+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 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 &tableau,
+ const py::tuple &index) {
+ return tableau.at64(index[0].cast<int64_t>(), index[1].cast<int64_t>());
+ });
+}
+
+static void populatePresburgerModule(py::module &m) {
+ PyPresburgerTableau::bind(m);
+ py::class_<PyPresburgerIntegerRelation>(m, "IntegerRelation",
+ py::module_local())
+ .def(py::init<>(&PyPresburgerIntegerRelation::getFromBuffers))
+ .def_property_readonly(MLIR_PYTHON_CAPI_PTR_ATTR,
+ &PyPresburgerIntegerRelation::getCapsule)
+ .def("__eq__",
+ [](PyPresburgerIntegerRelation &relation,
+ PyPresburgerIntegerRelation &other) {
+ return mlirPresburgerIntegerRelationIsEqual(relation.relation,
+ other.relation);
+ })
+ .def(
+ "intersect",
+ [](PyPresburgerIntegerRelation &relation,
+ PyPresburgerIntegerRelation &other) {
+ PyPresburgerIntegerRelation intersection(
+ mlirPresburgerIntegerRelationIntersect(relation.relation,
+ other.relation));
+ return intersection;
+ },
+ py::keep_alive<0, 1>())
+ .def(
+ "inequalities",
+ [](PyPresburgerIntegerRelation &relation) {
+ PyPresburgerTableau tableau(
+ relation.relation, PyPresburgerTableau::Kind::Inequalities);
+ return tableau;
+ },
+ py::keep_alive<0, 1>())
+ .def(
+ "equalities",
+ [](PyPresburgerIntegerRelation &relation) {
+ PyPresburgerTableau tableau(relation.relation,
+ PyPresburgerTableau::Kind::Equalities);
+ return tableau;
+ },
+ py::keep_alive<0, 1>())
+ .def("get_equality",
+ [](PyPresburgerIntegerRelation &relation, int64_t row) {
+ unsigned numCol =
+ mlirPresburgerIntegerRelationNumCols(relation.relation);
+ std::vector<int64_t> result(numCol);
+ for (unsigned i = 0; i < numCol; i++)
+ result[i] = mlirPresburgerIntegerRelationAtEq64(
+ relation.relation, row, i);
+ return result;
+ })
+ .def("get_inequality",
+ [](PyPresburgerIntegerRelation &relation, int64_t row) {
+ unsigned numCol =
+ mlirPresburgerIntegerRelationNumCols(relation.relation);
+ std::vector<int64_t> result(numCol);
+ for (unsigned i = 0; i < numCol; i++)
+ result[i] = mlirPresburgerIntegerRelationAtIneq64(
+ relation.relation, row, i);
+ return result;
+ })
+ .def_property_readonly("num_constraints",
+ &PyPresburgerIntegerRelation::getNumConstraints)
+ .def_property_readonly("num_equalities",
+ &PyPresburgerIntegerRelation::getNumEqualities)
+ .def_property_readonly("num_inequalities",
+ &PyPresburgerIntegerRelation::getNumInequalities)
+ .def_property_readonly("num_domain_vars",
+ &PyPresburgerIntegerRelation::getNumDomainVars)
+ .def_property_readonly("num_range_vars",
+ &PyPresburgerIntegerRelation::getNumRangeVars)
+ .def_property_readonly("num_symbol_vars",
+ &PyPresburgerIntegerRelation::getNumSymbolVars)
+ .def_property_readonly("num_local_vars",
+ &PyPresburgerIntegerRelation::getNumLocalVars)
+ .def_property_readonly("num_columns",
+ &PyPresburgerIntegerRelation::getNumCols)
+ .def("__str__", [](PyPresburgerIntegerRelation &relation) {
+ mlirPresburgerIntegerRelationDump(relation.relation);
+ return "";
+ });
+}
+// -----------------------------------------------------------------------------
+// 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/...
[truncated]
|
shelkesagar29
force-pushed
the
pburger_python
branch
from
1a4649c to
0744372
Compare
|
Looks very promising! @makslevental would probably be the best person to review the python/C api side of things. Me and @Superty can help with any Presburger related issues you might face. Thanks for taking this up! |
|
I can take a look tomorrow |
|
This will need some top-level documentation about object ownership. Tableaus are rather large and I see a bunch of |
| 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; |
There was a problem hiding this comment.
is there a reason to not just add int64_t at64 to PyPresburgerIntegerRelation?
There was a problem hiding this comment.
Co-author here. at64 on PyPresburgerIntegerRelation is ambiguous, are you referring to the equality matrix or inequality matrix? The intent was to allow creating an API like the following:
relation = mlir.presburger.IntegerRelation(...)
eq = relation.equalities()
eq[i, j] = XIntegeRelation internally stores equalities and inequalities as separate matrices of type presburger::IntMatrix. We could just expose IntMatrix as a separate C API as well, but currently IntegerRelation does not expose these IntMatrix objects directly in its public API. You can only access coefficients through IntegerRelation::atIneq|atEq methods.
Edit: the equalities[...] accessor method is not implemented here; I was hoping that could be added after the DynamicAPInt functionality was exposed, @shelkesagar29 can you add it?
There was a problem hiding this comment.
The intent was to allow creating an API like the following:
relation = mlir.presburger.IntegerRelation(...) eq = relation.equalities() eq[i, j] = X
No one is more of a fan of making these bindings more "pythonic" than me so I'll point out that if you take the def_property route I suggested below and just keep the "tableaus" as members of PyPresburgerIntegerRelation (one for equalities and one for inequalities), you'd be able to do
relation = mlir.presburger.IntegerRelation(...)
relation.at_eq[i, j] = Xand
relation = mlir.presburger.IntegerRelation(...)
relation.at_ineq[i, j] = Xwhich is a perfect compromise between "pythonic" and how these are used in C++.
I don't think that's true? They just hold
There are only two and I believe they're to prevent a use-after-free here: llvm-project/mlir/lib/Bindings/Python/Presburger.cpp Lines 48 to 52 in 0744372 I made a comment above that it would be simpler to just hoist |
|
(when the time comes, the ADT change should probably be pulled into a separate PR with unit test coverage) |
shelkesagar29
force-pushed
the
pburger_python
branch
from
0744372 to
4805c60
Compare
|
@christopherbate for vis |
shelkesagar29
force-pushed
the
pburger_python
branch
from
4805c60 to
f5acf65
Compare
|
✅ With the latest revision this PR passed the Python code formatter. |
shelkesagar29
force-pushed
the
pburger_python
branch
2 times, most recently
from
f06df51 to
0259456
Compare
| // IntegerRelation Dump | ||
| //===----------------------------------------------------------------------===// | ||
| MLIR_CAPI_EXPORTED void | ||
| mlirPresburgerIntegerRelationDump(MlirPresburgerIntegerRelation relation); |
There was a problem hiding this comment.
IntegerRelation has a print method, which should be prioritized over exposing this method.
The mlirPresburgerIntegerRelationPrint function should accept an opaque callback of type MlirStringCallback defined in mlir-c/Support.h allowing the caller to decide how to handle the string ref. That way you don't need to worry about how to pass a dynamically allocated string across the C API boundary.
| 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; |
There was a problem hiding this comment.
Co-author here. at64 on PyPresburgerIntegerRelation is ambiguous, are you referring to the equality matrix or inequality matrix? The intent was to allow creating an API like the following:
relation = mlir.presburger.IntegerRelation(...)
eq = relation.equalities()
eq[i, j] = XIntegeRelation internally stores equalities and inequalities as separate matrices of type presburger::IntMatrix. We could just expose IntMatrix as a separate C API as well, but currently IntegerRelation does not expose these IntMatrix objects directly in its public API. You can only access coefficients through IntegerRelation::atIneq|atEq methods.
Edit: the equalities[...] accessor method is not implemented here; I was hoping that could be added after the DynamicAPInt functionality was exposed, @shelkesagar29 can you add it?
That's right, the
I don't see how the tableau object could be eliminated if we want to keep the I think the current implementation is correct in terms of ensuring that The @shelkesagar29 We also probably want to add an explicit test for ensuring this is correct, some thing like |
Yes I'm proposing that the API be eliminated/hoisted. Note, I'm not proposing it be eliminated on principled grounds, like that there is no I'm proposing it be hoisted into
In fact the "correct" thing to do, if we decide the API is indeed worth the cognitive and maintenance cost, is to use
Or (as that doc alludes) to make this a |
shelkesagar29
force-pushed
the
pburger_python
branch
2 times, most recently
from
7c46e14 to
21c2ab8
Compare
c++ library This MR is work in progress.
shelkesagar29
force-pushed
the
pburger_python
branch
from
21c2ab8 to
8b6c8c2
Compare
| self.relation, pos, num); | ||
| }, | ||
| py::arg("pos"), py::arg("num")) | ||
| .def_property_readonly( |
There was a problem hiding this comment.
@makslevental
I have added relation.at_eq/ineq[I, j] API as you suggested.
However, this is readonly. Looks like we can't set individual element of internal IntMatrix.
If this is sufficient, which I think it is, we can remove equalities/inequalities methods.
There was a problem hiding this comment.
However, this is readonly. Looks like we can't set individual element of internal
You can make it writeable:
py::class_<Pet>(m, "Pet")
.def(py::init<const std::string &>())
.def_property("name", &Pet::getName, &Pet::setName)ctrl+f call the setter and getter functions @ https://pybind11.readthedocs.io/en/stable/classes.html
The key thing about pybind and the Python C API is that anything you can do in Python you can also do in the C API :) and so property getters/setters are possible through the C API.
I have added methods you suggested. Let me know what you think |
This MR is work in progress.
MR is created so that community is aware of ongoing work and repeated work is avoided.