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 mlirSMTTypeIsAnyNonFuncSMTValueType(MlirType type); |
30 | |
31 | /// Checks if the given type is any SMT value type. |
32 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAnySMTValueType(MlirType type); |
33 | |
34 | /// Checks if the given type is a smt::ArrayType. |
35 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAArray(MlirType type); |
36 | |
37 | /// Creates an array type with the given domain and range types. |
38 | MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetArray(MlirContext ctx, |
39 | MlirType domainType, |
40 | MlirType rangeType); |
41 | |
42 | /// Checks if the given type is a smt::BitVectorType. |
43 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsABitVector(MlirType type); |
44 | |
45 | /// Creates a smt::BitVectorType with the given width. |
46 | MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetBitVector(MlirContext ctx, |
47 | int32_t width); |
48 | |
49 | /// Checks if the given type is a smt::BoolType. |
50 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsABool(MlirType type); |
51 | |
52 | /// Creates a smt::BoolType. |
53 | MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetBool(MlirContext ctx); |
54 | |
55 | /// Checks if the given type is a smt::IntType. |
56 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAInt(MlirType type); |
57 | |
58 | /// Creates a smt::IntType. |
59 | MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetInt(MlirContext ctx); |
60 | |
61 | /// Checks if the given type is a smt::FuncType. |
62 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsASMTFunc(MlirType type); |
63 | |
64 | /// Creates a smt::FuncType with the given domain and range types. |
65 | MLIR_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. |
71 | MLIR_CAPI_EXPORTED bool mlirSMTTypeIsASort(MlirType type); |
72 | |
73 | /// Creates a smt::SortType with the given identifier and sort parameters. |
74 | MLIR_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. |
84 | MLIR_CAPI_EXPORTED bool mlirSMTAttrCheckBVCmpPredicate(MlirContext ctx, |
85 | MlirStringRef str); |
86 | |
87 | /// Checks if the given string is a valid smt::IntPredicate. |
88 | MLIR_CAPI_EXPORTED bool mlirSMTAttrCheckIntPredicate(MlirContext ctx, |
89 | MlirStringRef str); |
90 | |
91 | /// Checks if the given attribute is a smt::SMTAttribute. |
92 | MLIR_CAPI_EXPORTED bool mlirSMTAttrIsASMTAttribute(MlirAttribute attr); |
93 | |
94 | /// Creates a smt::BitVectorAttr with the given value and width. |
95 | MLIR_CAPI_EXPORTED MlirAttribute mlirSMTAttrGetBitVector(MlirContext ctx, |
96 | uint64_t value, |
97 | unsigned width); |
98 | |
99 | /// Creates a smt::BVCmpPredicateAttr with the given string. |
100 | MLIR_CAPI_EXPORTED MlirAttribute |
101 | mlirSMTAttrGetBVCmpPredicate(MlirContext ctx, MlirStringRef str); |
102 | |
103 | /// Creates a smt::IntPredicateAttr with the given string. |
104 | MLIR_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 | |