CIRCT  19.0.0git
LTLVisitors.h
Go to the documentation of this file.
1 //===- LTLVisitors.h - LTL dialect visitors ---------------------*- C++ -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 
9 #ifndef CIRCT_DIALECT_LTL_LTLVISITORS_H
10 #define CIRCT_DIALECT_LTL_LTLVISITORS_H
11 
13 #include "llvm/ADT/TypeSwitch.h"
14 
15 namespace circt {
16 namespace ltl {
17 template <typename ConcreteType, typename ResultType = void,
18  typename... ExtraArgs>
19 class Visitor {
20 public:
21  ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args) {
22  auto *thisCast = static_cast<ConcreteType *>(this);
23  return TypeSwitch<Operation *, ResultType>(op)
24  .template Case<AndOp, OrOp, DelayOp, ConcatOp, NotOp, ImplicationOp,
25  EventuallyOp, ClockOp, DisableOp>(
26  [&](auto op) -> ResultType {
27  return thisCast->visitLTL(op, args...);
28  })
29  .Default([&](auto) -> ResultType {
30  return thisCast->visitInvalidLTL(op, args...);
31  });
32  }
33 
34  /// This callback is invoked on any non-LTL operations.
35  ResultType visitInvalidLTL(Operation *op, ExtraArgs... args) {
36  op->emitOpError("is not an LTL operation");
37  abort();
38  }
39 
40  /// This callback is invoked on any LTL operations that were not handled by
41  /// their concrete `visitLTL(...)` callback.
42  ResultType visitUnhandledLTL(Operation *op, ExtraArgs... args) {
43  return ResultType();
44  }
45 
46 #define HANDLE(OPTYPE, OPKIND) \
47  ResultType visitLTL(OPTYPE op, ExtraArgs... args) { \
48  return static_cast<ConcreteType *>(this)->visit##OPKIND##LTL(op, args...); \
49  }
50 
51  HANDLE(AndOp, Unhandled);
52  HANDLE(OrOp, Unhandled);
53  HANDLE(DelayOp, Unhandled);
54  HANDLE(ConcatOp, Unhandled);
55  HANDLE(NotOp, Unhandled);
56  HANDLE(ImplicationOp, Unhandled);
57  HANDLE(EventuallyOp, Unhandled);
58  HANDLE(ClockOp, Unhandled);
59  HANDLE(DisableOp, Unhandled);
60 #undef HANDLE
61 };
62 
63 } // namespace ltl
64 } // namespace circt
65 
66 #endif // CIRCT_DIALECT_LTL_LTLVISITORS_H
ResultType visitInvalidLTL(Operation *op, ExtraArgs... args)
This callback is invoked on any non-LTL operations.
Definition: LTLVisitors.h:35
HANDLE(AndOp, Unhandled)
HANDLE(DelayOp, Unhandled)
HANDLE(EventuallyOp, Unhandled)
ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args)
Definition: LTLVisitors.h:21
HANDLE(NotOp, Unhandled)
HANDLE(ClockOp, Unhandled)
HANDLE(ConcatOp, Unhandled)
HANDLE(DisableOp, Unhandled)
ResultType visitUnhandledLTL(Operation *op, ExtraArgs... args)
This callback is invoked on any LTL operations that were not handled by their concrete visitLTL(....
Definition: LTLVisitors.h:42
HANDLE(OrOp, Unhandled)
HANDLE(ImplicationOp, Unhandled)
This file defines an intermediate representation for circuits acting as an abstraction for constraint...
Definition: DebugAnalysis.h:21
Definition: ltl.py:1