From a43de90f40e6db7e4b6bb3c9e1783f4ece331a80 Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Sat, 12 Apr 2025 17:07:14 -0400 Subject: [PATCH 1/4] [mlir][SMT] C APIs Co-authored-by: Bea Healy Co-authored-by: Martin Erhart Co-authored-by: Mike Urbach Co-authored-by: Will Dietz Co-authored-by: fzi-hielscher Co-authored-by: Fehr Mathieu --- mlir/include/mlir-c/Dialect/SMT.h | 110 +++++++++++++ mlir/include/mlir-c/Target/ExportSMTLIB.h | 27 ++++ mlir/lib/CAPI/Dialect/CMakeLists.txt | 9 ++ mlir/lib/CAPI/Dialect/SMT.cpp | 122 +++++++++++++++ mlir/lib/CAPI/Target/CMakeLists.txt | 12 ++ mlir/lib/CAPI/Target/ExportSMTLIB.cpp | 20 +++ mlir/test/CAPI/CMakeLists.txt | 10 ++ mlir/test/CAPI/smt.c | 182 ++++++++++++++++++++++ mlir/test/CMakeLists.txt | 1 + 9 files changed, 493 insertions(+) create mode 100644 mlir/include/mlir-c/Dialect/SMT.h create mode 100644 mlir/include/mlir-c/Target/ExportSMTLIB.h create mode 100644 mlir/lib/CAPI/Dialect/SMT.cpp create mode 100644 mlir/lib/CAPI/Target/ExportSMTLIB.cpp create mode 100644 mlir/test/CAPI/smt.c 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(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(unwrap(type)); +} + +MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width) { + return wrap(BitVectorType::get(unwrap(ctx), width)); +} + +bool smtTypeIsABool(MlirType type) { return isa(unwrap(type)); } + +MlirType smtTypeGetBool(MlirContext ctx) { + return wrap(BoolType::get(unwrap(ctx))); +} + +bool smtTypeIsAInt(MlirType type) { return isa(unwrap(type)); } + +MlirType smtTypeGetInt(MlirContext ctx) { + return wrap(IntType::get(unwrap(ctx))); +} + +bool smtTypeIsASMTFunc(MlirType type) { return isa(unwrap(type)); } + +MlirType smtTypeGetSMTFunc(MlirContext ctx, size_t numberOfDomainTypes, + const MlirType *domainTypes, MlirType rangeType) { + SmallVector 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(unwrap(type)); } + +MlirType smtTypeGetSort(MlirContext ctx, MlirIdentifier identifier, + size_t numberOfSortParams, const MlirType *sortParams) { + SmallVector 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(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/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 +#include + +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_is_not_IntPredicate\n"); + // CHECK: lt_is_IntPredicate + fprintf(stderr, + smtAttrCheckIntPredicate(ctx, mlirStringRefCreateFromCString("lt")) + ? "lt_is_IntPredicate\n" + : "lt_is_not_IntPredicate\n"); + + // CHECK: #smt.bv<5> : !smt.bv<32> + mlirAttributeDump(smtAttrGetBitVector(ctx, 5, 32)); + // CHECK: 0 : i64 + mlirAttributeDump( + smtAttrGetBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt"))); + // CHECK: 0 : i64 + mlirAttributeDump( + smtAttrGetIntPredicate(ctx, mlirStringRefCreateFromCString("lt"))); +} + +int main(void) { + MlirContext ctx = mlirContextCreate(); + mlirDialectHandleLoadDialect(mlirGetDialectHandle__smt__(), ctx); + mlirDialectHandleLoadDialect(mlirGetDialectHandle__func__(), ctx); + testExportSMTLIB(ctx); + testSMTType(ctx); + testSMTAttribute(ctx); + return 0; +} diff --git a/mlir/test/CMakeLists.txt b/mlir/test/CMakeLists.txt index a4aa6e1677bef..ac8b44f53aebf 100644 --- a/mlir/test/CMakeLists.txt +++ b/mlir/test/CMakeLists.txt @@ -105,6 +105,7 @@ set(MLIR_TEST_DEPENDS mlir-capi-pass-test mlir-capi-quant-test mlir-capi-rewrite-test + mlir-capi-smt-test mlir-capi-sparse-tensor-test mlir-capi-transform-test mlir-capi-transform-interpreter-test From dd1dd10e097d1fec44453cf5e2e6d04d58557ae9 Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Sat, 12 Apr 2025 17:38:05 -0400 Subject: [PATCH 2/4] remove extra MLIRArithDialect --- mlir/lib/Target/SMTLIB/CMakeLists.txt | 1 - mlir/test/CAPI/CMakeLists.txt | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) 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 9466497b18e89..a7f9eb9b4efe8 100644 --- a/mlir/test/CAPI/CMakeLists.txt +++ b/mlir/test/CAPI/CMakeLists.txt @@ -132,4 +132,4 @@ _add_capi_test_executable(mlir-capi-smt-test MLIRCAPIFunc MLIRCAPISMT MLIRCAPIExportSMTLIB -) \ No newline at end of file +) From 63b23811179186d3da9909bacb13b8a9ed533c5d Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Sat, 12 Apr 2025 18:09:29 -0400 Subject: [PATCH 3/4] fix smt.c memory leak --- mlir/test/CAPI/smt.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/mlir/test/CAPI/smt.c b/mlir/test/CAPI/smt.c index 32890fef8b1d7..2efb8be2da188 100644 --- a/mlir/test/CAPI/smt.c +++ b/mlir/test/CAPI/smt.c @@ -41,6 +41,7 @@ void testExportSMTLIB(MlirContext ctx) { // CHECK: ; solver scope 0 // CHECK-NEXT: (reset) + mlirModuleDestroy(module); } void testSMTType(MlirContext ctx) { @@ -178,5 +179,8 @@ int main(void) { testExportSMTLIB(ctx); testSMTType(ctx); testSMTAttribute(ctx); + + mlirContextDestroy(ctx); + return 0; } From 4aac44441c71ae80cfca7dce55c177d8105cb9d7 Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Mon, 14 Apr 2025 14:01:47 -0400 Subject: [PATCH 4/4] header comments Co-authored-by: Bea Healy Co-authored-by: Martin Erhart Co-authored-by: Mike Urbach Co-authored-by: Will Dietz Co-authored-by: fzi-hielscher Co-authored-by: Fehr Mathieu Co-authored-by: Clo91eaf --- mlir/include/mlir-c/Target/ExportSMTLIB.h | 11 ++++++++--- mlir/lib/CAPI/Dialect/SMT.cpp | 3 ++- mlir/lib/CAPI/Target/ExportSMTLIB.cpp | 9 ++++++++- mlir/test/CAPI/smt.c | 17 ++++++++--------- 4 files changed, 26 insertions(+), 14 deletions(-) diff --git a/mlir/include/mlir-c/Target/ExportSMTLIB.h b/mlir/include/mlir-c/Target/ExportSMTLIB.h index ee893a9f89fe7..31f411c4a89c2 100644 --- a/mlir/include/mlir-c/Target/ExportSMTLIB.h +++ b/mlir/include/mlir-c/Target/ExportSMTLIB.h @@ -1,7 +1,12 @@ -//===- MLIR-c/ExportSMTLIB.h - C API for emitting SMTLIB ---------*- C -*-===// +//===- mlir-c/Target/ExportSMTLIB.h - C API for emitting SMTLIB ---*- C -*-===// // -// This header declares the C interface for emitting SMTLIB from a MLIR MLIR -// module. +// 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 +// +//===----------------------------------------------------------------------===// +// +// This header declares the C interface for emitting SMTLIB from an MLIR module. // //===----------------------------------------------------------------------===// diff --git a/mlir/lib/CAPI/Dialect/SMT.cpp b/mlir/lib/CAPI/Dialect/SMT.cpp index f4df81a97c012..3a4620df8ccdf 100644 --- a/mlir/lib/CAPI/Dialect/SMT.cpp +++ b/mlir/lib/CAPI/Dialect/SMT.cpp @@ -8,8 +8,9 @@ #include "mlir-c/Dialect/SMT.h" #include "mlir/CAPI/Registration.h" +#include "mlir/Dialect/SMT/IR/SMTAttributes.h" #include "mlir/Dialect/SMT/IR/SMTDialect.h" -#include "mlir/Dialect/SMT/IR/SMTOps.h" +#include "mlir/Dialect/SMT/IR/SMTTypes.h" using namespace mlir; using namespace smt; diff --git a/mlir/lib/CAPI/Target/ExportSMTLIB.cpp b/mlir/lib/CAPI/Target/ExportSMTLIB.cpp index ab5350a1ec698..c9ac7ce704af8 100644 --- a/mlir/lib/CAPI/Target/ExportSMTLIB.cpp +++ b/mlir/lib/CAPI/Target/ExportSMTLIB.cpp @@ -1,6 +1,13 @@ //===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===// // -// Implements a C Interface for export SMTLIB. +// 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 +// +//===----------------------------------------------------------------------===// +// +// Implements a C Interface for export SMTLIB. // //===----------------------------------------------------------------------===// diff --git a/mlir/test/CAPI/smt.c b/mlir/test/CAPI/smt.c index 2efb8be2da188..77815d4f79657 100644 --- a/mlir/test/CAPI/smt.c +++ b/mlir/test/CAPI/smt.c @@ -1,12 +1,11 @@ - -/*===- 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 *| -|* *| -\*===----------------------------------------------------------------------===*/ +//===- smt.c - Test of SMT APIs -------------------------------------------===// +// +// 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 */