Skip to content

Commit 9deb08a

Browse files
maksleventalTaoBi22maerhartmikeurbachdtzSiFive
authored
[mlir][SMT] C APIs (#135501)
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]>
1 parent 2b58b3d commit 9deb08a

File tree

10 files changed

+509
-1
lines changed

10 files changed

+509
-1
lines changed

‎mlir/include/mlir-c/Dialect/SMT.h

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
//===- SMT.h - C interface for the SMT dialect --------------------*- C -*-===//
2+
//
3+
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4+
// See https://llvm.org/LICENSE.txt for license information.
5+
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6+
//
7+
//===----------------------------------------------------------------------===//
8+
9+
#ifndef MLIR_C_DIALECT_SMT_H
10+
#define MLIR_C_DIALECT_SMT_H
11+
12+
#include "mlir-c/IR.h"
13+
14+
#ifdef __cplusplus
15+
extern "C" {
16+
#endif
17+
18+
//===----------------------------------------------------------------------===//
19+
// Dialect API.
20+
//===----------------------------------------------------------------------===//
21+
22+
MLIR_DECLARE_CAPI_DIALECT_REGISTRATION(SMT, smt);
23+
24+
//===----------------------------------------------------------------------===//
25+
// Type API.
26+
//===----------------------------------------------------------------------===//
27+
28+
/// Checks if the given type is any non-func SMT value type.
29+
MLIR_CAPI_EXPORTED bool smtTypeIsAnyNonFuncSMTValueType(MlirType type);
30+
31+
/// Checks if the given type is any SMT value type.
32+
MLIR_CAPI_EXPORTED bool smtTypeIsAnySMTValueType(MlirType type);
33+
34+
/// Checks if the given type is a smt::ArrayType.
35+
MLIR_CAPI_EXPORTED bool smtTypeIsAArray(MlirType type);
36+
37+
/// Creates an array type with the given domain and range types.
38+
MLIR_CAPI_EXPORTED MlirType smtTypeGetArray(MlirContext ctx,
39+
MlirType domainType,
40+
MlirType rangeType);
41+
42+
/// Checks if the given type is a smt::BitVectorType.
43+
MLIR_CAPI_EXPORTED bool smtTypeIsABitVector(MlirType type);
44+
45+
/// Creates a smt::BitVectorType with the given width.
46+
MLIR_CAPI_EXPORTED MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width);
47+
48+
/// Checks if the given type is a smt::BoolType.
49+
MLIR_CAPI_EXPORTED bool smtTypeIsABool(MlirType type);
50+
51+
/// Creates a smt::BoolType.
52+
MLIR_CAPI_EXPORTED MlirType smtTypeGetBool(MlirContext ctx);
53+
54+
/// Checks if the given type is a smt::IntType.
55+
MLIR_CAPI_EXPORTED bool smtTypeIsAInt(MlirType type);
56+
57+
/// Creates a smt::IntType.
58+
MLIR_CAPI_EXPORTED MlirType smtTypeGetInt(MlirContext ctx);
59+
60+
/// Checks if the given type is a smt::FuncType.
61+
MLIR_CAPI_EXPORTED bool smtTypeIsASMTFunc(MlirType type);
62+
63+
/// Creates a smt::FuncType with the given domain and range types.
64+
MLIR_CAPI_EXPORTED MlirType smtTypeGetSMTFunc(MlirContext ctx,
65+
size_t numberOfDomainTypes,
66+
const MlirType *domainTypes,
67+
MlirType rangeType);
68+
69+
/// Checks if the given type is a smt::SortType.
70+
MLIR_CAPI_EXPORTED bool smtTypeIsASort(MlirType type);
71+
72+
/// Creates a smt::SortType with the given identifier and sort parameters.
73+
MLIR_CAPI_EXPORTED MlirType smtTypeGetSort(MlirContext ctx,
74+
MlirIdentifier identifier,
75+
size_t numberOfSortParams,
76+
const MlirType *sortParams);
77+
78+
//===----------------------------------------------------------------------===//
79+
// Attribute API.
80+
//===----------------------------------------------------------------------===//
81+
82+
/// Checks if the given string is a valid smt::BVCmpPredicate.
83+
MLIR_CAPI_EXPORTED bool smtAttrCheckBVCmpPredicate(MlirContext ctx,
84+
MlirStringRef str);
85+
86+
/// Checks if the given string is a valid smt::IntPredicate.
87+
MLIR_CAPI_EXPORTED bool smtAttrCheckIntPredicate(MlirContext ctx,
88+
MlirStringRef str);
89+
90+
/// Checks if the given attribute is a smt::SMTAttribute.
91+
MLIR_CAPI_EXPORTED bool smtAttrIsASMTAttribute(MlirAttribute attr);
92+
93+
/// Creates a smt::BitVectorAttr with the given value and width.
94+
MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetBitVector(MlirContext ctx,
95+
uint64_t value,
96+
unsigned width);
97+
98+
/// Creates a smt::BVCmpPredicateAttr with the given string.
99+
MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetBVCmpPredicate(MlirContext ctx,
100+
MlirStringRef str);
101+
102+
/// Creates a smt::IntPredicateAttr with the given string.
103+
MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetIntPredicate(MlirContext ctx,
104+
MlirStringRef str);
105+
106+
#ifdef __cplusplus
107+
}
108+
#endif
109+
110+
#endif // MLIR_C_DIALECT_SMT_H

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

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
//===- mlir-c/Target/ExportSMTLIB.h - C API for emitting SMTLIB ---*- C -*-===//
2+
//
3+
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4+
// See https://llvm.org/LICENSE.txt for license information.
5+
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6+
//
7+
//===----------------------------------------------------------------------===//
8+
//
9+
// This header declares the C interface for emitting SMTLIB from an MLIR module.
10+
//
11+
//===----------------------------------------------------------------------===//
12+
13+
#ifndef MLIR_C_EXPORTSMTLIB_H
14+
#define MLIR_C_EXPORTSMTLIB_H
15+
16+
#include "mlir-c/IR.h"
17+
18+
#ifdef __cplusplus
19+
extern "C" {
20+
#endif
21+
22+
/// Emits SMTLIB for the specified module using the provided callback and user
23+
/// data
24+
MLIR_CAPI_EXPORTED MlirLogicalResult mlirExportSMTLIB(MlirModule,
25+
MlirStringCallback,
26+
void *userData);
27+
28+
#ifdef __cplusplus
29+
}
30+
#endif
31+
32+
#endif // MLIR_C_EXPORTSMTLIB_H

