[Mlir-commits] [mlir] [mlir][SMT] add python bindings (PR #135674)

[Maksim Levental]

https://github.com/makslevental updated https://github.com/llvm/llvm-project/pull/135674

>From 3ba88a0333a158eac9ed6ce93fa738ade4477e89 Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Mon, 14 Apr 2025 16:35:40 -0400
Subject: [PATCH] [mlir][SMT] add python bindings

---
 mlir/python/CMakeLists.txt          |  9 +++++++++
 mlir/python/mlir/dialects/SMTOps.td | 14 ++++++++++++++
 mlir/python/mlir/dialects/smt.py    |  5 +++++
 mlir/test/python/dialects/smt.py    | 16 ++++++++++++++++
 4 files changed, 44 insertions(+)
 create mode 100644 mlir/python/mlir/dialects/SMTOps.td
 create mode 100644 mlir/python/mlir/dialects/smt.py
 create mode 100644 mlir/test/python/dialects/smt.py

diff --git a/mlir/python/CMakeLists.txt b/mlir/python/CMakeLists.txt
index fb115a5f43423..3985668486931 100644
--- a/mlir/python/CMakeLists.txt
+++ b/mlir/python/CMakeLists.txt
@@ -403,6 +403,15 @@ declare_mlir_dialect_python_bindings(
     "../../include/mlir/Dialect/SparseTensor/IR/SparseTensorAttrDefs.td"
 )
 
+declare_mlir_dialect_python_bindings(
+  ADD_TO_PARENT MLIRPythonSources.Dialects
+  ROOT_DIR "${CMAKE_CURRENT_SOURCE_DIR}/mlir"
+  TD_FILE dialects/SMTOps.td
+  GEN_ENUM_BINDINGS
+  SOURCES
+    dialects/smt.py
+  DIALECT_NAME smt)
+
 declare_mlir_dialect_python_bindings(
     ADD_TO_PARENT MLIRPythonSources.Dialects
     ROOT_DIR "${CMAKE_CURRENT_SOURCE_DIR}/mlir"
diff --git a/mlir/python/mlir/dialects/SMTOps.td b/mlir/python/mlir/dialects/SMTOps.td
new file mode 100644
index 0000000000000..e143f071eb658
--- /dev/null
+++ b/mlir/python/mlir/dialects/SMTOps.td
@@ -0,0 +1,14 @@
+//===- SMTOps.td - Entry point for SMT bindings ------------*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef BINDINGS_PYTHON_SMT_OPS
+#define BINDINGS_PYTHON_SMT_OPS
+
+include "mlir/Dialect/SMT/IR/SMT.td"
+
+#endif // BINDINGS_PYTHON_SMT_OPS
diff --git a/mlir/python/mlir/dialects/smt.py b/mlir/python/mlir/dialects/smt.py
new file mode 100644
index 0000000000000..7948486988b4c
--- /dev/null
+++ b/mlir/python/mlir/dialects/smt.py
@@ -0,0 +1,5 @@
+#  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
+
+from ._smt_ops_gen import *
diff --git a/mlir/test/python/dialects/smt.py b/mlir/test/python/dialects/smt.py
new file mode 100644
index 0000000000000..3e10f3ca35321
--- /dev/null
+++ b/mlir/test/python/dialects/smt.py
@@ -0,0 +1,16 @@
+# REQUIRES: bindings_python
+# RUN: %PYTHON% %s | FileCheck %s
+
+import mlir
+
+from mlir.dialects import smt
+from mlir.ir import Context, Location, Module, InsertionPoint
+
+with Context() as ctx, Location.unknown():
+    m = Module.create()
+    with InsertionPoint(m.body):
+        true = smt.constant(True)
+        false = smt.constant(False)
+    # CHECK: smt.constant true
+    # CHECK: smt.constant false
+    print(m)