SMTTypes.cpp.inc

Go to the documentation of this file.

/*===- TableGen'erated file -------------------------------------*- C++ -*-===*\
|*                                                                            *|
|* TypeDef Definitions                                                        *|
|*                                                                            *|
|* Automatically generated file, do not edit!                                 *|
|*                                                                            *|
\*===----------------------------------------------------------------------===*/
 
#ifdef GET_TYPEDEF_LIST
#undef GET_TYPEDEF_LIST
 
::llzk::smt::BoolType,
::llzk::smt::IntType,
::llzk::smt::BitVectorType,
::llzk::smt::ArrayType,
::llzk::smt::SMTFuncType,
::llzk::smt::SortType
 
#endif  // GET_TYPEDEF_LIST
 
#ifdef GET_TYPEDEF_CLASSES
#undef GET_TYPEDEF_CLASSES
 
static ::mlir::OptionalParseResult generatedTypeParser(::mlir::AsmParser &parser, ::llvm::StringRef *mnemonic, ::mlir::Type &value) {
  return ::mlir::AsmParser::KeywordSwitch<::mlir::OptionalParseResult>(parser)
    .Case(::llzk::smt::BoolType::getMnemonic(), [&](llvm::StringRef, llvm::SMLoc) {
      value = ::llzk::smt::BoolType::parse(parser);
      return ::mlir::success(!!value);
    })
    .Case(::llzk::smt::IntType::getMnemonic(), [&](llvm::StringRef, llvm::SMLoc) {
      value = ::llzk::smt::IntType::parse(parser);
      return ::mlir::success(!!value);
    })
    .Case(::llzk::smt::BitVectorType::getMnemonic(), [&](llvm::StringRef, llvm::SMLoc) {
      value = ::llzk::smt::BitVectorType::parse(parser);
      return ::mlir::success(!!value);
    })
    .Case(::llzk::smt::ArrayType::getMnemonic(), [&](llvm::StringRef, llvm::SMLoc) {
      value = ::llzk::smt::ArrayType::parse(parser);
      return ::mlir::success(!!value);
    })
    .Case(::llzk::smt::SMTFuncType::getMnemonic(), [&](llvm::StringRef, llvm::SMLoc) {
      value = ::llzk::smt::SMTFuncType::parse(parser);
      return ::mlir::success(!!value);
    })
    .Case(::llzk::smt::SortType::getMnemonic(), [&](llvm::StringRef, llvm::SMLoc) {
      value = ::llzk::smt::SortType::parse(parser);
      return ::mlir::success(!!value);
    })
    .Default([&](llvm::StringRef keyword, llvm::SMLoc) {
      *mnemonic = keyword;
      return std::nullopt;
    });
}
 
static ::llvm::LogicalResult generatedTypePrinter(::mlir::Type def, ::mlir::AsmPrinter &printer) {
  return ::llvm::TypeSwitch<::mlir::Type, ::llvm::LogicalResult>(def)    .Case<::llzk::smt::BoolType>([&](auto t) {
      printer << ::llzk::smt::BoolType::getMnemonic();
t.print(printer);
      return ::mlir::success();
    })
    .Case<::llzk::smt::IntType>([&](auto t) {
      printer << ::llzk::smt::IntType::getMnemonic();
t.print(printer);
      return ::mlir::success();
    })
    .Case<::llzk::smt::BitVectorType>([&](auto t) {
      printer << ::llzk::smt::BitVectorType::getMnemonic();
t.print(printer);
      return ::mlir::success();
    })
    .Case<::llzk::smt::ArrayType>([&](auto t) {
      printer << ::llzk::smt::ArrayType::getMnemonic();
t.print(printer);
      return ::mlir::success();
    })
    .Case<::llzk::smt::SMTFuncType>([&](auto t) {
      printer << ::llzk::smt::SMTFuncType::getMnemonic();
t.print(printer);
      return ::mlir::success();
    })
    .Case<::llzk::smt::SortType>([&](auto t) {
      printer << ::llzk::smt::SortType::getMnemonic();
t.print(printer);
      return ::mlir::success();
    })
    .Default([](auto) { return ::mlir::failure(); });
}
 
