CIRCT  20.0.0git
ExportSMTLIB.h
Go to the documentation of this file.
1 //===- ExportSMTLIB.h - SMT-LIB Exporter ------------------------*- 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 // Defines the interface to the SMT-LIB emitter.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef CIRCT_TARGET_EXPORTSMTLIB_H
14 #define CIRCT_TARGET_EXPORTSMTLIB_H
15 
16 #include "circt/Support/LLVM.h"
17 
18 namespace circt {
19 namespace ExportSMTLIB {
20 
21 /// Emission options for the ExportSMTLIB pass. Allows controlling the emitted
22 /// format and overall behavior.
24  // Don't produce 'let' expressions to bind expressions that are only used
25  // once, but inline them directly at the use-site.
26  bool inlineSingleUseValues = false;
27  // Increase indentation for each 'let' expression body.
28  bool indentLetBody = false;
29 };
30 
31 /// Run the ExportSMTLIB pass.
32 LogicalResult
33 exportSMTLIB(Operation *module, llvm::raw_ostream &os,
34  const SMTEmissionOptions &options = SMTEmissionOptions());
35 
36 /// Register the ExportSMTLIB pass.
38 
39 } // namespace ExportSMTLIB
40 } // namespace circt
41 
42 #endif // CIRCT_TARGET_EXPORTSMTLIB_H
LogicalResult exportSMTLIB(Operation *module, llvm::raw_ostream &os, const SMTEmissionOptions &options=SMTEmissionOptions())
Run the ExportSMTLIB pass.
void registerExportSMTLIBTranslation()
Register the ExportSMTLIB pass.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21
Emission options for the ExportSMTLIB pass.
Definition: ExportSMTLIB.h:23