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
21void dumpCallback(MlirStringRef message, void *userData) {
22 fprintf(stderr, format: "%.*s", (int)message.length, message.data);
23}
24
25void 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
47void 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
143void 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
175int 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

source code of mlir/test/CAPI/smt.c