namespace llzk {
namespace smt {
::mlir::Type BoolType::parse(::mlir::AsmParser &odsParser) {
  ::mlir::Builder odsBuilder(odsParser.getContext());
  ::llvm::SMLoc odsLoc = odsParser.getCurrentLocation();
  (void) odsLoc;
  return BoolType::get(odsParser.getContext());
}
 
void BoolType::print(::mlir::AsmPrinter &odsPrinter) const {
  ::mlir::Builder odsBuilder(getContext());
}
 
} // namespace smt
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::smt::BoolType)
namespace llzk {
namespace smt {
::mlir::Type IntType::parse(::mlir::AsmParser &odsParser) {
  ::mlir::Builder odsBuilder(odsParser.getContext());
  ::llvm::SMLoc odsLoc = odsParser.getCurrentLocation();
  (void) odsLoc;
  return IntType::get(odsParser.getContext());
}
 
void IntType::print(::mlir::AsmPrinter &odsPrinter) const {
  ::mlir::Builder odsBuilder(getContext());
}
 
} // namespace smt
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::smt::IntType)
namespace llzk {
namespace smt {
namespace detail {
struct BitVectorTypeStorage : public ::mlir::TypeStorage {
  using KeyTy = std::tuple<int64_t>;
  BitVectorTypeStorage(int64_t width) : width(std::move(width)) {}
 
  KeyTy getAsKey() const {
    return KeyTy(width);
  }
 
  bool operator==(const KeyTy &tblgenKey) const {
    return (width == std::get<0>(tblgenKey));
  }
 
  static ::llvm::hash_code hashKey(const KeyTy &tblgenKey) {
    return ::llvm::hash_combine(std::get<0>(tblgenKey));
  }
 
  static BitVectorTypeStorage *construct(::mlir::TypeStorageAllocator &allocator, KeyTy &&tblgenKey) {
    auto width = std::move(std::get<0>(tblgenKey));
    return new (allocator.allocate<BitVectorTypeStorage>()) BitVectorTypeStorage(std::move(width));
  }
 
  int64_t width;
};
} // namespace detail
BitVectorType BitVectorType::get(::mlir::MLIRContext *context, int64_t width) {
  return Base::get(context, std::move(width));
}
 
BitVectorType BitVectorType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, int64_t width) {
  return Base::getChecked(emitError, context, width);
}
 
::llvm::LogicalResult BitVectorType::verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, int64_t width) {
  if (::mlir::failed(verify(emitError, width)))
    return ::mlir::failure();
  return ::mlir::success();
}
 
::mlir::Type BitVectorType::parse(::mlir::AsmParser &odsParser) {
  ::mlir::Builder odsBuilder(odsParser.getContext());
  ::llvm::SMLoc odsLoc = odsParser.getCurrentLocation();
  (void) odsLoc;
  ::mlir::FailureOr<int64_t> _result_width;
  // Parse literal '<'
  if (odsParser.parseLess()) return {};
 
  // Parse variable 'width'
  _result_width = ::mlir::FieldParser<int64_t>::parse(odsParser);
  if (::mlir::failed(_result_width)) {
    odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse BitVectorType parameter 'width' which is to be a `int64_t`");
    return {};
  }
  // Parse literal '>'
  if (odsParser.parseGreater()) return {};
  assert(::mlir::succeeded(_result_width));
  return odsParser.getChecked<BitVectorType>(odsLoc, odsParser.getContext(),
      int64_t((*_result_width)));
}
 
void BitVectorType::print(::mlir::AsmPrinter &odsPrinter) const {
  ::mlir::Builder odsBuilder(getContext());
  odsPrinter << "<";
  odsPrinter.printStrippedAttrOrType(getWidth());
  odsPrinter << ">";
}
 
