MLIR  21.0.0git
ExportSMTLIB.h
Go to the documentation of this file.
1 //===- mlir-c/Target/ExportSMTLIB.h - C API for emitting SMTLIB ---*- C -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This header declares the C interface for emitting SMTLIB from an MLIR module.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef MLIR_C_EXPORTSMTLIB_H
14 #define MLIR_C_EXPORTSMTLIB_H
15 
16 #include "mlir-c/IR.h"
17 
18 #ifdef __cplusplus
19 extern "C" {
20 #endif
21 
22 /// Emits SMTLIB for the specified module using the provided callback and user
23 /// data
25 mlirTranslateModuleToSMTLIB(MlirModule, MlirStringCallback, void *userData,
26  bool inlineSingleUseValues, bool indentLetBody);
27 
29  MlirOperation, MlirStringCallback, void *userData,
30  bool inlineSingleUseValues, bool indentLetBody);
31 
32 #ifdef __cplusplus
33 }
34 #endif
35 
36 #endif // MLIR_C_EXPORTSMTLIB_H
#define MLIR_CAPI_EXPORTED
Definition: Support.h:46
void(* MlirStringCallback)(MlirStringRef, void *)
A callback for returning string references.
Definition: Support.h:105
MLIR_CAPI_EXPORTED MlirLogicalResult mlirTranslateOperationToSMTLIB(MlirOperation, MlirStringCallback, void *userData, bool inlineSingleUseValues, bool indentLetBody)
MLIR_CAPI_EXPORTED MlirLogicalResult mlirTranslateModuleToSMTLIB(MlirModule, MlirStringCallback, void *userData, bool inlineSingleUseValues, bool indentLetBody)
Emits SMTLIB for the specified module using the provided callback and user data.
A logical result value, essentially a boolean with named states.
Definition: Support.h:116