mlir::smt Namespace Reference

Namespaces
namespace	detail

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

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

Function Documentation

exportSMTLIB()

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

Run the ExportSMTLIB pass.

Definition at line 681 of file ExportSMTLIB.cpp.

References mlir::Operation::getNumRegions(), mlir::Operation::getRegion(), mlir::Region::hasOneBlock(), options, and result.

Referenced by mlirTranslateOperationToSMTLIB().

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

Referenced by mlir::registerAllTranslations().