llzk::smt_info::detail Namespace Reference

Classes
class	SMTInfoSetOpGenericAdaptorBase

Functions
mlir::Attribute	getKeywordAttr (mlir::MLIRContext *context, llvm::StringRef value)
	Creates a keyword attribute without exposing generated attribute storage to operation implementation files.
mlir::Attribute	getSymbolAttr (mlir::MLIRContext *context, llvm::StringRef value)
	Creates a symbol attribute without exposing generated attribute storage to operation implementation files.
mlir::LogicalResult	verifyKeyword (llvm::function_ref< mlir::InFlightDiagnostic()> emitError, llvm::StringRef value)
	Verifies that value is a valid SMT-LIB keyword and reports failures through emitError.

Function Documentation

getKeywordAttr()

mlir::Attribute llzk::smt_info::detail::getKeywordAttr	(	mlir::MLIRContext *	context,
		llvm::StringRef	value )

Creates a keyword attribute without exposing generated attribute storage to operation implementation files.

getSymbolAttr()

mlir::Attribute llzk::smt_info::detail::getSymbolAttr	(	mlir::MLIRContext *	context,
		llvm::StringRef	value )

Creates a symbol attribute without exposing generated attribute storage to operation implementation files.

verifyKeyword()

mlir::LogicalResult llzk::smt_info::detail::verifyKeyword	(	llvm::function_ref< mlir::InFlightDiagnostic()>	emitError,
		llvm::StringRef	value )

Verifies that value is a valid SMT-LIB keyword and reports failures through emitError.