#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"
Go to the source code of this file.
|
using | ValueMap = llvm::ScopedHashTable< mlir::Value, std::string > |
|
|
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...
|
|
◆ DEBUG_TYPE
#define DEBUG_TYPE "export-smtlib" |
◆ 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.
◆ ValueMap
using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string> |
◆ emit()
static LogicalResult emit |
( |
SolverOp |
solver, |
|
|
const SMTEmissionOptions & |
options, |
|
|
mlir::raw_indented_ostream & |
stream |
|
) |
| |
|
static |