ExportSMTLIB.cpp File Reference

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

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'.

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()

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

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

Referenced by mlir::MlirOptMainConfig::emitBytecode().