mlir::smt Namespace Reference

Namespaces
	detail

Classes
class	SMTOpVisitor
	This helps visit SMT nodes. More...
class	SMTTypeVisitor
	This helps visit SMT types. More...
struct	SMTEmissionOptions
	Emission options for the ExportSMTLIB pass. More...

Functions
bool	isAnySMTValueType (mlir::Type type)
	Returns whether the given type is an SMT value type. More...
bool	isAnyNonFuncSMTValueType (mlir::Type type)
	Returns whether the given type is an SMT value type (excluding functions). More...
void	registerExportSMTLIBTranslation ()
	Register the ExportSMTLIB pass. More...
LogicalResult	exportSMTLIB (Operation *module, llvm::raw_ostream &os, const SMTEmissionOptions &options=SMTEmissionOptions())
	Run the ExportSMTLIB pass. More...

Function Documentation

exportSMTLIB()

LogicalResult mlir::smt::exportSMTLIB	(	Operation *	module,
		llvm::raw_ostream &	os,
		const SMTEmissionOptions &	options = SMTEmissionOptions()
	)

Run the ExportSMTLIB pass.

Definition at line 682 of file ExportSMTLIB.cpp.

References mlir::WalkResult::advance(), emit(), mlir::Operation::emitError(), mlir::Operation::getNumRegions(), mlir::Operation::getRegion(), mlir::Region::hasOneBlock(), mlir::WalkResult::interrupt(), options, and mlir::Operation::walk().

Referenced by mlirTranslateOperationToSMTLIB(), and registerExportSMTLIBTranslation().

isAnyNonFuncSMTValueType()

bool mlir::smt::isAnyNonFuncSMTValueType

(

mlir::Type

type

)

Returns whether the given type is an SMT value type (excluding functions).

Definition at line 29 of file SMTTypes.cpp.

References isAnySMTValueType().

Referenced by mlirSMTTypeIsAnyNonFuncSMTValueType(), and verifyQuantifierRegions().

isAnySMTValueType()

bool mlir::smt::isAnySMTValueType

(

mlir::Type

type

)

Returns whether the given type is an SMT value type.

Definition at line 33 of file SMTTypes.cpp.

Referenced by isAnyNonFuncSMTValueType(), and mlirSMTTypeIsAnySMTValueType().

registerExportSMTLIBTranslation()

void mlir::smt::registerExportSMTLIBTranslation

(

)

Register the ExportSMTLIB pass.

Definition at line 706 of file ExportSMTLIB.cpp.

References exportSMTLIB(), and mlir::smt::SMTEmissionOptions::inlineSingleUseValues.

Referenced by mlir::registerAllTranslations().