terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[ExportSMTLIB][CAPI] Add test for mlir export SMTLIB 

Signed-off-by: Clo91eaf <Clo91eaf@qq.com>
This commit is contained in:
Clo91eaf 2025-02-21 17:16:19 +08:00 committed by Asuna
parent 257426e53b
commit 6a6652d5c1
4 changed files with 72 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
test/CAPI/CMakeLists.txt
View File

@ -13,6 +13,7 @@ target_link_libraries(circt-capi-ir-test
CIRCTCAPISV
CIRCTCAPIFSM
CIRCTCAPIExportFIRRTL
CIRCTCAPIExportSMTLIB
CIRCTCAPIExportVerilog
)
@ -63,6 +64,21 @@ add_llvm_executable(circt-capi-arc-test
)
llvm_update_compile_flags(circt-capi-arc-test)
add_llvm_executable(circt-capi-smtlib-test
PARTIAL_SOURCES_INTENDED
smtlib.c
)
llvm_update_compile_flags(circt-capi-smtlib-test)
target_link_libraries(circt-capi-smtlib-test
PRIVATE
MLIRCAPIIR
MLIRCAPIFunc
CIRCTCAPISMT
CIRCTCAPIExportSMTLIB
)
target_link_libraries(circt-capi-arc-test
PRIVATE

52
test/CAPI/smtlib.c Normal file
View File

@ -0,0 +1,52 @@
/*===- smtlib.c - Simple test of SMTLIB C API -----------------------------===*\
|* *|
|* 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: circt-capi-smtlib-test 2>&1 | FileCheck %s
*/
#include "circt-c/Dialect/SMT.h"
#include "circt-c/ExportSMTLIB.h"
#include "mlir-c/Dialect/Func.h"
#include "mlir-c/IR.h"
#include "mlir-c/Support.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 = mlirExportSMTLIB(module, dumpCallback, NULL);
(void)result;
assert(mlirLogicalResultIsSuccess(result));
// CHECK: ; solver scope 0
// CHECK-NEXT: (reset)
}
int main(void) {
MlirContext ctx = mlirContextCreate();
mlirDialectHandleLoadDialect(mlirGetDialectHandle__smt__(), ctx);
mlirDialectHandleLoadDialect(mlirGetDialectHandle__func__(), ctx);
testExportSMTLIB(ctx);
return 0;
}

1
test/CMakeLists.txt
View File

@ -25,6 +25,7 @@ set(CIRCT_TEST_DEPENDS
circt-capi-rtg-pipelines-test
circt-capi-rtg-test
circt-capi-rtgtest-test
circt-capi-smtlib-test
circt-as
circt-bmc
circt-dis

6
test/lit.cfg.py
View File

@ -61,9 +61,9 @@ tools = [
'arcilator', 'circt-as', 'circt-capi-ir-test', 'circt-capi-om-test',
'circt-capi-firrtl-test', 'circt-capi-firtool-test',
'circt-capi-rtg-pipelines-test', 'circt-capi-rtg-test',
'circt-capi-rtgtest-test', 'circt-dis', 'circt-lec', 'circt-reduce',
'circt-synth', 'circt-test', 'circt-translate', 'firtool', 'hlstool',
'om-linker', 'kanagawatool'
'circt-capi-rtgtest-test', 'circt-capi-smtlib-test', 'circt-dis',
'circt-lec', 'circt-reduce', 'circt-synth', 'circt-test', 'circt-translate',
'firtool', 'hlstool', 'om-linker', 'kanagawatool'
]
if "CIRCT_OPT_CHECK_IR_ROUNDTRIP" in os.environ: