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

[llvmlistbot at llvm.org]

llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-mlir

Author: Maksim Levental (makslevental)

<details>
<summary>Changes</summary>

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
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)

``````````

</details>


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