‎mlir/lib/CAPI/Dialect/CMakeLists.txt

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -269,3 +269,12 @@ add_mlir_upstream_c_api_library(MLIRCAPIVector
269269
MLIRCAPIIR
270270
MLIRVectorDialect
271271
)
272+
273+
add_mlir_upstream_c_api_library(MLIRCAPISMT
274+
SMT.cpp
275+
276+
PARTIAL_SOURCES_INTENDED
277+
LINK_LIBS PUBLIC
278+
MLIRCAPIIR
279+
MLIRSMT
280+
)

‎mlir/lib/CAPI/Dialect/SMT.cpp

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
//===- SMT.cpp - C interface for the SMT dialect --------------------------===//
2+
//
3+
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4+
// See https://llvm.org/LICENSE.txt for license information.
5+
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6+
//
7+
//===----------------------------------------------------------------------===//
8+
9+
#include "mlir-c/Dialect/SMT.h"
10+
#include "mlir/CAPI/Registration.h"
11+
#include "mlir/Dialect/SMT/IR/SMTAttributes.h"
12+
#include "mlir/Dialect/SMT/IR/SMTDialect.h"
13+
#include "mlir/Dialect/SMT/IR/SMTTypes.h"
14+
15+
using namespace mlir;
16+
using namespace smt;
17+
18+
//===----------------------------------------------------------------------===//
19+
// Dialect API.
20+
//===----------------------------------------------------------------------===//
21+
22+
MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, mlir::smt::SMTDialect)
23+
24+
//===----------------------------------------------------------------------===//
25+
// Type API.
26+
//===----------------------------------------------------------------------===//
27+
28+
bool smtTypeIsAnyNonFuncSMTValueType(MlirType type) {
29+
return isAnyNonFuncSMTValueType(unwrap(type));
30+
}
31+
32+
bool smtTypeIsAnySMTValueType(MlirType type) {
33+
return isAnySMTValueType(unwrap(type));
34+
}
35+
36+
bool smtTypeIsAArray(MlirType type) { return isa<ArrayType>(unwrap(type)); }
37+
38+
MlirType smtTypeGetArray(MlirContext ctx, MlirType domainType,
39+
MlirType rangeType) {
40+
return wrap(
41+
ArrayType::get(unwrap(ctx), unwrap(domainType), unwrap(rangeType)));
42+
}
43+
44+
bool smtTypeIsABitVector(MlirType type) {
45+
return isa<BitVectorType>(unwrap(type));
46+
}
47+
48+
MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width) {
49+
return wrap(BitVectorType::get(unwrap(ctx), width));
50+
}
51+
52+
bool smtTypeIsABool(MlirType type) { return isa<BoolType>(unwrap(type)); }
53+
54+
MlirType smtTypeGetBool(MlirContext ctx) {
55+
return wrap(BoolType::get(unwrap(ctx)));
56+
}
57+
58+
bool smtTypeIsAInt(MlirType type) { return isa<IntType>(unwrap(type)); }
59+
60+
MlirType smtTypeGetInt(MlirContext ctx) {
61+
return wrap(IntType::get(unwrap(ctx)));
62+
}
63+
64+
bool smtTypeIsASMTFunc(MlirType type) { return isa<SMTFuncType>(unwrap(type)); }
65+
66+
MlirType smtTypeGetSMTFunc(MlirContext ctx, size_t numberOfDomainTypes,
67+
const MlirType *domainTypes, MlirType rangeType) {
68+
SmallVector<Type> domainTypesVec;
69+
domainTypesVec.reserve(numberOfDomainTypes);
70+
71+
for (size_t i = 0; i < numberOfDomainTypes; i++)
72+
domainTypesVec.push_back(unwrap(domainTypes[i]));
73+
74+
return wrap(SMTFuncType::get(unwrap(ctx), domainTypesVec, unwrap(rangeType)));
75+
}
76+
77+
bool smtTypeIsASort(MlirType type) { return isa<SortType>(unwrap(type)); }
78+
79+
MlirType smtTypeGetSort(MlirContext ctx, MlirIdentifier identifier,
80+
size_t numberOfSortParams, const MlirType *sortParams) {
81+
SmallVector<Type> sortParamsVec;
82+
sortParamsVec.reserve(numberOfSortParams);
83+
84+
for (size_t i = 0; i < numberOfSortParams; i++)
85+
sortParamsVec.push_back(unwrap(sortParams[i]));
86+
87+
return wrap(SortType::get(unwrap(ctx), unwrap(identifier), sortParamsVec));
88+
}
89+
90+
//===----------------------------------------------------------------------===//
91+
// Attribute API.
92+
//===----------------------------------------------------------------------===//
93+
94+
bool smtAttrCheckBVCmpPredicate(MlirContext ctx, MlirStringRef str) {
95+
return symbolizeBVCmpPredicate(unwrap(str)).has_value();
96+
}
97+
98+
bool smtAttrCheckIntPredicate(MlirContext ctx, MlirStringRef str) {
99+
return symbolizeIntPredicate(unwrap(str)).has_value();
100+
}
101+
102+
bool smtAttrIsASMTAttribute(MlirAttribute attr) {
103+
return isa<BitVectorAttr, BVCmpPredicateAttr, IntPredicateAttr>(unwrap(attr));
104+
}
105+
106+
MlirAttribute smtAttrGetBitVector(MlirContext ctx, uint64_t value,
107+
unsigned width) {
108+
return wrap(BitVectorAttr::get(unwrap(ctx), value, width));
109+
}
110+
111+
MlirAttribute smtAttrGetBVCmpPredicate(MlirContext ctx, MlirStringRef str) {
112+
auto predicate = symbolizeBVCmpPredicate(unwrap(str));
113+
assert(predicate.has_value() && "invalid predicate");
114+
115+
return wrap(BVCmpPredicateAttr::get(unwrap(ctx), predicate.value()));
116+
}
117+
118+
MlirAttribute smtAttrGetIntPredicate(MlirContext ctx, MlirStringRef str) {
119+
auto predicate = symbolizeIntPredicate(unwrap(str));
120+
assert(predicate.has_value() && "invalid predicate");
121+
122+
return wrap(IntPredicateAttr::get(unwrap(ctx), predicate.value()));
123+
}

