| //===- smt.c - Test of SMT APIs -------------------------------------------===// | |
| // | |
| // Part of the LLVM Project, under the Apache License v2.0 with LLVM | |
| // Exceptions. | |
| // See https://llvm.org/LICENSE.txt for license information. | |
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | |
| // | |
| //===----------------------------------------------------------------------===// | |
| /* RUN: mlir-capi-smt-test 2>&1 | FileCheck %s | |
| */ | |
| #include "mlir-c/Dialect/SMT.h" | |
| #include "mlir-c/Dialect/Func.h" | |
| #include "mlir-c/IR.h" | |
| #include "mlir-c/Support.h" | |
| #include "mlir-c/Target/ExportSMTLIB.h" | |
| #include <assert.h> | |
| #include <stdio.h> | |
| void dumpCallback(MlirStringRef message, void *userData) { | |
| fprintf(stderr, "%.*s", (int)message.length, message.data); | |
| } | |
| void testExportSMTLIB(MlirContext ctx) { | |
| // clang-format off | |
| const char *testSMT = | |
| "func.func @test() {\n" | |
| " smt.solver() : () -> () { }\n" | |
| " return\n" | |
| "}\n"; | |
| // clang-format on | |
| MlirModule module = | |
| mlirModuleCreateParse(ctx, mlirStringRefCreateFromCString(testSMT)); | |
| MlirLogicalResult result = mlirTranslateModuleToSMTLIB( | |
| module, dumpCallback, NULL, false, false, true); | |
| (void)result; | |
| assert(mlirLogicalResultIsSuccess(result)); | |
| // CHECK: ; solver scope 0 | |
| // CHECK-NEXT: (reset) | |
| result = mlirTranslateModuleToSMTLIB(module, dumpCallback, NULL, false, false, | |
| false); | |
| assert(mlirLogicalResultIsSuccess(result)); | |
| (void)result; | |
| // CHECK-NOT: (reset) | |
| mlirModuleDestroy(module); | |
| } | |
| void testSMTType(MlirContext ctx) { | |
| MlirType boolType = mlirSMTTypeGetBool(ctx); | |
| MlirType intType = mlirSMTTypeGetInt(ctx); | |
| MlirType arrayType = mlirSMTTypeGetArray(ctx, intType, boolType); | |
| MlirType bvType = mlirSMTTypeGetBitVector(ctx, 32); | |
| MlirType funcType = | |
| mlirSMTTypeGetSMTFunc(ctx, 2, (MlirType[]){intType, boolType}, boolType); | |
| MlirType sortType = mlirSMTTypeGetSort( | |
| ctx, mlirIdentifierGet(ctx, mlirStringRefCreateFromCString("sort")), 0, | |
| NULL); | |
| // CHECK: !smt.bool | |
| mlirTypeDump(boolType); | |
| // CHECK: !smt.int | |
| mlirTypeDump(intType); | |
| // CHECK: !smt.array<[!smt.int -> !smt.bool]> | |
| mlirTypeDump(arrayType); | |
| // CHECK: !smt.bv<32> | |
| mlirTypeDump(bvType); | |
| // CHECK: !smt.func<(!smt.int, !smt.bool) !smt.bool> | |
| mlirTypeDump(funcType); | |
| // CHECK: !smt.sort<"sort"> | |
| mlirTypeDump(sortType); | |
| // CHECK: bool_is_any_non_func_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(boolType) | |
| ? "bool_is_any_non_func_smt_value_type\n" | |
| : "bool_is_func_smt_value_type\n"); | |
| // CHECK: int_is_any_non_func_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(intType) | |
| ? "int_is_any_non_func_smt_value_type\n" | |
| : "int_is_func_smt_value_type\n"); | |
| // CHECK: array_is_any_non_func_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(arrayType) | |
| ? "array_is_any_non_func_smt_value_type\n" | |
| : "array_is_func_smt_value_type\n"); | |
| // CHECK: bit_vector_is_any_non_func_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(bvType) | |
| ? "bit_vector_is_any_non_func_smt_value_type\n" | |
| : "bit_vector_is_func_smt_value_type\n"); | |
| // CHECK: sort_is_any_non_func_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(sortType) | |
| ? "sort_is_any_non_func_smt_value_type\n" | |
| : "sort_is_func_smt_value_type\n"); | |
| // CHECK: smt_func_is_func_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(funcType) | |
| ? "smt_func_is_any_non_func_smt_value_type\n" | |
| : "smt_func_is_func_smt_value_type\n"); | |
| // CHECK: bool_is_any_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnySMTValueType(boolType) | |
| ? "bool_is_any_smt_value_type\n" | |
| : "bool_is_not_any_smt_value_type\n"); | |
| // CHECK: int_is_any_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnySMTValueType(intType) | |
| ? "int_is_any_smt_value_type\n" | |
| : "int_is_not_any_smt_value_type\n"); | |
| // CHECK: array_is_any_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnySMTValueType(arrayType) | |
| ? "array_is_any_smt_value_type\n" | |
| : "array_is_not_any_smt_value_type\n"); | |
| // CHECK: array_is_any_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnySMTValueType(bvType) | |
| ? "array_is_any_smt_value_type\n" | |
| : "array_is_not_any_smt_value_type\n"); | |
| // CHECK: smt_func_is_any_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnySMTValueType(funcType) | |
| ? "smt_func_is_any_smt_value_type\n" | |
| : "smt_func_is_not_any_smt_value_type\n"); | |
| // CHECK: sort_is_any_smt_value_type | |
| fprintf(stderr, mlirSMTTypeIsAnySMTValueType(sortType) | |
| ? "sort_is_any_smt_value_type\n" | |
| : "sort_is_not_any_smt_value_type\n"); | |
| // CHECK: int_type_is_not_a_bool | |
| fprintf(stderr, mlirSMTTypeIsABool(intType) ? "int_type_is_a_bool\n" | |
| : "int_type_is_not_a_bool\n"); | |
| // CHECK: bool_type_is_not_a_int | |
| fprintf(stderr, mlirSMTTypeIsAInt(boolType) ? "bool_type_is_a_int\n" | |
| : "bool_type_is_not_a_int\n"); | |
| // CHECK: bv_type_is_not_a_array | |
| fprintf(stderr, mlirSMTTypeIsAArray(bvType) ? "bv_type_is_a_array\n" | |
| : "bv_type_is_not_a_array\n"); | |
| // CHECK: array_type_is_not_a_bit_vector | |
| fprintf(stderr, mlirSMTTypeIsABitVector(arrayType) | |
| ? "array_type_is_a_bit_vector\n" | |
| : "array_type_is_not_a_bit_vector\n"); | |
| // CHECK: sort_type_is_not_a_smt_func | |
| fprintf(stderr, mlirSMTTypeIsASMTFunc(sortType) | |
| ? "sort_type_is_a_smt_func\n" | |
| : "sort_type_is_not_a_smt_func\n"); | |
| // CHECK: func_type_is_not_a_sort | |
| fprintf(stderr, mlirSMTTypeIsASort(funcType) ? "func_type_is_a_sort\n" | |
| : "func_type_is_not_a_sort\n"); | |
| } | |
| void testSMTAttribute(MlirContext ctx) { | |
| // CHECK: slt_is_BVCmpPredicate | |
| fprintf(stderr, mlirSMTAttrCheckBVCmpPredicate( | |
| ctx, mlirStringRefCreateFromCString("slt")) | |
| ? "slt_is_BVCmpPredicate\n" | |
| : "slt_is_not_BVCmpPredicate\n"); | |
| // CHECK: lt_is_not_BVCmpPredicate | |
| fprintf(stderr, mlirSMTAttrCheckBVCmpPredicate( | |
| ctx, mlirStringRefCreateFromCString("lt")) | |
| ? "lt_is_BVCmpPredicate\n" | |
| : "lt_is_not_BVCmpPredicate\n"); | |
| // CHECK: slt_is_not_IntPredicate | |
| fprintf(stderr, mlirSMTAttrCheckIntPredicate( | |
| ctx, mlirStringRefCreateFromCString("slt")) | |
| ? "slt_is_IntPredicate\n" | |
| : "slt_is_not_IntPredicate\n"); | |
| // CHECK: lt_is_IntPredicate | |
| fprintf(stderr, mlirSMTAttrCheckIntPredicate( | |
| ctx, mlirStringRefCreateFromCString("lt")) | |
| ? "lt_is_IntPredicate\n" | |
| : "lt_is_not_IntPredicate\n"); | |
| // CHECK: #smt.bv<5> : !smt.bv<32> | |
| mlirAttributeDump(mlirSMTAttrGetBitVector(ctx, 5, 32)); | |
| // CHECK: 0 : i64 | |
| mlirAttributeDump( | |
| mlirSMTAttrGetBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt"))); | |
| // CHECK: 0 : i64 | |
| mlirAttributeDump( | |
| mlirSMTAttrGetIntPredicate(ctx, mlirStringRefCreateFromCString("lt"))); | |
| } | |
| int main(void) { | |
| MlirContext ctx = mlirContextCreate(); | |
| mlirDialectHandleLoadDialect(mlirGetDialectHandle__smt__(), ctx); | |
| mlirDialectHandleLoadDialect(mlirGetDialectHandle__func__(), ctx); | |
| testExportSMTLIB(ctx); | |
| testSMTType(ctx); | |
| testSMTAttribute(ctx); | |
| mlirContextDestroy(ctx); | |
| return 0; | |
| } |