[SMT][python] enable python bindings (#8071)

include/circt-c/Dialect/SMT.h

@@ -0,0 +1,24 @@
+//===- SMT.h - C interface for the SMT dialect --------------------*- C -*-===//
+//
+// 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 CIRCT_C_DIALECT_SMT_H
+#define CIRCT_C_DIALECT_SMT_H
+
+#include "mlir-c/IR.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+MLIR_DECLARE_CAPI_DIALECT_REGISTRATION(SMT, smt);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // CIRCT_C_DIALECT_SMT_H

integration_test/Bindings/Python/dialects/smt.py

@@ -0,0 +1,17 @@
+# REQUIRES: bindings_python
+# RUN: %PYTHON% %s | FileCheck %s
+
+import circt
+
+from circt.dialects import smt
+from circt.ir import Context, Location, Module, InsertionPoint
+
+with Context() as ctx, Location.unknown():
+  circt.register_dialects(ctx)
+  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)

lib/Bindings/Python/CIRCTModule.cpp

@@ -26,6 +26,7 @@
 #ifdef CIRCT_INCLUDE_TESTS
 #include "circt-c/Dialect/RTGTest.h"
 #endif
+#include "circt-c/Dialect/SMT.h"
 #include "circt-c/Dialect/SV.h"
 #include "circt-c/Dialect/Seq.h"
 #include "circt-c/Dialect/Verif.h"
@@ -135,6 +136,10 @@ PYBIND11_MODULE(_circt, m) {
         MlirDialectHandle verif = mlirGetDialectHandle__verif__();
         mlirDialectHandleRegisterDialect(verif, context);
         mlirDialectHandleLoadDialect(verif, context);
+
+        MlirDialectHandle smt = mlirGetDialectHandle__smt__();
+        mlirDialectHandleRegisterDialect(smt, context);
+        mlirDialectHandleLoadDialect(smt, context);
       },
       "Register CIRCT dialects on a PyMlirContext.");
 

lib/Bindings/Python/CMakeLists.txt

@@ -45,6 +45,7 @@ set(PYTHON_BINDINGS_LINK_LIBS
   CIRCTCAPIRTG
   CIRCTCAPIRtgTool
   CIRCTCAPISeq
+  CIRCTCAPISMT
   CIRCTCAPISV
   CIRCTCAPIVerif
   MLIRCAPITransforms
@@ -212,6 +213,14 @@ declare_mlir_dialect_python_bindings(
     dialects/verif.py
   DIALECT_NAME verif)
 
+declare_mlir_dialect_python_bindings(
+  ADD_TO_PARENT CIRCTBindingsPythonSources.Dialects
+  ROOT_DIR "${CMAKE_CURRENT_SOURCE_DIR}"
+  TD_FILE dialects/SMTOps.td
+  SOURCES
+    dialects/smt.py
+  DIALECT_NAME smt)
+
 declare_mlir_dialect_python_bindings(
   ADD_TO_PARENT CIRCTBindingsPythonSources.Dialects
   ROOT_DIR "${CMAKE_CURRENT_SOURCE_DIR}"

lib/Bindings/Python/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 "circt/Dialect/SMT/SMT.td"
+
+#endif // BINDINGS_PYTHON_SMT_OPS

lib/Bindings/Python/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 *

lib/CAPI/Dialect/CMakeLists.txt

@@ -21,6 +21,7 @@ set(LLVM_OPTIONAL_SOURCES
   RTGTest.cpp
   SV.cpp
   Seq.cpp
+  SMT.cpp
   Verif.cpp
 )
 
@@ -224,3 +225,11 @@ add_circt_public_c_api_library(CIRCTCAPIEmit
   MLIRCAPIIR
   CIRCTEmit
 )
+
+add_circt_public_c_api_library(CIRCTCAPISMT
+  SMT.cpp
+
+  LINK_LIBS PUBLIC
+  MLIRCAPIIR
+  CIRCTSMT
+)

lib/CAPI/Dialect/SMT.cpp

@@ -0,0 +1,14 @@
+//===- SMT.cpp - C interface for the SMT dialect --------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt-c/Dialect/SMT.h"
+#include "circt/Dialect/SMT/SMTDialect.h"
+
+#include "mlir/CAPI/Registration.h"
+
+MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, circt::smt::SMTDialect)