int64_t BitVectorType::getWidth() const {
  return getImpl()->width;
}
 
} // namespace smt
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::smt::BitVectorType)
namespace llzk {
namespace smt {
namespace detail {
struct ArrayTypeStorage : public ::mlir::TypeStorage {
  using KeyTy = std::tuple<mlir::Type, mlir::Type>;
  ArrayTypeStorage(mlir::Type domainType, mlir::Type rangeType) : domainType(std::move(domainType)), rangeType(std::move(rangeType)) {}
 
  KeyTy getAsKey() const {
    return KeyTy(domainType, rangeType);
  }
 
  bool operator==(const KeyTy &tblgenKey) const {
    return (domainType == std::get<0>(tblgenKey)) && (rangeType == std::get<1>(tblgenKey));
  }
 
  static ::llvm::hash_code hashKey(const KeyTy &tblgenKey) {
    return ::llvm::hash_combine(std::get<0>(tblgenKey), std::get<1>(tblgenKey));
  }
 
  static ArrayTypeStorage *construct(::mlir::TypeStorageAllocator &allocator, KeyTy &&tblgenKey) {
    auto domainType = std::move(std::get<0>(tblgenKey));
    auto rangeType = std::move(std::get<1>(tblgenKey));
    return new (allocator.allocate<ArrayTypeStorage>()) ArrayTypeStorage(std::move(domainType), std::move(rangeType));
  }
 
  mlir::Type domainType;
  mlir::Type rangeType;
};
} // namespace detail
ArrayType ArrayType::get(::mlir::MLIRContext *context, mlir::Type domainType, mlir::Type rangeType) {
  return Base::get(context, std::move(domainType), std::move(rangeType));
}
 
ArrayType ArrayType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, mlir::Type domainType, mlir::Type rangeType) {
  return Base::getChecked(emitError, context, domainType, rangeType);
}
 
::llvm::LogicalResult ArrayType::verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::Type domainType, mlir::Type rangeType) {
  if (::mlir::failed(verify(emitError, domainType, rangeType)))
    return ::mlir::failure();
  return ::mlir::success();
}
 
::mlir::Type ArrayType::parse(::mlir::AsmParser &odsParser) {
  ::mlir::Builder odsBuilder(odsParser.getContext());
  ::llvm::SMLoc odsLoc = odsParser.getCurrentLocation();
  (void) odsLoc;
  ::mlir::FailureOr<mlir::Type> _result_domainType;
  ::mlir::FailureOr<mlir::Type> _result_rangeType;
  // Parse literal '<'
  if (odsParser.parseLess()) return {};
  // Parse literal '['
  if (odsParser.parseLSquare()) return {};
 
  // Parse variable 'domainType'
  _result_domainType = ::mlir::FieldParser<mlir::Type>::parse(odsParser);
  if (::mlir::failed(_result_domainType)) {
    odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse ArrayType parameter 'domainType' which is to be a `mlir::Type`");
    return {};
  }
  // Parse literal '->'
  if (odsParser.parseArrow()) return {};
 
  // Parse variable 'rangeType'
  _result_rangeType = ::mlir::FieldParser<mlir::Type>::parse(odsParser);
  if (::mlir::failed(_result_rangeType)) {
    odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse ArrayType parameter 'rangeType' which is to be a `mlir::Type`");
    return {};
  }
  // Parse literal ']'
  if (odsParser.parseRSquare()) return {};
  // Parse literal '>'
  if (odsParser.parseGreater()) return {};
  assert(::mlir::succeeded(_result_domainType));
  assert(::mlir::succeeded(_result_rangeType));
  return odsParser.getChecked<ArrayType>(odsLoc, odsParser.getContext(),
      mlir::Type((*_result_domainType)),
      mlir::Type((*_result_rangeType)));
}
 
void ArrayType::print(::mlir::AsmPrinter &odsPrinter) const {
  ::mlir::Builder odsBuilder(getContext());
  odsPrinter << "<";
  odsPrinter << "[";
  odsPrinter.printStrippedAttrOrType(getDomainType());
  odsPrinter << ' ' << "->";
  odsPrinter << ' ';
  odsPrinter.printStrippedAttrOrType(getRangeType());
  odsPrinter << "]";
  odsPrinter << ">";
}
 
