#include "mlir/Target/SMTLIB/ExportSMTLIB.h"
#include "mlir/Dialect/Arith/Utils/Utils.h"
#include "mlir/Dialect/Func/IR/FuncOps.h"
#include "mlir/Dialect/SMT/IR/SMTOps.h"
#include "mlir/Dialect/SMT/IR/SMTVisitors.h"
#include "mlir/Support/IndentedOstream.h"
#include "mlir/Target/SMTLIB/Namespace.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"

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 32 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 208 of file ExportSMTLIB.cpp.

Typedef Documentation

◆ ValueMap

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

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

References mlir::WalkResult::advance(), mlir::Operation::emitError(), mlir::Operation::getDialect(), mlir::Operation::getResultTypes(), and mlir::Block::walk().

Referenced by mlir::MlirOptMainConfig::emitBytecode(), mlir::smt::exportSMTLIB(), and mlir::detail::ParallelDiagnosticHandlerImpl::~ParallelDiagnosticHandlerImpl().

Macros

Typedefs