llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs > Class Template Reference

This helps visit SMT types. More...

#include <SMTVisitors.h>

Public Member Functions
ResultType	dispatchSMTTypeVisitor (mlir::Type type, ExtraArgs... args)
ResultType	visitInvalidSMTType (mlir::Type, ExtraArgs...)
	This callback is invoked on any non-expression types.
ResultType	visitUnhandledSMTType (mlir::Type, ExtraArgs...)
	This callback is invoked on any SMT type that are not handled by the concrete visitor.
	HANDLE (BoolType, Unhandled)
	HANDLE (IntType, Unhandled)
	HANDLE (BitVectorType, Unhandled)
	HANDLE (ArrayType, Unhandled)
	HANDLE (SMTFuncType, Unhandled)
	HANDLE (SortType, Unhandled)

Detailed Description

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>
class llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >

This helps visit SMT types.

Definition at line 152 of file SMTVisitors.h.

Member Function Documentation

dispatchSMTTypeVisitor()

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

ResultType llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::dispatchSMTTypeVisitor ( mlir::Type type, ExtraArgs... args )

inline

Definition at line 154 of file SMTVisitors.h.

HANDLE() [1/6]

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ArrayType	,
		Unhandled	)

HANDLE() [2/6]

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BitVectorType	,
		Unhandled	)

HANDLE() [3/6]

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BoolType	,
		Unhandled	)

HANDLE() [4/6]

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntType	,
		Unhandled	)

HANDLE() [5/6]

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	SMTFuncType	,
		Unhandled	)

HANDLE() [6/6]

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	SortType	,
		Unhandled	)

visitInvalidSMTType()

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

ResultType llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::visitInvalidSMTType ( mlir::Type , ExtraArgs...  )

inline

This callback is invoked on any non-expression types.

Definition at line 164 of file SMTVisitors.h.

visitUnhandledSMTType()

template<typename ConcreteType, typename ResultType = void, typename... ExtraArgs>

ResultType llzk::smt::SMTTypeVisitor< ConcreteType, ResultType, ExtraArgs >::visitUnhandledSMTType ( mlir::Type , ExtraArgs...  )

inline

This callback is invoked on any SMT type that are not handled by the concrete visitor.

Definition at line 168 of file SMTVisitors.h.

---

The documentation for this class was generated from the following file:

• include/llzk/Dialect/SMT/IR/SMTVisitors.h