mlir::Type ArrayType::getDomainType() const {
  return getImpl()->domainType;
}
 
mlir::Type ArrayType::getRangeType() const {
  return getImpl()->rangeType;
}
 
} // namespace smt
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::smt::ArrayType)
namespace llzk {
namespace smt {
namespace detail {
struct SMTFuncTypeStorage : public ::mlir::TypeStorage {
  using KeyTy = std::tuple<::llvm::ArrayRef<mlir::Type>, mlir::Type>;
  SMTFuncTypeStorage(::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType) : domainTypes(std::move(domainTypes)), rangeType(std::move(rangeType)) {}
 
  KeyTy getAsKey() const {
    return KeyTy(domainTypes, rangeType);
  }
 
  bool operator==(const KeyTy &tblgenKey) const {
    return (domainTypes == std::get<0>(tblgenKey)) && (rangeType == std::get<1>(tblgenKey));
  }
 
  static ::llvm::hash_code hashKey(const KeyTy &tblgenKey) {
    return ::llvm::hash_combine(std::get<0>(tblgenKey), std::get<1>(tblgenKey));
  }
 
  static SMTFuncTypeStorage *construct(::mlir::TypeStorageAllocator &allocator, KeyTy &&tblgenKey) {
    auto domainTypes = std::move(std::get<0>(tblgenKey));
    auto rangeType = std::move(std::get<1>(tblgenKey));
    domainTypes = allocator.copyInto(domainTypes);
    return new (allocator.allocate<SMTFuncTypeStorage>()) SMTFuncTypeStorage(std::move(domainTypes), std::move(rangeType));
  }
 
  ::llvm::ArrayRef<mlir::Type> domainTypes;
  mlir::Type rangeType;
};
} // namespace detail
SMTFuncType SMTFuncType::get(::mlir::MLIRContext *context, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType) {
  return Base::get(context, std::move(domainTypes), std::move(rangeType));
}
 
SMTFuncType SMTFuncType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType) {
  return Base::getChecked(emitError, context, domainTypes, rangeType);
}
 
SMTFuncType SMTFuncType::get(llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType) {
  return Base::get(rangeType.getContext(), domainTypes, rangeType);
}
 
SMTFuncType SMTFuncType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType) {
  return Base::getChecked(emitError, rangeType.getContext(), domainTypes, rangeType);
}
 
SMTFuncType SMTFuncType::get(mlir::Type rangeType) {
  return Base::get(rangeType.getContext(),
               llvm::ArrayRef<mlir::Type>{}, rangeType);
}
 
SMTFuncType SMTFuncType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::Type rangeType) {
  return Base::getChecked(emitError, rangeType.getContext(),
               llvm::ArrayRef<mlir::Type>{}, rangeType);
}
 
::llvm::LogicalResult SMTFuncType::verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType) {
  if (::mlir::failed(verify(emitError, domainTypes, rangeType)))
    return ::mlir::failure();
  return ::mlir::success();
}
 
::mlir::Type SMTFuncType::parse(::mlir::AsmParser &odsParser) {
  ::mlir::Builder odsBuilder(odsParser.getContext());
  ::llvm::SMLoc odsLoc = odsParser.getCurrentLocation();
  (void) odsLoc;
  ::mlir::FailureOr<::llvm::SmallVector<mlir::Type>> _result_domainTypes;
  ::mlir::FailureOr<mlir::Type> _result_rangeType;
  // Parse literal '<'
  if (odsParser.parseLess()) return {};
  // Parse literal '('
  if (odsParser.parseLParen()) return {};
 
  // Parse variable 'domainTypes'
  _result_domainTypes = ::mlir::FieldParser<::llvm::SmallVector<mlir::Type>>::parse(odsParser);
  if (::mlir::failed(_result_domainTypes)) {
    odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse SMTFuncType parameter 'domainTypes' which is to be a `::llvm::ArrayRef<mlir::Type>`");
    return {};
  }
  // Parse literal ')'
  if (odsParser.parseRParen()) return {};
 
  // Parse variable 'rangeType'
  _result_rangeType = ::mlir::FieldParser<mlir::Type>::parse(odsParser);
  if (::mlir::failed(_result_rangeType)) {
    odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse SMTFuncType parameter 'rangeType' which is to be a `mlir::Type`");
    return {};
  }
  // Parse literal '>'
  if (odsParser.parseGreater()) return {};
  assert(::mlir::succeeded(_result_domainTypes));
  assert(::mlir::succeeded(_result_rangeType));
  return odsParser.getChecked<SMTFuncType>(odsLoc, odsParser.getContext(),
      ::llvm::ArrayRef<mlir::Type>((*_result_domainTypes)),
      mlir::Type((*_result_rangeType)));
}
 
