[Mlir-commits] [mlir] [mlir][SMT] C APIs (PR #135501)
Maksim Levental
llvmlistbot at llvm.org
Sat Apr 12 14:13:25 PDT 2025
https://github.com/makslevental created https://github.com/llvm/llvm-project/pull/135501
None
>From 4fba3b9f401c53aaafea246c7c662cad39385aed Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Sat, 12 Apr 2025 17:07:14 -0400
Subject: [PATCH] [mlir][SMT] C APIs
---
mlir/include/mlir-c/Dialect/SMT.h | 110 +++++++++++++
mlir/include/mlir-c/Target/ExportSMTLIB.h | 27 ++++
mlir/lib/CAPI/Dialect/CMakeLists.txt | 8 +
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 ++++++++++++++++++++++
8 files changed, 491 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..f12faa23d408e 100644
--- a/mlir/lib/CAPI/Dialect/CMakeLists.txt
+++ b/mlir/lib/CAPI/Dialect/CMakeLists.txt
@@ -269,3 +269,11 @@ add_mlir_upstream_c_api_library(MLIRCAPIVector
MLIRCAPIIR
MLIRVectorDialect
)
+
+add_mlir_upstream_c_api_library(MLIRCAPISMT
+ SMT.cpp
+
+ 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..346864737709e
--- /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/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+#include "mlir/CAPI/Registration.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/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..0bc895ec6e07e
--- /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: circt-capi-smtlib-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_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;
+}
More information about the Mlir-commits
mailing list