11 #include "mlir/IR/Builders.h"
12 #include "mlir/IR/DialectImplementation.h"
13 #include "llvm/ADT/TypeSwitch.h"
15 using namespace circt;
19 #define GET_TYPEDEF_CLASSES
20 #include "circt/Dialect/SMT/SMTTypes.cpp.inc"
22 void SMTDialect::registerTypes() {
24 #define GET_TYPEDEF_LIST
25 #include "circt/Dialect/SMT/SMTTypes.cpp.inc"
34 return isa<BoolType, BitVectorType, ArrayType, IntType, SortType,
43 BitVectorType::verify(function_ref<InFlightDiagnostic()> emitError,
46 return emitError() <<
"bit-vector must have at least a width of one";
54 LogicalResult ArrayType::verify(function_ref<InFlightDiagnostic()> emitError,
55 Type domainType, Type rangeType) {
57 return emitError() <<
"domain must be any SMT value type";
59 return emitError() <<
"range must be any SMT value type";
68 LogicalResult SMTFuncType::verify(function_ref<InFlightDiagnostic()> emitError,
69 ArrayRef<Type> domainTypes, Type rangeType) {
70 if (domainTypes.empty())
71 return emitError() <<
"domain must not be empty";
73 return emitError() <<
"domain types must be any non-function SMT type";
75 return emitError() <<
"range type must be any non-function SMT type";
84 LogicalResult SortType::verify(function_ref<InFlightDiagnostic()> emitError,
85 StringAttr identifier,
86 ArrayRef<Type> sortParams) {
89 <<
"sort parameter types must be any non-function SMT type";
bool isAnyNonFuncSMTValueType(mlir::Type type)
Returns whether the given type is an SMT value type (excluding functions).
bool isAnySMTValueType(mlir::Type type)
Returns whether the given type is an SMT value type.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.