1 | //===- smt.c - Test of SMT APIs -------------------------------------------===// |
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 | /* RUN: mlir-capi-smt-test 2>&1 | FileCheck %s |
11 | */ |
12 | |
13 | #include "mlir-c/Dialect/SMT.h" |
14 | #include "mlir-c/Dialect/Func.h" |
15 | #include "mlir-c/IR.h" |
16 | #include "mlir-c/Support.h" |
17 | #include "mlir-c/Target/ExportSMTLIB.h" |
18 | #include <assert.h> |
19 | #include <stdio.h> |
20 | |
21 | void dumpCallback(MlirStringRef message, void *userData) { |
22 | fprintf(stderr, format: "%.*s" , (int)message.length, message.data); |
23 | } |
24 | |
25 | void testExportSMTLIB(MlirContext ctx) { |
26 | // clang-format off |
27 | const char *testSMT = |
28 | "func.func @test() {\n" |
29 | " smt.solver() : () -> () { }\n" |
30 | " return\n" |
31 | "}\n" ; |
32 | // clang-format on |
33 | |
34 | MlirModule module = |
35 | mlirModuleCreateParse(context: ctx, module: mlirStringRefCreateFromCString(str: testSMT)); |
36 | |
37 | MlirLogicalResult result = |
38 | mlirTranslateModuleToSMTLIB(module, dumpCallback, NULL, false, false); |
39 | (void)result; |
40 | assert(mlirLogicalResultIsSuccess(result)); |
41 | |
42 | // CHECK: ; solver scope 0 |
43 | // CHECK-NEXT: (reset) |
44 | mlirModuleDestroy(module); |
45 | } |
46 | |
47 | void testSMTType(MlirContext ctx) { |
48 | MlirType boolType = mlirSMTTypeGetBool(ctx); |
49 | MlirType intType = mlirSMTTypeGetInt(ctx); |
50 | MlirType arrayType = mlirSMTTypeGetArray(ctx, domainType: intType, rangeType: boolType); |
51 | MlirType bvType = mlirSMTTypeGetBitVector(ctx, width: 32); |
52 | MlirType funcType = |
53 | mlirSMTTypeGetSMTFunc(ctx, numberOfDomainTypes: 2, domainTypes: (MlirType[]){intType, boolType}, rangeType: boolType); |
54 | MlirType sortType = mlirSMTTypeGetSort( |
55 | ctx, identifier: mlirIdentifierGet(context: ctx, str: mlirStringRefCreateFromCString(str: "sort" )), numberOfSortParams: 0, |
56 | NULL); |
57 | |
58 | // CHECK: !smt.bool |
59 | mlirTypeDump(type: boolType); |
60 | // CHECK: !smt.int |
61 | mlirTypeDump(type: intType); |
62 | // CHECK: !smt.array<[!smt.int -> !smt.bool]> |
63 | mlirTypeDump(type: arrayType); |
64 | // CHECK: !smt.bv<32> |
65 | mlirTypeDump(type: bvType); |
66 | // CHECK: !smt.func<(!smt.int, !smt.bool) !smt.bool> |
67 | mlirTypeDump(type: funcType); |
68 | // CHECK: !smt.sort<"sort"> |
69 | mlirTypeDump(type: sortType); |
70 | |
71 | // CHECK: bool_is_any_non_func_smt_value_type |
72 | fprintf(stderr, format: mlirSMTTypeIsAnyNonFuncSMTValueType(type: boolType) |
73 | ? "bool_is_any_non_func_smt_value_type\n" |
74 | : "bool_is_func_smt_value_type\n" ); |
75 | // CHECK: int_is_any_non_func_smt_value_type |
76 | fprintf(stderr, format: mlirSMTTypeIsAnyNonFuncSMTValueType(type: intType) |
77 | ? "int_is_any_non_func_smt_value_type\n" |
78 | : "int_is_func_smt_value_type\n" ); |
79 | // CHECK: array_is_any_non_func_smt_value_type |
80 | fprintf(stderr, format: mlirSMTTypeIsAnyNonFuncSMTValueType(type: arrayType) |
81 | ? "array_is_any_non_func_smt_value_type\n" |
82 | : "array_is_func_smt_value_type\n" ); |
83 | // CHECK: bit_vector_is_any_non_func_smt_value_type |
84 | fprintf(stderr, format: mlirSMTTypeIsAnyNonFuncSMTValueType(type: bvType) |
85 | ? "bit_vector_is_any_non_func_smt_value_type\n" |
86 | : "bit_vector_is_func_smt_value_type\n" ); |
87 | // CHECK: sort_is_any_non_func_smt_value_type |
88 | fprintf(stderr, format: mlirSMTTypeIsAnyNonFuncSMTValueType(type: sortType) |
89 | ? "sort_is_any_non_func_smt_value_type\n" |
90 | : "sort_is_func_smt_value_type\n" ); |
91 | // CHECK: smt_func_is_func_smt_value_type |
92 | fprintf(stderr, format: mlirSMTTypeIsAnyNonFuncSMTValueType(type: funcType) |
93 | ? "smt_func_is_any_non_func_smt_value_type\n" |
94 | : "smt_func_is_func_smt_value_type\n" ); |
95 | |
96 | // CHECK: bool_is_any_smt_value_type |
97 | fprintf(stderr, format: mlirSMTTypeIsAnySMTValueType(type: boolType) |
98 | ? "bool_is_any_smt_value_type\n" |
99 | : "bool_is_not_any_smt_value_type\n" ); |
100 | // CHECK: int_is_any_smt_value_type |
101 | fprintf(stderr, format: mlirSMTTypeIsAnySMTValueType(type: intType) |
102 | ? "int_is_any_smt_value_type\n" |
103 | : "int_is_not_any_smt_value_type\n" ); |
104 | // CHECK: array_is_any_smt_value_type |
105 | fprintf(stderr, format: mlirSMTTypeIsAnySMTValueType(type: arrayType) |
106 | ? "array_is_any_smt_value_type\n" |
107 | : "array_is_not_any_smt_value_type\n" ); |
108 | // CHECK: array_is_any_smt_value_type |
109 | fprintf(stderr, format: mlirSMTTypeIsAnySMTValueType(type: bvType) |
110 | ? "array_is_any_smt_value_type\n" |
111 | : "array_is_not_any_smt_value_type\n" ); |
112 | // CHECK: smt_func_is_any_smt_value_type |
113 | fprintf(stderr, format: mlirSMTTypeIsAnySMTValueType(type: funcType) |
114 | ? "smt_func_is_any_smt_value_type\n" |
115 | : "smt_func_is_not_any_smt_value_type\n" ); |
116 | // CHECK: sort_is_any_smt_value_type |
117 | fprintf(stderr, format: mlirSMTTypeIsAnySMTValueType(type: sortType) |
118 | ? "sort_is_any_smt_value_type\n" |
119 | : "sort_is_not_any_smt_value_type\n" ); |
120 | |
121 | // CHECK: int_type_is_not_a_bool |
122 | fprintf(stderr, format: mlirSMTTypeIsABool(type: intType) ? "int_type_is_a_bool\n" |
123 | : "int_type_is_not_a_bool\n" ); |
124 | // CHECK: bool_type_is_not_a_int |
125 | fprintf(stderr, format: mlirSMTTypeIsAInt(type: boolType) ? "bool_type_is_a_int\n" |
126 | : "bool_type_is_not_a_int\n" ); |
127 | // CHECK: bv_type_is_not_a_array |
128 | fprintf(stderr, format: mlirSMTTypeIsAArray(type: bvType) ? "bv_type_is_a_array\n" |
129 | : "bv_type_is_not_a_array\n" ); |
130 | // CHECK: array_type_is_not_a_bit_vector |
131 | fprintf(stderr, format: mlirSMTTypeIsABitVector(type: arrayType) |
132 | ? "array_type_is_a_bit_vector\n" |
133 | : "array_type_is_not_a_bit_vector\n" ); |
134 | // CHECK: sort_type_is_not_a_smt_func |
135 | fprintf(stderr, format: mlirSMTTypeIsASMTFunc(type: sortType) |
136 | ? "sort_type_is_a_smt_func\n" |
137 | : "sort_type_is_not_a_smt_func\n" ); |
138 | // CHECK: func_type_is_not_a_sort |
139 | fprintf(stderr, format: mlirSMTTypeIsASort(type: funcType) ? "func_type_is_a_sort\n" |
140 | : "func_type_is_not_a_sort\n" ); |
141 | } |
142 | |
143 | void testSMTAttribute(MlirContext ctx) { |
144 | // CHECK: slt_is_BVCmpPredicate |
145 | fprintf(stderr, format: mlirSMTAttrCheckBVCmpPredicate( |
146 | ctx, str: mlirStringRefCreateFromCString(str: "slt" )) |
147 | ? "slt_is_BVCmpPredicate\n" |
148 | : "slt_is_not_BVCmpPredicate\n" ); |
149 | // CHECK: lt_is_not_BVCmpPredicate |
150 | fprintf(stderr, format: mlirSMTAttrCheckBVCmpPredicate( |
151 | ctx, str: mlirStringRefCreateFromCString(str: "lt" )) |
152 | ? "lt_is_BVCmpPredicate\n" |
153 | : "lt_is_not_BVCmpPredicate\n" ); |
154 | // CHECK: slt_is_not_IntPredicate |
155 | fprintf(stderr, format: mlirSMTAttrCheckIntPredicate( |
156 | ctx, str: mlirStringRefCreateFromCString(str: "slt" )) |
157 | ? "slt_is_IntPredicate\n" |
158 | : "slt_is_not_IntPredicate\n" ); |
159 | // CHECK: lt_is_IntPredicate |
160 | fprintf(stderr, format: mlirSMTAttrCheckIntPredicate( |
161 | ctx, str: mlirStringRefCreateFromCString(str: "lt" )) |
162 | ? "lt_is_IntPredicate\n" |
163 | : "lt_is_not_IntPredicate\n" ); |
164 | |
165 | // CHECK: #smt.bv<5> : !smt.bv<32> |
166 | mlirAttributeDump(attr: mlirSMTAttrGetBitVector(ctx, value: 5, width: 32)); |
167 | // CHECK: 0 : i64 |
168 | mlirAttributeDump( |
169 | attr: mlirSMTAttrGetBVCmpPredicate(ctx, str: mlirStringRefCreateFromCString(str: "slt" ))); |
170 | // CHECK: 0 : i64 |
171 | mlirAttributeDump( |
172 | attr: mlirSMTAttrGetIntPredicate(ctx, str: mlirStringRefCreateFromCString(str: "lt" ))); |
173 | } |
174 | |
175 | int main(void) { |
176 | MlirContext ctx = mlirContextCreate(); |
177 | mlirDialectHandleLoadDialect(mlirGetDialectHandle__smt__(), ctx); |
178 | mlirDialectHandleLoadDialect(mlirGetDialectHandle__func__(), ctx); |
179 | testExportSMTLIB(ctx); |
180 | testSMTType(ctx); |
181 | testSMTAttribute(ctx); |
182 | |
183 | mlirContextDestroy(context: ctx); |
184 | |
185 | return 0; |
186 | } |
187 | |