void SMTFuncType::print(::mlir::AsmPrinter &odsPrinter) const {
  ::mlir::Builder odsBuilder(getContext());
  odsPrinter << "<";
  odsPrinter << "(";
  odsPrinter.printStrippedAttrOrType(getDomainTypes());
  odsPrinter << ")";
  odsPrinter << " ";
  odsPrinter.printStrippedAttrOrType(getRangeType());
  odsPrinter << ">";
}
 
::llvm::ArrayRef<mlir::Type> SMTFuncType::getDomainTypes() const {
  return getImpl()->domainTypes;
}
 
mlir::Type SMTFuncType::getRangeType() const {
  return getImpl()->rangeType;
}
 
} // namespace smt
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::smt::SMTFuncType)
namespace llzk {
namespace smt {
namespace detail {
struct SortTypeStorage : public ::mlir::TypeStorage {
  using KeyTy = std::tuple<mlir::StringAttr, ::llvm::ArrayRef<mlir::Type>>;
  SortTypeStorage(mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams) : identifier(std::move(identifier)), sortParams(std::move(sortParams)) {}
 
  KeyTy getAsKey() const {
    return KeyTy(identifier, sortParams);
  }
 
  bool operator==(const KeyTy &tblgenKey) const {
    return (identifier == std::get<0>(tblgenKey)) && (::llvm::ArrayRef<mlir::Type>(sortParams) == ::llvm::ArrayRef<mlir::Type>(std::get<1>(tblgenKey)));
  }
 
  static ::llvm::hash_code hashKey(const KeyTy &tblgenKey) {
    return ::llvm::hash_combine(std::get<0>(tblgenKey), std::get<1>(tblgenKey));
  }
 
  static SortTypeStorage *construct(::mlir::TypeStorageAllocator &allocator, KeyTy &&tblgenKey) {
    auto identifier = std::move(std::get<0>(tblgenKey));
    auto sortParams = std::move(std::get<1>(tblgenKey));
    sortParams = allocator.copyInto(sortParams);
    return new (allocator.allocate<SortTypeStorage>()) SortTypeStorage(std::move(identifier), std::move(sortParams));
  }
 
  mlir::StringAttr identifier;
  ::llvm::ArrayRef<mlir::Type> sortParams;
};
} // namespace detail
SortType SortType::get(::mlir::MLIRContext *context, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams) {
  return Base::get(context, std::move(identifier), std::move(sortParams));
}
 
SortType SortType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams) {
  return Base::getChecked(emitError, context, identifier, sortParams);
}
 
SortType SortType::get(::mlir::MLIRContext *context, llvm::StringRef identifier, llvm::ArrayRef<mlir::Type> sortParams) {
  return Base::get(context, mlir::StringAttr::get(context, identifier),
                       sortParams);
}
 
SortType SortType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, llvm::StringRef identifier, llvm::ArrayRef<mlir::Type> sortParams) {
  return Base::getChecked(emitError, context, mlir::StringAttr::get(context, identifier),
                       sortParams);
}
 
SortType SortType::get(::mlir::MLIRContext *context, llvm::StringRef identifier) {
  return Base::get(context, mlir::StringAttr::get(context, identifier),
                llvm::ArrayRef<mlir::Type>{});
}
 
SortType SortType::getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, llvm::StringRef identifier) {
  return Base::getChecked(emitError, context, mlir::StringAttr::get(context, identifier),
                llvm::ArrayRef<mlir::Type>{});
}
 
