CIRCT  20.0.0git
Macros | Typedefs | Functions
ExportSMTLIB.cpp File Reference
#include "circt/Target/ExportSMTLIB.h"
#include "circt/Dialect/HW/HWDialect.h"
#include "circt/Dialect/SMT/SMTOps.h"
#include "circt/Dialect/SMT/SMTVisitors.h"
#include "circt/Support/Namespace.h"
#include "mlir/Dialect/Func/IR/FuncOps.h"
#include "mlir/IR/BuiltinOps.h"
#include "mlir/Support/IndentedOstream.h"
#include "mlir/Tools/mlir-translate/Translation.h"
#include "llvm/ADT/ScopedHashTable.h"
#include "llvm/ADT/StringRef.h"
#include "llvm/Support/Format.h"
#include "llvm/Support/raw_ostream.h"
Include dependency graph for ExportSMTLIB.cpp:

Go to the source code of this file.

Macros

#define DEBUG_TYPE   "export-smtlib"
 
#define HANDLE_OP(OPTYPE, NAME, KIND)
 

Typedefs

using ValueMap = llvm::ScopedHashTable< mlir::Value, std::string >
 

Functions

static LogicalResult emit (SolverOp solver, const SMTEmissionOptions &options, mlir::raw_indented_ostream &stream)
 Emit the SMT operations in the given 'solver' to the 'stream'. More...
 

Macro Definition Documentation

◆ DEBUG_TYPE

#define DEBUG_TYPE   "export-smtlib"

Definition at line 33 of file ExportSMTLIB.cpp.

◆ HANDLE_OP

#define HANDLE_OP (   OPTYPE,
  NAME,
  KIND 
)
Value:
LogicalResult visitSMTOp(OPTYPE op, VisitorInfo &info) { \
return print##KIND##Op(op, NAME, info); \
}

Definition at line 209 of file ExportSMTLIB.cpp.

Typedef Documentation

◆ ValueMap

using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>

Definition at line 31 of file ExportSMTLIB.cpp.

Function Documentation

◆ emit()

static LogicalResult emit ( SolverOp  solver,
const SMTEmissionOptions options,
mlir::raw_indented_ostream &  stream 
)
static

Emit the SMT operations in the given 'solver' to the 'stream'.

Definition at line 617 of file ExportSMTLIB.cpp.

Referenced by circt::ExportSMTLIB::exportSMTLIB().