[llvm] [mlir] [Python] Develop python bindings for Presburger library (PR #113233)

Christopher Bate via llvm-commits llvm-commits at lists.llvm.org
Thu Nov 14 10:24:27 PST 2024


================
@@ -0,0 +1,295 @@
+#include "mlir-c/Presburger.h"
+#include "mlir-c/Bindings/Python/Interop.h"
+#include "llvm/ADT/ScopeExit.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();
+  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;
----------------
christopherbate wrote:

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: 

```python
relation = mlir.presburger.IntegerRelation(...)
eq = relation.equalities() 
eq[i, j] = X
```

IntegeRelation 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.

https://github.com/llvm/llvm-project/pull/113233


More information about the llvm-commits mailing list