[mlir][SMT] add python bindings

[makslevental]

This PR adds "rich" python bindings to SMT dialect.

Note, this commit cc99ede is NFC and renames SMT C APIs to be more aligned with our conventions (prefix with mlir) and could be split out but it was useful/needed here to write the bindings in DialectSMT.cpp "correctly".

[github-actions]

✅ With the latest revision this PR passed the Python code formatter.

[llvmbot]

@llvm/pr-subscribers-mlir

Author: Maksim Levental (makslevental)

Changes

TODO: add test of -export-smtlib

---

Full diff: https://github.com/llvm/llvm-project/pull/135674.diff

4 Files Affected:

• (modified) mlir/python/CMakeLists.txt (+9)
• (added) mlir/python/mlir/dialects/SMTOps.td (+14)
• (added) mlir/python/mlir/dialects/smt.py (+5)
• (added) mlir/test/python/dialects/smt.py (+16)

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)

[ftynse]

LGTM as long as the commit message is updated

[math-fehr]

Cool, thanks a lot!

[github-actions]

✅ With the latest revision this PR passed the C/C++ code formatter.