mirror of https://github.com/llvm/circt.git
[SMT][CAPI] Add more SMT C API
Signed-off-by: Clo91eaf <Clo91eaf@qq.com>
This commit is contained in:
parent
6128e12465
commit
17fb5b522f
|
@ -15,8 +15,94 @@
|
|||
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
|
||||
|
|
|
@ -8,7 +8,116 @@
|
|||
|
||||
#include "circt-c/Dialect/SMT.h"
|
||||
#include "circt/Dialect/SMT/SMTDialect.h"
|
||||
#include "circt/Dialect/SMT/SMTOps.h"
|
||||
|
||||
#include "mlir/CAPI/Registration.h"
|
||||
|
||||
using namespace circt;
|
||||
using namespace smt;
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Dialect API.
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, circt::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()));
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue