13 #ifndef CIRCT_DIALECT_SMT_SMTVISITORS_H
14 #define CIRCT_DIALECT_SMT_SMTVISITORS_H
17 #include "llvm/ADT/TypeSwitch.h"
23 template <
typename ConcreteType,
typename ResultType = void,
24 typename... ExtraArgs>
28 auto *thisCast =
static_cast<ConcreteType *
>(
this);
29 return TypeSwitch<Operation *, ResultType>(op)
32 BoolConstantOp, IntConstantOp, BVConstantOp,
34 BVNegOp, BVAddOp, BVMulOp, BVURemOp, BVSRemOp, BVSModOp, BVShlOp,
35 BVLShrOp, BVAShrOp, BVUDivOp, BVSDivOp,
37 BVNotOp, BVAndOp, BVOrOp, BVXOrOp,
39 ConcatOp, ExtractOp, RepeatOp, BVCmpOp,
41 IntAddOp, IntMulOp, IntSubOp, IntDivOp, IntModOp, IntCmpOp,
43 EqOp, DistinctOp, IteOp,
45 DeclareFunOp, ApplyFuncOp,
47 SolverOp, AssertOp, ResetOp, PushOp, PopOp, CheckOp,
49 NotOp, AndOp, OrOp, XOrOp, ImpliesOp,
51 ArrayStoreOp, ArraySelectOp, ArrayBroadcastOp,
53 ForallOp, ExistsOp, YieldOp>([&](
auto expr) -> ResultType {
54 return thisCast->visitSMTOp(expr, args...);
56 .Default([&](
auto expr) -> ResultType {
57 return thisCast->visitInvalidSMTOp(op, args...);
63 op->emitOpError(
"unknown SMT node");
73 #define HANDLE(OPTYPE, OPKIND) \
74 ResultType visitSMTOp(OPTYPE op, ExtraArgs... args) { \
75 return static_cast<ConcreteType *>(this)->visit##OPKIND##SMTOp(op, \
153 template <
typename ConcreteType,
typename ResultType = void,
154 typename... ExtraArgs>
158 auto *thisCast =
static_cast<ConcreteType *
>(
this);
159 return TypeSwitch<Type, ResultType>(type)
160 .template Case<BoolType, IntType, BitVectorType, ArrayType, SMTFuncType,
161 SortType>([&](
auto expr) -> ResultType {
162 return thisCast->visitSMTType(expr, args...);
164 .Default([&](
auto expr) -> ResultType {
165 return thisCast->visitInvalidSMTType(type, args...);
178 #define HANDLE(TYPE, KIND) \
179 ResultType visitSMTType(TYPE op, ExtraArgs... args) { \
180 return static_cast<ConcreteType *>(this)->visit##KIND##SMTType(op, \
This helps visit SMT nodes.
HANDLE(YieldOp, Unhandled)
HANDLE(PushOp, Unhandled)
HANDLE(BVAddOp, Unhandled)
HANDLE(DeclareFunOp, Unhandled)
HANDLE(BVOrOp, Unhandled)
HANDLE(ForallOp, Unhandled)
HANDLE(BVLShrOp, Unhandled)
HANDLE(ResetOp, Unhandled)
ResultType visitUnhandledSMTOp(Operation *op, ExtraArgs... args)
This callback is invoked on any SMT operations that are not handled by the concrete visitor.
HANDLE(BVUDivOp, Unhandled)
HANDLE(BVConstantOp, Unhandled)
ResultType visitInvalidSMTOp(Operation *op, ExtraArgs... args)
This callback is invoked on any non-expression operations.
HANDLE(BVAndOp, Unhandled)
HANDLE(BVMulOp, Unhandled)
HANDLE(IntConstantOp, Unhandled)
HANDLE(IntDivOp, Unhandled)
HANDLE(ApplyFuncOp, Unhandled)
HANDLE(IntModOp, Unhandled)
HANDLE(BVNotOp, Unhandled)
HANDLE(BVShlOp, Unhandled)
HANDLE(SolverOp, Unhandled)
HANDLE(RepeatOp, Unhandled)
HANDLE(BVSRemOp, Unhandled)
HANDLE(IntSubOp, Unhandled)
HANDLE(DistinctOp, Unhandled)
HANDLE(ImpliesOp, Unhandled)
HANDLE(BVAShrOp, Unhandled)
HANDLE(ArraySelectOp, Unhandled)
HANDLE(BVNegOp, Unhandled)
HANDLE(ArrayBroadcastOp, Unhandled)
HANDLE(BVSDivOp, Unhandled)
HANDLE(ExistsOp, Unhandled)
HANDLE(ArrayStoreOp, Unhandled)
ResultType dispatchSMTOpVisitor(Operation *op, ExtraArgs... args)
HANDLE(IntMulOp, Unhandled)
HANDLE(BVURemOp, Unhandled)
HANDLE(BVXOrOp, Unhandled)
HANDLE(IntAddOp, Unhandled)
HANDLE(ExtractOp, Unhandled)
HANDLE(BVSModOp, Unhandled)
HANDLE(ConcatOp, Unhandled)
HANDLE(IntCmpOp, Unhandled)
HANDLE(AssertOp, Unhandled)
HANDLE(CheckOp, Unhandled)
HANDLE(BVCmpOp, Unhandled)
HANDLE(BoolConstantOp, Unhandled)
This helps visit SMT types.
HANDLE(BitVectorType, Unhandled)
HANDLE(ArrayType, Unhandled)
HANDLE(BoolType, Unhandled)
HANDLE(SMTFuncType, Unhandled)
ResultType visitUnhandledSMTType(Type type, ExtraArgs... args)
This callback is invoked on any SMT type that are not handled by the concrete visitor.
HANDLE(SortType, Unhandled)
ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args)
HANDLE(IntegerType, Unhandled)
ResultType visitInvalidSMTType(Type type, ExtraArgs... args)
This callback is invoked on any non-expression types.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.