‎mlir/lib/CAPI/Target/CMakeLists.txt

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
add_mlir_upstream_c_api_library(MLIRCAPITarget
22
LLVMIR.cpp
33

4+
PARTIAL_SOURCES_INTENDED
5+
46
LINK_COMPONENTS
57
Core
68

@@ -11,3 +13,13 @@ add_mlir_upstream_c_api_library(MLIRCAPITarget
1113
MLIRLLVMIRToLLVMTranslation
1214
MLIRSupport
1315
)
16+
17+
add_mlir_upstream_c_api_library(MLIRCAPIExportSMTLIB
18+
ExportSMTLIB.cpp
19+
20+
PARTIAL_SOURCES_INTENDED
21+
22+
LINK_LIBS PUBLIC
23+
MLIRCAPIIR
24+
MLIRExportSMTLIB
25+
)

‎mlir/lib/CAPI/Target/ExportSMTLIB.cpp

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
//===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===//
2+
//
3+
// Part of the LLVM Project, under the Apache License v2.0 with LLVM
4+
// Exceptions.
5+
// See https://llvm.org/LICENSE.txt for license information.
6+
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
7+
//
8+
//===----------------------------------------------------------------------===//
9+
//
10+
// Implements a C Interface for export SMTLIB.
11+
//
12+
//===----------------------------------------------------------------------===//
13+
14+
#include "mlir-c/Target/ExportSMTLIB.h"
15+
#include "mlir/CAPI/IR.h"
16+
#include "mlir/CAPI/Support.h"
17+
#include "mlir/CAPI/Utils.h"
18+
#include "mlir/Target/SMTLIB/ExportSMTLIB.h"
19+
20+
using namespace mlir;
21+
22+
MlirLogicalResult mlirExportSMTLIB(MlirModule module,
23+
MlirStringCallback callback,
24+
void *userData) {
25+
mlir::detail::CallbackOstream stream(callback, userData);
26+
return wrap(smt::exportSMTLIB(unwrap(module), stream));
27+
}

‎mlir/lib/Target/SMTLIB/CMakeLists.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,4 @@ add_mlir_translation_library(MLIRExportSMTLIB
1111
MLIRSMT
1212
MLIRSupport
1313
MLIRTranslateLib
14-
MLIRArithDialect
1514
)

‎mlir/test/CAPI/CMakeLists.txt

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,3 +123,13 @@ _add_capi_test_executable(mlir-capi-translation-test
123123
MLIRCAPIRegisterEverything
124124
MLIRCAPITarget
125125
)
126+
127+
_add_capi_test_executable(mlir-capi-smt-test
128+
smt.c
129+
130+
LINK_LIBS PRIVATE
131+
MLIRCAPIIR
132+
MLIRCAPIFunc
133+
MLIRCAPISMT
134+
MLIRCAPIExportSMTLIB
135+
)

0 commit comments

Comments
 (0)