[mlir][SMT] C APIs #135501

makslevental · 2025-04-12T21:13:18Z

This PR upstreams/adds the C APIs for SMT dialect (from CIRCT).

github-actions · 2025-04-12T21:15:37Z

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

llvmbot · 2025-04-12T21:40:07Z

@llvm/pr-subscribers-mlir

Author: Maksim Levental (makslevental)

Changes

Patch is 21.24 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/135501.diff

10 Files Affected:

(added) mlir/include/mlir-c/Dialect/SMT.h (+110)
(added) mlir/include/mlir-c/Target/ExportSMTLIB.h (+27)
(modified) mlir/lib/CAPI/Dialect/CMakeLists.txt (+9)
(added) mlir/lib/CAPI/Dialect/SMT.cpp (+122)
(modified) mlir/lib/CAPI/Target/CMakeLists.txt (+12)
(added) mlir/lib/CAPI/Target/ExportSMTLIB.cpp (+20)
(modified) mlir/lib/Target/SMTLIB/CMakeLists.txt (-1)
(modified) mlir/test/CAPI/CMakeLists.txt (+10)
(added) mlir/test/CAPI/smt.c (+182)
(modified) mlir/test/CMakeLists.txt (+1)

diff --git a/mlir/include/mlir-c/Dialect/SMT.h b/mlir/include/mlir-c/Dialect/SMT.h
new file mode 100644
index 0000000000000..d076dccce1b06
--- /dev/null
+++ b/mlir/include/mlir-c/Dialect/SMT.h
@@ -0,0 +1,110 @@
+//===- 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 MLIR_C_DIALECT_SMT_H
+#define MLIR_C_DIALECT_SMT_H
+
+#include "mlir-c/IR.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+//===----------------------------------------------------------------------===//
+// Dialect API.
+//===----------------------------------------------------------------------===//
+
+MLIR_DECLARE_CAPI_DIALECT_REGISTRATION(SMT, smt);
+
+//===----------------------------------------------------------------------===//
+// Type API.
+//===----------------------------------------------------------------------===//
+
+/// Checks if the given type is any non-func SMT value type.
+MLIR_CAPI_EXPORTED bool smtTypeIsAnyNonFuncSMTValueType(MlirType type);
+
+/// Checks if the given type is any SMT value type.
+MLIR_CAPI_EXPORTED bool smtTypeIsAnySMTValueType(MlirType type);
+
+/// Checks if the given type is a smt::ArrayType.
+MLIR_CAPI_EXPORTED bool smtTypeIsAArray(MlirType type);
+
+/// Creates an array type with the given domain and range types.
+MLIR_CAPI_EXPORTED MlirType smtTypeGetArray(MlirContext ctx,
+                                            MlirType domainType,
+                                            MlirType rangeType);
+
+/// Checks if the given type is a smt::BitVectorType.
+MLIR_CAPI_EXPORTED bool smtTypeIsABitVector(MlirType type);
+
+/// Creates a smt::BitVectorType with the given width.
+MLIR_CAPI_EXPORTED MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width);
+
+/// Checks if the given type is a smt::BoolType.
+MLIR_CAPI_EXPORTED bool smtTypeIsABool(MlirType type);
+
+/// Creates a smt::BoolType.
+MLIR_CAPI_EXPORTED MlirType smtTypeGetBool(MlirContext ctx);
+
+/// Checks if the given type is a smt::IntType.
+MLIR_CAPI_EXPORTED bool smtTypeIsAInt(MlirType type);
+
+/// Creates a smt::IntType.
+MLIR_CAPI_EXPORTED MlirType smtTypeGetInt(MlirContext ctx);
+
+/// Checks if the given type is a smt::FuncType.
+MLIR_CAPI_EXPORTED bool smtTypeIsASMTFunc(MlirType type);
+
+/// Creates a smt::FuncType with the given domain and range types.
+MLIR_CAPI_EXPORTED MlirType smtTypeGetSMTFunc(MlirContext ctx,
+                                              size_t numberOfDomainTypes,
+                                              const MlirType *domainTypes,
+                                              MlirType rangeType);
+
+/// Checks if the given type is a smt::SortType.
+MLIR_CAPI_EXPORTED bool smtTypeIsASort(MlirType type);
+
+/// Creates a smt::SortType with the given identifier and sort parameters.
+MLIR_CAPI_EXPORTED MlirType smtTypeGetSort(MlirContext ctx,
+                                           MlirIdentifier identifier,
+                                           size_t numberOfSortParams,
+                                           const MlirType *sortParams);
+
+//===----------------------------------------------------------------------===//
+// Attribute API.
+//===----------------------------------------------------------------------===//
+
+/// Checks if the given string is a valid smt::BVCmpPredicate.
+MLIR_CAPI_EXPORTED bool smtAttrCheckBVCmpPredicate(MlirContext ctx,
+                                                   MlirStringRef str);
+
+/// Checks if the given string is a valid smt::IntPredicate.
+MLIR_CAPI_EXPORTED bool smtAttrCheckIntPredicate(MlirContext ctx,
+                                                 MlirStringRef str);
+
+/// Checks if the given attribute is a smt::SMTAttribute.
+MLIR_CAPI_EXPORTED bool smtAttrIsASMTAttribute(MlirAttribute attr);
+
+/// Creates a smt::BitVectorAttr with the given value and width.
+MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetBitVector(MlirContext ctx,
+                                                     uint64_t value,
+                                                     unsigned width);
+
+/// Creates a smt::BVCmpPredicateAttr with the given string.
+MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetBVCmpPredicate(MlirContext ctx,
+                                                          MlirStringRef str);
+
+/// Creates a smt::IntPredicateAttr with the given string.
+MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetIntPredicate(MlirContext ctx,
+                                                        MlirStringRef str);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // MLIR_C_DIALECT_SMT_H
diff --git a/mlir/include/mlir-c/Target/ExportSMTLIB.h b/mlir/include/mlir-c/Target/ExportSMTLIB.h
new file mode 100644
index 0000000000000..ee893a9f89fe7
--- /dev/null
+++ b/mlir/include/mlir-c/Target/ExportSMTLIB.h
@@ -0,0 +1,27 @@
+//===- MLIR-c/ExportSMTLIB.h - C API for emitting SMTLIB ---------*- C -*-===//
+//
+// This header declares the C interface for emitting SMTLIB from a MLIR MLIR
+// module.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_C_EXPORTSMTLIB_H
+#define MLIR_C_EXPORTSMTLIB_H
+
+#include "mlir-c/IR.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/// Emits SMTLIB for the specified module using the provided callback and user
+/// data
+MLIR_CAPI_EXPORTED MlirLogicalResult mlirExportSMTLIB(MlirModule,
+                                                      MlirStringCallback,
+                                                      void *userData);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // MLIR_C_EXPORTSMTLIB_H
diff --git a/mlir/lib/CAPI/Dialect/CMakeLists.txt b/mlir/lib/CAPI/Dialect/CMakeLists.txt
index ddd3d6629a532..bb1fdf8be3c8f 100644
--- a/mlir/lib/CAPI/Dialect/CMakeLists.txt
+++ b/mlir/lib/CAPI/Dialect/CMakeLists.txt
@@ -269,3 +269,12 @@ add_mlir_upstream_c_api_library(MLIRCAPIVector
   MLIRCAPIIR
   MLIRVectorDialect
 )