::llvm::LogicalResult SortType::verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams) {
  if (::mlir::failed(verify(emitError, identifier, sortParams)))
    return ::mlir::failure();
  return ::mlir::success();
}
 
::mlir::Type SortType::parse(::mlir::AsmParser &odsParser) {
  ::mlir::Builder odsBuilder(odsParser.getContext());
  ::llvm::SMLoc odsLoc = odsParser.getCurrentLocation();
  (void) odsLoc;
  ::mlir::FailureOr<mlir::StringAttr> _result_identifier;
  ::mlir::FailureOr<::llvm::SmallVector<mlir::Type>> _result_sortParams;
  // Parse literal '<'
  if (odsParser.parseLess()) return {};
 
  // Parse variable 'identifier'
  _result_identifier = ::mlir::FieldParser<mlir::StringAttr>::parse(odsParser);
  if (::mlir::failed(_result_identifier)) {
    odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse SortType parameter 'identifier' which is to be a `mlir::StringAttr`");
    return {};
  }
  // Parse literal '['
  if (odsParser.parseOptionalLSquare()) {
  } else {
 
    // Parse variable 'sortParams'
    _result_sortParams = ::mlir::FieldParser<::llvm::SmallVector<mlir::Type>>::parse(odsParser);
    if (::mlir::failed(_result_sortParams)) {
      odsParser.emitError(odsParser.getCurrentLocation(), "failed to parse SortType parameter 'sortParams' which is to be a `::llvm::ArrayRef<mlir::Type>`");
      return {};
    }
    // Parse literal ']'
    if (odsParser.parseRSquare()) return {};
  }
  // Parse literal '>'
  if (odsParser.parseGreater()) return {};
  assert(::mlir::succeeded(_result_identifier));
  return odsParser.getChecked<SortType>(odsLoc, odsParser.getContext(),
      mlir::StringAttr((*_result_identifier)),
      ::llvm::ArrayRef<mlir::Type>((_result_sortParams.value_or(::llvm::SmallVector<mlir::Type>()))));
}
 
void SortType::print(::mlir::AsmPrinter &odsPrinter) const {
  ::mlir::Builder odsBuilder(getContext());
  odsPrinter << "<";
  odsPrinter.printStrippedAttrOrType(getIdentifier());
  if (!(::llvm::ArrayRef<mlir::Type>(getSortParams()) == ::llvm::ArrayRef<mlir::Type>(::llvm::SmallVector<mlir::Type>()))) {
    odsPrinter << "[";
    if (!(::llvm::ArrayRef<mlir::Type>(getSortParams()) == ::llvm::ArrayRef<mlir::Type>(::llvm::SmallVector<mlir::Type>()))) {
      odsPrinter.printStrippedAttrOrType(getSortParams());
    }
    odsPrinter << "]";
  } else {
  }
  odsPrinter << ">";
}
 
mlir::StringAttr SortType::getIdentifier() const {
  return getImpl()->identifier;
}
 
::llvm::ArrayRef<mlir::Type> SortType::getSortParams() const {
  return getImpl()->sortParams;
}
 
} // namespace smt
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::smt::SortType)
namespace llzk {
namespace smt {

::mlir::Type SMTDialect::parseType(::mlir::DialectAsmParser &parser) const {
  ::llvm::SMLoc typeLoc = parser.getCurrentLocation();
  ::llvm::StringRef mnemonic;
  ::mlir::Type genType;
  auto parseResult = generatedTypeParser(parser, &mnemonic, genType);
  if (parseResult.has_value())
    return genType;
  
  parser.emitError(typeLoc) << "unknown  type `"
      << mnemonic << "` in dialect `" << getNamespace() << "`";
  return {};
}

void SMTDialect::printType(::mlir::Type type,
                    ::mlir::DialectAsmPrinter &printer) const {
  if (::mlir::succeeded(generatedTypePrinter(type, printer)))
    return;
  
}
} // namespace smt
} // namespace llzk
 
#endif  // GET_TYPEDEF_CLASSES