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

This helps visit SMT nodes. More...

#include <SMTVisitors.h>

Public Member Functions
ResultType	dispatchSMTOpVisitor (Operation *op, ExtraArgs... args)
ResultType	visitInvalidSMTOp (Operation *op, ExtraArgs... args)
	This callback is invoked on any non-expression operations.
ResultType	visitUnhandledSMTOp (Operation *op, ExtraArgs... args)
	This callback is invoked on any SMT operations that are not handled by the concrete visitor.
	HANDLE (BoolConstantOp, Unhandled)
	HANDLE (IntConstantOp, Unhandled)
	HANDLE (BVConstantOp, Unhandled)
	HANDLE (BVNegOp, Unhandled)
	HANDLE (BVAddOp, Unhandled)
	HANDLE (BVMulOp, Unhandled)
	HANDLE (BVURemOp, Unhandled)
	HANDLE (BVSRemOp, Unhandled)
	HANDLE (BVSModOp, Unhandled)
	HANDLE (BVShlOp, Unhandled)
	HANDLE (BVLShrOp, Unhandled)
	HANDLE (BVAShrOp, Unhandled)
	HANDLE (BVUDivOp, Unhandled)
	HANDLE (BVSDivOp, Unhandled)
	HANDLE (BVNotOp, Unhandled)
	HANDLE (BVAndOp, Unhandled)
	HANDLE (BVOrOp, Unhandled)
	HANDLE (BVXOrOp, Unhandled)
	HANDLE (ConcatOp, Unhandled)
	HANDLE (ExtractOp, Unhandled)
	HANDLE (RepeatOp, Unhandled)
	HANDLE (BVCmpOp, Unhandled)
	HANDLE (BV2IntOp, Unhandled)
	HANDLE (IntAddOp, Unhandled)
	HANDLE (IntMulOp, Unhandled)
	HANDLE (IntSubOp, Unhandled)
	HANDLE (IntDivOp, Unhandled)
	HANDLE (IntModOp, Unhandled)
	HANDLE (IntCmpOp, Unhandled)
	HANDLE (Int2BVOp, Unhandled)
	HANDLE (EqOp, Unhandled)
	HANDLE (DistinctOp, Unhandled)
	HANDLE (IteOp, Unhandled)
	HANDLE (DeclareFunOp, Unhandled)
	HANDLE (ApplyFuncOp, Unhandled)
	HANDLE (SolverOp, Unhandled)
	HANDLE (AssertOp, Unhandled)
	HANDLE (ResetOp, Unhandled)
	HANDLE (PushOp, Unhandled)
	HANDLE (PopOp, Unhandled)
	HANDLE (CheckOp, Unhandled)
	HANDLE (SetLogicOp, Unhandled)
	HANDLE (NotOp, Unhandled)
	HANDLE (AndOp, Unhandled)
	HANDLE (OrOp, Unhandled)
	HANDLE (XOrOp, Unhandled)
	HANDLE (ImpliesOp, Unhandled)
	HANDLE (ArrayStoreOp, Unhandled)
	HANDLE (ArraySelectOp, Unhandled)
	HANDLE (ArrayBroadcastOp, Unhandled)
	HANDLE (ForallOp, Unhandled)
	HANDLE (ExistsOp, Unhandled)
	HANDLE (YieldOp, Unhandled)

Detailed Description

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

This helps visit SMT nodes.

Definition at line 25 of file SMTVisitors.h.

Member Function Documentation

dispatchSMTOpVisitor()

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

ResultType llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::dispatchSMTOpVisitor ( Operation * op, ExtraArgs... args )

inline

Definition at line 27 of file SMTVisitors.h.

HANDLE() [1/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	AndOp	,
		Unhandled	)

HANDLE() [2/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ApplyFuncOp	,
		Unhandled	)

HANDLE() [3/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ArrayBroadcastOp	,
		Unhandled	)

HANDLE() [4/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ArraySelectOp	,
		Unhandled	)

HANDLE() [5/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ArrayStoreOp	,
		Unhandled	)