+
+add_mlir_upstream_c_api_library(MLIRCAPISMT
+  SMT.cpp
+
+  PARTIAL_SOURCES_INTENDED
+  LINK_LIBS PUBLIC
+  MLIRCAPIIR
+  MLIRSMT
+)
diff --git a/mlir/lib/CAPI/Dialect/SMT.cpp b/mlir/lib/CAPI/Dialect/SMT.cpp
new file mode 100644
index 0000000000000..f4df81a97c012
--- /dev/null
+++ b/mlir/lib/CAPI/Dialect/SMT.cpp
@@ -0,0 +1,122 @@
+//===- 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 "mlir-c/Dialect/SMT.h"
+#include "mlir/CAPI/Registration.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+
+using namespace mlir;
+using namespace smt;
+
+//===----------------------------------------------------------------------===//
+// Dialect API.
+//===----------------------------------------------------------------------===//
+
+MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, mlir::smt::SMTDialect)
+
+//===----------------------------------------------------------------------===//
+// Type API.
+//===----------------------------------------------------------------------===//
+
+bool smtTypeIsAnyNonFuncSMTValueType(MlirType type) {
+  return isAnyNonFuncSMTValueType(unwrap(type));
+}
+
+bool smtTypeIsAnySMTValueType(MlirType type) {
+  return isAnySMTValueType(unwrap(type));
+}
+
+bool smtTypeIsAArray(MlirType type) { return isa<ArrayType>(unwrap(type)); }
+
+MlirType smtTypeGetArray(MlirContext ctx, MlirType domainType,
+                         MlirType rangeType) {
+  return wrap(
+      ArrayType::get(unwrap(ctx), unwrap(domainType), unwrap(rangeType)));
+}
+
+bool smtTypeIsABitVector(MlirType type) {
+  return isa<BitVectorType>(unwrap(type));
+}
+
+MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width) {
+  return wrap(BitVectorType::get(unwrap(ctx), width));
+}
+
+bool smtTypeIsABool(MlirType type) { return isa<BoolType>(unwrap(type)); }
+
+MlirType smtTypeGetBool(MlirContext ctx) {
+  return wrap(BoolType::get(unwrap(ctx)));
+}
+
+bool smtTypeIsAInt(MlirType type) { return isa<IntType>(unwrap(type)); }
+
+MlirType smtTypeGetInt(MlirContext ctx) {
+  return wrap(IntType::get(unwrap(ctx)));
+}
+
+bool smtTypeIsASMTFunc(MlirType type) { return isa<SMTFuncType>(unwrap(type)); }
+
+MlirType smtTypeGetSMTFunc(MlirContext ctx, size_t numberOfDomainTypes,
+                           const MlirType *domainTypes, MlirType rangeType) {
+  SmallVector<Type> domainTypesVec;
+  domainTypesVec.reserve(numberOfDomainTypes);
+
+  for (size_t i = 0; i < numberOfDomainTypes; i++)
+    domainTypesVec.push_back(unwrap(domainTypes[i]));
+
+  return wrap(SMTFuncType::get(unwrap(ctx), domainTypesVec, unwrap(rangeType)));
+}
+
+bool smtTypeIsASort(MlirType type) { return isa<SortType>(unwrap(type)); }
+
+MlirType smtTypeGetSort(MlirContext ctx, MlirIdentifier identifier,
+                        size_t numberOfSortParams, const MlirType *sortParams) {
+  SmallVector<Type> sortParamsVec;
+  sortParamsVec.reserve(numberOfSortParams);
+
+  for (size_t i = 0; i < numberOfSortParams; i++)
+    sortParamsVec.push_back(unwrap(sortParams[i]));
+
+  return wrap(SortType::get(unwrap(ctx), unwrap(identifier), sortParamsVec));
+}
+
+//===----------------------------------------------------------------------===//
+// Attribute API.
+//===----------------------------------------------------------------------===//
+
+bool smtAttrCheckBVCmpPredicate(MlirContext ctx, MlirStringRef str) {
+  return symbolizeBVCmpPredicate(unwrap(str)).has_value();
+}
+
+bool smtAttrCheckIntPredicate(MlirContext ctx, MlirStringRef str) {
+  return symbolizeIntPredicate(unwrap(str)).has_value();
+}
+
+bool smtAttrIsASMTAttribute(MlirAttribute attr) {
+  return isa<BitVectorAttr, BVCmpPredicateAttr, IntPredicateAttr>(unwrap(attr));
+}
+
+MlirAttribute smtAttrGetBitVector(MlirContext ctx, uint64_t value,
+                                  unsigned width) {
+  return wrap(BitVectorAttr::get(unwrap(ctx), value, width));
+}
+
+MlirAttribute smtAttrGetBVCmpPredicate(MlirContext ctx, MlirStringRef str) {
+  auto predicate = symbolizeBVCmpPredicate(unwrap(str));
+  assert(predicate.has_value() && "invalid predicate");
+
+  return wrap(BVCmpPredicateAttr::get(unwrap(ctx), predicate.value()));
+}
+
+MlirAttribute smtAttrGetIntPredicate(MlirContext ctx, MlirStringRef str) {
+  auto predicate = symbolizeIntPredicate(unwrap(str));
+  assert(predicate.has_value() && "invalid predicate");
+
+  return wrap(IntPredicateAttr::get(unwrap(ctx), predicate.value()));
+}
diff --git a/mlir/lib/CAPI/Target/CMakeLists.txt b/mlir/lib/CAPI/Target/CMakeLists.txt
index ea617da72261b..8fbb7aa954d9e 100644
--- a/mlir/lib/CAPI/Target/CMakeLists.txt
+++ b/mlir/lib/CAPI/Target/CMakeLists.txt
@@ -1,6 +1,8 @@
 add_mlir_upstream_c_api_library(MLIRCAPITarget
   LLVMIR.cpp
 
+  PARTIAL_SOURCES_INTENDED
+
   LINK_COMPONENTS
   Core
 
@@ -11,3 +13,13 @@ add_mlir_upstream_c_api_library(MLIRCAPITarget
   MLIRLLVMIRToLLVMTranslation
   MLIRSupport
 )
+
+add_mlir_upstream_c_api_library(MLIRCAPIExportSMTLIB
+  ExportSMTLIB.cpp
+
+  PARTIAL_SOURCES_INTENDED
+
+  LINK_LIBS PUBLIC
+  MLIRCAPIIR
+  MLIRExportSMTLIB
+)
diff --git a/mlir/lib/CAPI/Target/ExportSMTLIB.cpp b/mlir/lib/CAPI/Target/ExportSMTLIB.cpp
new file mode 100644
index 0000000000000..ab5350a1ec698
--- /dev/null
+++ b/mlir/lib/CAPI/Target/ExportSMTLIB.cpp
@@ -0,0 +1,20 @@
+//===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===//
+//
+//  Implements a C Interface for export SMTLIB.
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir-c/Target/ExportSMTLIB.h"
+#include "mlir/CAPI/IR.h"
+#include "mlir/CAPI/Support.h"
+#include "mlir/CAPI/Utils.h"
+#include "mlir/Target/SMTLIB/ExportSMTLIB.h"
+
+using namespace mlir;
+
+MlirLogicalResult mlirExportSMTLIB(MlirModule module,
+                                   MlirStringCallback callback,
+                                   void *userData) {
+  mlir::detail::CallbackOstream stream(callback, userData);
+  return wrap(smt::exportSMTLIB(unwrap(module), stream));
+}
diff --git a/mlir/lib/Target/SMTLIB/CMakeLists.txt b/mlir/lib/Target/SMTLIB/CMakeLists.txt
index c17d09bd6e230..4f47bef8e26ce 100644
--- a/mlir/lib/Target/SMTLIB/CMakeLists.txt
+++ b/mlir/lib/Target/SMTLIB/CMakeLists.txt
@@ -11,5 +11,4 @@ add_mlir_translation_library(MLIRExportSMTLIB
   MLIRSMT
   MLIRSupport
   MLIRTranslateLib
-  MLIRArithDialect
 )
diff --git a/mlir/test/CAPI/CMakeLists.txt b/mlir/test/CAPI/CMakeLists.txt
index e795672bce5d1..9466497b18e89 100644
--- a/mlir/test/CAPI/CMakeLists.txt
+++ b/mlir/test/CAPI/CMakeLists.txt
@@ -123,3 +123,13 @@ _add_capi_test_executable(mlir-capi-translation-test
     MLIRCAPIRegisterEverything
     MLIRCAPITarget
 )
+
+_add_capi_test_executable(mlir-capi-smt-test
+  smt.c
+
+  LINK_LIBS PRIVATE
+    MLIRCAPIIR
+    MLIRCAPIFunc
+    MLIRCAPISMT
+    MLIRCAPIExportSMTLIB
+)
\ No newline at end of file
diff --git a/mlir/test/CAPI/smt.c b/mlir/test/CAPI/smt.c
new file mode 100644
index 0000000000000..32890fef8b1d7
--- /dev/null
+++ b/mlir/test/CAPI/smt.c
@@ -0,0 +1,182 @@
+
+/*===- smtlib.c - Simple test of SMTLIB C API -----------------------------===*\
+|*                                                                            *|
+|* 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                    *|
+|*                                                                            *|
+\*===----------------------------------------------------------------------===*/
+
+/* RUN: mlir-capi-smt-test 2>&1 | FileCheck %s
+ */
+
+#include "mlir-c/Dialect/SMT.h"
+#include "mlir-c/Dialect/Func.h"
+#include "mlir-c/IR.h"
+#include "mlir-c/Support.h"
+#include "mlir-c/Target/ExportSMTLIB.h"
+#include <assert.h>
+#include <stdio.h>
+
+void dumpCallback(MlirStringRef message, void *userData) {
+  fprintf(stderr, "%.*s", (int)message.length, message.data);
+}
+
+void testExportSMTLIB(MlirContext ctx) {
+  // clang-format off
+  const char *testSMT = 
+    "func.func @test() {\n"
+    "  smt.solver() : () -> () { }\n"
+    "  return\n"
+    "}\n";
+  // clang-format on
+
+  MlirModule module =
+      mlirModuleCreateParse(ctx, mlirStringRefCreateFromCString(testSMT));
+
+  MlirLogicalResult result = mlirExportSMTLIB(module, dumpCallback, NULL);
+  (void)result;
+  assert(mlirLogicalResultIsSuccess(result));
+
+  // CHECK: ; solver scope 0
+  // CHECK-NEXT: (reset)
+}
+
+void testSMTType(MlirContext ctx) {
+  MlirType boolType = smtTypeGetBool(ctx);
+  MlirType intType = smtTypeGetInt(ctx);
+  MlirType arrayType = smtTypeGetArray(ctx, intType, boolType);
+  MlirType bvType = smtTypeGetBitVector(ctx, 32);
+  MlirType funcType =
+      smtTypeGetSMTFunc(ctx, 2, (MlirType[]){intType, boolType}, boolType);
+  MlirType sortType = smtTypeGetSort(
+      ctx, mlirIdentifierGet(ctx, mlirStringRefCreateFromCString("sort")), 0,
+      NULL);
+
+  // CHECK: !smt.bool
+  mlirTypeDump(boolType);
+  // CHECK: !smt.int
+  mlirTypeDump(intType);
+  // CHECK: !smt.array<[!smt.int -> !smt.bool]>
+  mlirTypeDump(arrayType);
+  // CHECK: !smt.bv<32>
+  mlirTypeDump(bvType);
+  // CHECK: !smt.func<(!smt.int, !smt.bool) !smt.bool>
+  mlirTypeDump(funcType);
+  // CHECK: !smt.sort<"sort">
+  mlirTypeDump(sortType);
+
+  // CHECK: bool_is_any_non_func_smt_value_type
+  fprintf(stderr, smtTypeIsAnyNonFuncSMTValueType(boolType)
+                      ? "bool_is_any_non_func_smt_value_type\n"
+                      : "bool_is_func_smt_value_type\n");
+  // CHECK: int_is_any_non_func_smt_value_type
+  fprintf(stderr, smtTypeIsAnyNonFuncSMTValueType(intType)
+                      ? "int_is_any_non_func_smt_value_type\n"
+                      : "int_is_func_smt_value_type\n");
+  // CHECK: array_is_any_non_func_smt_value_type
+  fprintf(stderr, smtTypeIsAnyNonFuncSMTValueType(arrayType)
+                      ? "array_is_any_non_func_smt_value_type\n"
+                      : "array_is_func_smt_value_type\n");
+  // CHECK: bit_vector_is_any_non_func_smt_value_type
+  fprintf(stderr, smtTypeIsAnyNonFuncSMTValueType(bvType)
+                      ? "bit_vector_is_any_non_func_smt_value_type\n"
+                      : "bit_vector_is_func_smt_value_type\n");
+  // CHECK: sort_is_any_non_func_smt_value_type
+  fprintf(stderr, smtTypeIsAnyNonFuncSMTValueType(sortType)
+                      ? "sort_is_any_non_func_smt_value_type\n"
+                      : "sort_is_func_smt_value_type\n");
+  // CHECK: smt_func_is_func_smt_value_type
+  fprintf(stderr, smtTypeIsAnyNonFuncSMTValueType(funcType)
+                      ? "smt_func_is_any_non_func_smt_value_type\n"
+                      : "smt_func_is_func_smt_value_type\n");
+
+  // CHECK: bool_is_any_smt_value_type
+  fprintf(stderr, smtTypeIsAnySMTValueType(boolType)
+                      ? "bool_is_any_smt_value_type\n"
+                      : "bool_is_not_any_smt_value_type\n");
+  // CHECK: int_is_any_smt_value_type
+  fprintf(stderr, smtTypeIsAnySMTValueType(intType)
+                      ? "int_is_any_smt_value_type\n"
+                      : "int_is_not_any_smt_value_type\n");
+  // CHECK: array_is_any_smt_value_type
+  fprintf(stderr, smtTypeIsAnySMTValueType(arrayType)
+                      ? "array_is_any_smt_value_type\n"
+                      : "array_is_not_any_smt_value_type\n");
+  // CHECK: array_is_any_smt_value_type
+  fprintf(stderr, smtTypeIsAnySMTValueType(bvType)
+                      ? "array_is_any_smt_value_type\n"
+                      : "array_is_not_any_smt_value_type\n");
+  // CHECK: smt_func_is_any_smt_value_type
+  fprintf(stderr, smtTypeIsAnySMTValueType(funcType)
+                      ? "smt_func_is_any_smt_value_type\n"
+                      : "smt_func_is_not_any_smt_value_type\n");
+  // CHECK: sort_is_any_smt_value_type
+  fprintf(stderr, smtTypeIsAnySMTValueType(sortType)
+                      ? "sort_is_any_smt_value_type\n"
+                      : "sort_is_not_any_smt_value_type\n");
+
+  // CHECK: int_type_is_not_a_bool
+  fprintf(stderr, smtTypeIsABool(intType) ? "int_type_is_a_bool\n"
+                                          : "int_type_is_not_a_bool\n");
+  // CHECK: bool_type_is_not_a_int
+  fprintf(stderr, smtTypeIsAInt(boolType) ? "bool_type_is_a_int\n"
+                                          : "bool_type_is_not_a_int\n");
+  // CHECK: bv_type_is_not_a_array
+  fprintf(stderr, smtTypeIsAArray(bvType) ? "bv_type_is_a_array\n"
+                                          : "bv_type_is_not_a_array\n");
+  // CHECK: array_type_is_not_a_bit_vector
+  fprintf(stderr, smtTypeIsABitVector(arrayType)
+                      ? "array_type_is_a_bit_vector\n"
+                      : "array_type_is_not_a_bit_vector\n");
+  // CHECK: sort_type_is_not_a_smt_func
+  fprintf(stderr, smtTypeIsASMTFunc(sortType)
+                      ? "sort_type_is_a_smt_func\n"
+                      : "sort_type_is_not_a_smt_func\n");
+  // CHECK: func_type_is_not_a_sort
+  fprintf(stderr, smtTypeIsASort(funcType) ? "func_type_is_a_sort\n"
+                                           : "func_type_is_not_a_sort\n");
+}
+
+void testSMTAttribute(MlirContext ctx) {
+  // CHECK: slt_is_BVCmpPredicate
+  fprintf(stderr,
+          smtAttrCheckBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt"))
+              ? "slt_is_BVCmpPredicate\n"
+              : "slt_is_not_BVCmpPredicate\n");
+  // CHECK: lt_is_not_BVCmpPredicate
+  fprintf(stderr,
+          smtAttrCheckBVCmpPredicate(ctx, mlirStringRefCreateFromCString("lt"))
+              ? "lt_is_BVCmpPredicate\n"
+              : "lt_is_not_BVCmpPredicate\n");
+  // CHECK: slt_is_not_IntPredicate
+  fprintf(stderr,
+          smtAttrCheckIntPredicate(ctx, mlirStringRefCreateFromCString("slt"))
+              ? "slt_is_IntPredicate\n"
+              : "slt_...
[truncated]

Co-authored-by: Bea Healy <[email protected]> Co-authored-by: Martin Erhart <[email protected]> Co-authored-by: Mike Urbach <[email protected]> Co-authored-by: Will Dietz <[email protected]> Co-authored-by: fzi-hielscher <[email protected]> Co-authored-by: Fehr Mathieu <[email protected]>

maerhart

LGTM! You should probably run git blame over the CAPI files again. I think there were 1 or 2 people contributing most of the CAPI that aren't mentioned as co-authors of the commit.

maerhart · 2025-04-14T15:16:19Z

mlir/include/mlir-c/Target/ExportSMTLIB.h

+// This header declares the C interface for emitting SMTLIB from a MLIR MLIR
+// module.


Shouldn't here be the license header instead?

maerhart · 2025-04-14T15:19:11Z

mlir/lib/CAPI/Dialect/SMT.cpp

+#include "mlir-c/Dialect/SMT.h"
+#include "mlir/CAPI/Registration.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTOps.h"


Nit: including SMTTypes.h and SMTAttributes.h instead of SMTOps.h should usually be enough.

maerhart · 2025-04-14T15:24:05Z

mlir/test/CAPI/smt.c

+/*===- smtlib.c - Simple test of SMTLIB C API -----------------------------===*\
+|*                                                                            *|
+|* 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                    *|
+|*                                                                            *|
+\*===----------------------------------------------------------------------===*/


Nit: the filename doesn't match and the way it is commented out is not really consistent with the other files in this directory

maerhart · 2025-04-14T15:25:32Z

mlir/lib/CAPI/Target/ExportSMTLIB.cpp

@@ -0,0 +1,20 @@
+//===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===//
+//
+//  Implements a C Interface for export SMTLIB.


Shouldn't here be the license header instead?

Co-authored-by: Bea Healy <[email protected]> Co-authored-by: Martin Erhart <[email protected]> Co-authored-by: Mike Urbach <[email protected]> Co-authored-by: Will Dietz <[email protected]> Co-authored-by: fzi-hielscher <[email protected]> Co-authored-by: Fehr Mathieu <[email protected]> Co-authored-by: Clo91eaf <[email protected]>

This PR upstreams/adds the C APIs for SMT dialect (from CIRCT). --------- Co-authored-by: Bea Healy <[email protected]> Co-authored-by: Martin Erhart <[email protected]> Co-authored-by: Mike Urbach <[email protected]> Co-authored-by: Will Dietz <[email protected]> Co-authored-by: fzi-hielscher <[email protected]> Co-authored-by: Fehr Mathieu <[email protected]> Co-authored-by: Clo91eaf <[email protected]>

makslevental force-pushed the makslevental/export-smtlib-capi branch from 4fba3b9 to 8443066 Compare April 12, 2025 21:34

makslevental mentioned this pull request Apr 12, 2025

[MLIR] Fix build after #131492 #135502

Merged

makslevental force-pushed the makslevental/export-smtlib-capi branch from 8443066 to e69f43c Compare April 12, 2025 21:38

makslevental requested review from jplehr and math-fehr April 12, 2025 21:39

makslevental marked this pull request as ready for review April 12, 2025 21:39

llvmbot added the mlir label Apr 12, 2025

makslevental force-pushed the makslevental/export-smtlib-capi branch from e69f43c to abdb4df Compare April 12, 2025 21:40

makslevental requested a review from maerhart April 12, 2025 21:41

makslevental force-pushed the makslevental/export-smtlib-capi branch from abdb4df to 2385b7a Compare April 12, 2025 21:42

makslevental and others added 2 commits April 12, 2025 17:44

remove extra MLIRArithDialect

dd1dd10

makslevental force-pushed the makslevental/export-smtlib-capi branch from 2385b7a to dd1dd10 Compare April 12, 2025 21:44

fix smt.c memory leak

63b2381

maerhart approved these changes Apr 14, 2025

View reviewed changes

makslevental force-pushed the makslevental/export-smtlib-capi branch from 54e8e63 to 4aac444 Compare April 14, 2025 18:38

makslevental merged commit 9deb08a into llvm:main Apr 14, 2025
11 checks passed

makslevental deleted the makslevental/export-smtlib-capi branch April 17, 2025 01:11

Clo91eaf mentioned this pull request Apr 23, 2025

Bump llvm and move smt dialect from circt to mlir sequencer/zaozi#30

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[mlir][SMT] C APIs #135501

[mlir][SMT] C APIs #135501

Uh oh!

makslevental commented Apr 12, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Apr 12, 2025 •

edited

Loading

Uh oh!

llvmbot commented Apr 12, 2025

Uh oh!

maerhart left a comment

Uh oh!

maerhart Apr 14, 2025

Uh oh!

maerhart Apr 14, 2025

Uh oh!

maerhart Apr 14, 2025

Uh oh!

maerhart Apr 14, 2025

Uh oh!

Uh oh!

Uh oh!

		// This header declares the C interface for emitting SMTLIB from a MLIR MLIR
		// module.

[mlir][SMT] C APIs #135501

[mlir][SMT] C APIs #135501

Uh oh!

Conversation

makslevental commented Apr 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

llvmbot commented Apr 12, 2025

Uh oh!

maerhart left a comment

Choose a reason for hiding this comment

Uh oh!

maerhart Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

maerhart Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

maerhart Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

maerhart Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

makslevental commented Apr 12, 2025 •

edited

Loading

github-actions bot commented Apr 12, 2025 •

edited

Loading