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
15extern "C" {
16#endif
17
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 MlirAttribute
101mlirSMTAttrGetBVCmpPredicate(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 __cplusplus
108}
109#endif
110
111#endif // MLIR_C_DIALECT_SMT_H
112

source code of mlir/include/mlir-c/Dialect/SMT.h