112 lines · c
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-exception6//7//===----------------------------------------------------------------------===//8 9#ifndef MLIR_C_DIALECT_SMT_H10#define MLIR_C_DIALECT_SMT_H11 12#include "mlir-c/IR.h"13 14#ifdef __cplusplus15extern "C" {16#endif17 18//===----------------------------------------------------------------------===//19// Dialect API.20//===----------------------------------------------------------------------===//21 22MLIR_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.29MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAnyNonFuncSMTValueType(MlirType type);30 31/// Checks if the given type is any SMT value type.32MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAnySMTValueType(MlirType type);33 34/// Checks if the given type is a smt::ArrayType.35MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAArray(MlirType type);36 37/// Creates an array type with the given domain and range types.38MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetArray(MlirContext ctx,39 MlirType domainType,40 MlirType rangeType);41 42/// Checks if the given type is a smt::BitVectorType.43MLIR_CAPI_EXPORTED bool mlirSMTTypeIsABitVector(MlirType type);44 45/// Creates a smt::BitVectorType with the given width.46MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetBitVector(MlirContext ctx,47 int32_t width);48 49/// Checks if the given type is a smt::BoolType.50MLIR_CAPI_EXPORTED bool mlirSMTTypeIsABool(MlirType type);51 52/// Creates a smt::BoolType.53MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetBool(MlirContext ctx);54 55/// Checks if the given type is a smt::IntType.56MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAInt(MlirType type);57 58/// Creates a smt::IntType.59MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetInt(MlirContext ctx);60 61/// Checks if the given type is a smt::FuncType.62MLIR_CAPI_EXPORTED bool mlirSMTTypeIsASMTFunc(MlirType type);63 64/// Creates a smt::FuncType with the given domain and range types.65MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetSMTFunc(MlirContext ctx,66 size_t numberOfDomainTypes,67 const MlirType *domainTypes,68 MlirType rangeType);69 70/// Checks if the given type is a smt::SortType.71MLIR_CAPI_EXPORTED bool mlirSMTTypeIsASort(MlirType type);72 73/// Creates a smt::SortType with the given identifier and sort parameters.74MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetSort(MlirContext ctx,75 MlirIdentifier identifier,76 size_t numberOfSortParams,77 const MlirType *sortParams);78 79//===----------------------------------------------------------------------===//80// Attribute API.81//===----------------------------------------------------------------------===//82 83/// Checks if the given string is a valid smt::BVCmpPredicate.84MLIR_CAPI_EXPORTED bool mlirSMTAttrCheckBVCmpPredicate(MlirContext ctx,85 MlirStringRef str);86 87/// Checks if the given string is a valid smt::IntPredicate.88MLIR_CAPI_EXPORTED bool mlirSMTAttrCheckIntPredicate(MlirContext ctx,89 MlirStringRef str);90 91/// Checks if the given attribute is a smt::SMTAttribute.92MLIR_CAPI_EXPORTED bool mlirSMTAttrIsASMTAttribute(MlirAttribute attr);93 94/// Creates a smt::BitVectorAttr with the given value and width.95MLIR_CAPI_EXPORTED MlirAttribute mlirSMTAttrGetBitVector(MlirContext ctx,96 uint64_t value,97 unsigned width);98 99/// Creates a smt::BVCmpPredicateAttr with the given string.100MLIR_CAPI_EXPORTED MlirAttribute101mlirSMTAttrGetBVCmpPredicate(MlirContext ctx, MlirStringRef str);102 103/// Creates a smt::IntPredicateAttr with the given string.104MLIR_CAPI_EXPORTED MlirAttribute mlirSMTAttrGetIntPredicate(MlirContext ctx,105 MlirStringRef str);106 107#ifdef __cplusplus108}109#endif110 111#endif // MLIR_C_DIALECT_SMT_H112