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, 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, \
150 template <
typename ConcreteType,
typename ResultType = void,
151 typename... ExtraArgs>
155 auto *thisCast =
static_cast<ConcreteType *
>(
this);
156 return TypeSwitch<Type, ResultType>(type)
157 .template Case<BoolType, IntType, BitVectorType, ArrayType, SMTFuncType,
158 SortType>([&](
auto expr) -> ResultType {
159 return thisCast->visitSMTType(expr, args...);
161 .Default([&](
auto expr) -> ResultType {
162 return thisCast->visitInvalidSMTType(type, args...);
175 #define HANDLE(TYPE, KIND) \
176 ResultType visitSMTType(TYPE op, ExtraArgs... args) { \
177 return static_cast<ConcreteType *>(this)->visit##KIND##SMTType(op, \
This helps visit SMT nodes.
HANDLE(YieldOp, Unhandled)
HANDLE(BVAddOp, Unhandled)
HANDLE(DeclareFunOp, Unhandled)
HANDLE(BVOrOp, Unhandled)
HANDLE(ForallOp, Unhandled)
HANDLE(BVLShrOp, 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.