[mlir][SMT] C APIs

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

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

@@ -0,0 +1,32 @@
+//===- mlir-c/Target/ExportSMTLIB.h - C API for emitting SMTLIB ---*- 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This header declares the C interface for emitting SMTLIB from an 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

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

mlir/lib/CAPI/Dialect/SMT.cpp

@@ -0,0 +1,123 @@
+//===- 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/SMTAttributes.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTTypes.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()));
+}

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

mlir/lib/CAPI/Target/ExportSMTLIB.cpp

@@ -0,0 +1,27 @@
+//===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===//
+//
+// 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.
+//
+//===----------------------------------------------------------------------===//
+
+#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));
+}

mlir/lib/Target/SMTLIB/CMakeLists.txt

@@ -11,5 +11,4 @@ add_mlir_translation_library(MLIRExportSMTLIB
   MLIRSMT
   MLIRSupport
   MLIRTranslateLib
-  MLIRArithDialect
 )

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