HANDLE() [6/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	AssertOp	,
		Unhandled	)

HANDLE() [7/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BoolConstantOp	,
		Unhandled	)

HANDLE() [8/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BV2IntOp	,
		Unhandled	)

HANDLE() [9/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVAddOp	,
		Unhandled	)

HANDLE() [10/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVAndOp	,
		Unhandled	)

HANDLE() [11/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVAShrOp	,
		Unhandled	)

HANDLE() [12/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVCmpOp	,
		Unhandled	)

HANDLE() [13/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVConstantOp	,
		Unhandled	)

HANDLE() [14/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVLShrOp	,
		Unhandled	)

HANDLE() [15/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVMulOp	,
		Unhandled	)

HANDLE() [16/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVNegOp	,
		Unhandled	)

HANDLE() [17/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVNotOp	,
		Unhandled	)

HANDLE() [18/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVOrOp	,
		Unhandled	)

HANDLE() [19/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVSDivOp	,
		Unhandled	)

HANDLE() [20/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVShlOp	,
		Unhandled	)

HANDLE() [21/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVSModOp	,
		Unhandled	)

HANDLE() [22/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVSRemOp	,
		Unhandled	)

HANDLE() [23/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVUDivOp	,
		Unhandled	)

HANDLE() [24/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVURemOp	,
		Unhandled	)

HANDLE() [25/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	BVXOrOp	,
		Unhandled	)

HANDLE() [26/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	CheckOp	,
		Unhandled	)

HANDLE() [27/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ConcatOp	,
		Unhandled	)

HANDLE() [28/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	DeclareFunOp	,
		Unhandled	)

HANDLE() [29/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	DistinctOp	,
		Unhandled	)

HANDLE() [30/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	EqOp	,
		Unhandled	)

HANDLE() [31/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ExistsOp	,
		Unhandled	)

HANDLE() [32/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ExtractOp	,
		Unhandled	)

HANDLE() [33/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ForallOp	,
		Unhandled	)

HANDLE() [34/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ImpliesOp	,
		Unhandled	)

HANDLE() [35/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	Int2BVOp	,
		Unhandled	)

HANDLE() [36/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntAddOp	,
		Unhandled	)

HANDLE() [37/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntCmpOp	,
		Unhandled	)

HANDLE() [38/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntConstantOp	,
		Unhandled	)

HANDLE() [39/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntDivOp	,
		Unhandled	)

HANDLE() [40/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntModOp	,
		Unhandled	)

HANDLE() [41/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntMulOp	,
		Unhandled	)

HANDLE() [42/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IntSubOp	,
		Unhandled	)

HANDLE() [43/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	IteOp	,
		Unhandled	)

HANDLE() [44/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	NotOp	,
		Unhandled	)

HANDLE() [45/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	OrOp	,
		Unhandled	)

HANDLE() [46/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	PopOp	,
		Unhandled	)

HANDLE() [47/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	PushOp	,
		Unhandled	)

HANDLE() [48/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	RepeatOp	,
		Unhandled	)

HANDLE() [49/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	ResetOp	,
		Unhandled	)

HANDLE() [50/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	SetLogicOp	,
		Unhandled	)

HANDLE() [51/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	SolverOp	,
		Unhandled	)

HANDLE() [52/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	XOrOp	,
		Unhandled	)

HANDLE() [53/53]

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

llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::HANDLE	(	YieldOp	,
		Unhandled	)

visitInvalidSMTOp()

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

ResultType llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::visitInvalidSMTOp ( Operation * op, ExtraArgs... args )

inline

This callback is invoked on any non-expression operations.

Definition at line 59 of file SMTVisitors.h.

visitUnhandledSMTOp()

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

ResultType llzk::smt::SMTOpVisitor< ConcreteType, ResultType, ExtraArgs >::visitUnhandledSMTOp ( Operation * op, ExtraArgs... args )

inline

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

Definition at line 66 of file SMTVisitors.h.

---

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

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