37 lines · c
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-exception6//7//===----------------------------------------------------------------------===//8//9// This header declares the C interface for emitting SMTLIB from an MLIR module.10//11//===----------------------------------------------------------------------===//12 13#ifndef MLIR_C_EXPORTSMTLIB_H14#define MLIR_C_EXPORTSMTLIB_H15 16#include "mlir-c/IR.h"17 18#ifdef __cplusplus19extern "C" {20#endif21 22/// Emits SMTLIB for the specified module using the provided callback and user23/// data24MLIR_CAPI_EXPORTED MlirLogicalResult25mlirTranslateModuleToSMTLIB(MlirModule, MlirStringCallback, void *userData,26 bool inlineSingleUseValues, bool indentLetBody);27 28MLIR_CAPI_EXPORTED MlirLogicalResult mlirTranslateOperationToSMTLIB(29 MlirOperation, MlirStringCallback, void *userData,30 bool inlineSingleUseValues, bool indentLetBody);31 32#ifdef __cplusplus33}34#endif35 36#endif // MLIR_C_EXPORTSMTLIB_H37