1 | //===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===// |
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 | // Implements a C Interface for export SMTLIB. |
11 | // |
12 | //===----------------------------------------------------------------------===// |
13 | |
14 | #include "mlir-c/Target/ExportSMTLIB.h" |
15 | #include "mlir/CAPI/IR.h" |
16 | #include "mlir/CAPI/Support.h" |
17 | #include "mlir/CAPI/Utils.h" |
18 | #include "mlir/Target/SMTLIB/ExportSMTLIB.h" |
19 | |
20 | using namespace mlir; |
21 | |
22 | MlirLogicalResult mlirTranslateOperationToSMTLIB(MlirOperation module, |
23 | MlirStringCallback callback, |
24 | void *userData, |
25 | bool inlineSingleUseValues, |
26 | bool indentLetBody) { |
27 | mlir::detail::CallbackOstream stream(callback, userData); |
28 | smt::SMTEmissionOptions options; |
29 | options.inlineSingleUseValues = inlineSingleUseValues; |
30 | options.indentLetBody = indentLetBody; |
31 | return wrap(res: smt::exportSMTLIB(module: unwrap(c: module), os&: stream)); |
32 | } |
33 | |
34 | MlirLogicalResult mlirTranslateModuleToSMTLIB(MlirModule module, |
35 | MlirStringCallback callback, |
36 | void *userData, |
37 | bool inlineSingleUseValues, |
38 | bool indentLetBody) { |
39 | return mlirTranslateOperationToSMTLIB(module: mlirModuleGetOperation(module), |
40 | callback, userData, |
41 | inlineSingleUseValues, indentLetBody); |
42 | } |
43 | |