187 lines · c
1//===- smt.c - Test of SMT APIs -------------------------------------------===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM4// Exceptions.5// See https://llvm.org/LICENSE.txt for license information.6// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception7//8//===----------------------------------------------------------------------===//9 10/* RUN: mlir-capi-smt-test 2>&1 | FileCheck %s11 */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, "%.*s", (int)message.length, message.data);23}24 25void testExportSMTLIB(MlirContext ctx) {26 // clang-format off27 const char *testSMT = 28 "func.func @test() {\n"29 " smt.solver() : () -> () { }\n"30 " return\n"31 "}\n";32 // clang-format on33 34 MlirModule module =35 mlirModuleCreateParse(ctx, mlirStringRefCreateFromCString(testSMT));36 37 MlirLogicalResult result =38 mlirTranslateModuleToSMTLIB(module, dumpCallback, NULL, false, false);39 (void)result;40 assert(mlirLogicalResultIsSuccess(result));41 42 // CHECK: ; solver scope 043 // 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, intType, boolType);51 MlirType bvType = mlirSMTTypeGetBitVector(ctx, 32);52 MlirType funcType =53 mlirSMTTypeGetSMTFunc(ctx, 2, (MlirType[]){intType, boolType}, boolType);54 MlirType sortType = mlirSMTTypeGetSort(55 ctx, mlirIdentifierGet(ctx, mlirStringRefCreateFromCString("sort")), 0,56 NULL);57 58 // CHECK: !smt.bool59 mlirTypeDump(boolType);60 // CHECK: !smt.int61 mlirTypeDump(intType);62 // CHECK: !smt.array<[!smt.int -> !smt.bool]>63 mlirTypeDump(arrayType);64 // CHECK: !smt.bv<32>65 mlirTypeDump(bvType);66 // CHECK: !smt.func<(!smt.int, !smt.bool) !smt.bool>67 mlirTypeDump(funcType);68 // CHECK: !smt.sort<"sort">69 mlirTypeDump(sortType);70 71 // CHECK: bool_is_any_non_func_smt_value_type72 fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(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_type76 fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(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_type80 fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(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_type84 fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(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_type88 fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(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_type92 fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(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_type97 fprintf(stderr, mlirSMTTypeIsAnySMTValueType(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_type101 fprintf(stderr, mlirSMTTypeIsAnySMTValueType(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_type105 fprintf(stderr, mlirSMTTypeIsAnySMTValueType(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_type109 fprintf(stderr, mlirSMTTypeIsAnySMTValueType(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_type113 fprintf(stderr, mlirSMTTypeIsAnySMTValueType(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_type117 fprintf(stderr, mlirSMTTypeIsAnySMTValueType(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_bool122 fprintf(stderr, mlirSMTTypeIsABool(intType) ? "int_type_is_a_bool\n"123 : "int_type_is_not_a_bool\n");124 // CHECK: bool_type_is_not_a_int125 fprintf(stderr, mlirSMTTypeIsAInt(boolType) ? "bool_type_is_a_int\n"126 : "bool_type_is_not_a_int\n");127 // CHECK: bv_type_is_not_a_array128 fprintf(stderr, mlirSMTTypeIsAArray(bvType) ? "bv_type_is_a_array\n"129 : "bv_type_is_not_a_array\n");130 // CHECK: array_type_is_not_a_bit_vector131 fprintf(stderr, mlirSMTTypeIsABitVector(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_func135 fprintf(stderr, mlirSMTTypeIsASMTFunc(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_sort139 fprintf(stderr, mlirSMTTypeIsASort(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_BVCmpPredicate145 fprintf(stderr, mlirSMTAttrCheckBVCmpPredicate(146 ctx, mlirStringRefCreateFromCString("slt"))147 ? "slt_is_BVCmpPredicate\n"148 : "slt_is_not_BVCmpPredicate\n");149 // CHECK: lt_is_not_BVCmpPredicate150 fprintf(stderr, mlirSMTAttrCheckBVCmpPredicate(151 ctx, mlirStringRefCreateFromCString("lt"))152 ? "lt_is_BVCmpPredicate\n"153 : "lt_is_not_BVCmpPredicate\n");154 // CHECK: slt_is_not_IntPredicate155 fprintf(stderr, mlirSMTAttrCheckIntPredicate(156 ctx, mlirStringRefCreateFromCString("slt"))157 ? "slt_is_IntPredicate\n"158 : "slt_is_not_IntPredicate\n");159 // CHECK: lt_is_IntPredicate160 fprintf(stderr, mlirSMTAttrCheckIntPredicate(161 ctx, mlirStringRefCreateFromCString("lt"))162 ? "lt_is_IntPredicate\n"163 : "lt_is_not_IntPredicate\n");164 165 // CHECK: #smt.bv<5> : !smt.bv<32>166 mlirAttributeDump(mlirSMTAttrGetBitVector(ctx, 5, 32));167 // CHECK: 0 : i64168 mlirAttributeDump(169 mlirSMTAttrGetBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt")));170 // CHECK: 0 : i64171 mlirAttributeDump(172 mlirSMTAttrGetIntPredicate(ctx, mlirStringRefCreateFromCString("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(ctx);184 185 return 0;186}187