#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/Support/Format.h"

Include dependency graph for ExportSMTLIB.cpp:

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 31 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 207 of file ExportSMTLIB.cpp.

Typedef Documentation

◆ ValueMap

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

Definition at line 29 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 549 of file ExportSMTLIB.cpp.

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

Macros

Typedefs