SMTTypes.h.inc

Go to the documentation of this file.

/*===- TableGen'erated file -------------------------------------*- C++ -*-===*\
|*                                                                            *|
|* TypeDef Declarations                                                       *|
|*                                                                            *|
|* Automatically generated file, do not edit!                                 *|
|*                                                                            *|
\*===----------------------------------------------------------------------===*/
 
#ifdef GET_TYPEDEF_CLASSES
#undef GET_TYPEDEF_CLASSES
 
 
namespace mlir {
class AsmParser;
class AsmPrinter;
} // namespace mlir
namespace llzk {
namespace smt {
class BoolType;
class IntType;
class BitVectorType;
class ArrayType;
class SMTFuncType;
class SortType;
class BoolType : public ::mlir::Type::TypeBase<BoolType, ::mlir::Type, ::mlir::TypeStorage> {
public:
  using Base::Base;
  static constexpr ::llvm::StringLiteral name = "smt.bool";
  static constexpr ::llvm::StringLiteral dialectName = "smt";
  static constexpr ::llvm::StringLiteral getMnemonic() {
    return {"bool"};
  }
 
  static ::mlir::Type parse(::mlir::AsmParser &odsParser);
  void print(::mlir::AsmPrinter &odsPrinter) const;
};
class IntType : public ::mlir::Type::TypeBase<IntType, ::mlir::Type, ::mlir::TypeStorage> {
public:
  using Base::Base;
  static constexpr ::llvm::StringLiteral name = "smt.int";
  static constexpr ::llvm::StringLiteral dialectName = "smt";
  static constexpr ::llvm::StringLiteral getMnemonic() {
    return {"int"};
  }
 
  static ::mlir::Type parse(::mlir::AsmParser &odsParser);
  void print(::mlir::AsmPrinter &odsPrinter) const;
};
namespace detail {
struct BitVectorTypeStorage;
} // namespace detail
class BitVectorType : public ::mlir::Type::TypeBase<BitVectorType, ::mlir::Type, detail::BitVectorTypeStorage> {
public:
  using Base::Base;
  static constexpr ::llvm::StringLiteral name = "smt.bv";
  static constexpr ::llvm::StringLiteral dialectName = "smt";
  using Base::getChecked;
  static BitVectorType get(::mlir::MLIRContext *context, int64_t width);
  static BitVectorType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, int64_t width);
  static ::llvm::LogicalResult verify(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, int64_t width);
  static ::llvm::LogicalResult verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, int64_t width);
  static constexpr ::llvm::StringLiteral getMnemonic() {
    return {"bv"};
  }
 
  static ::mlir::Type parse(::mlir::AsmParser &odsParser);
  void print(::mlir::AsmPrinter &odsPrinter) const;
  int64_t getWidth() const;
};
namespace detail {
struct ArrayTypeStorage;
} // namespace detail
class ArrayType : public ::mlir::Type::TypeBase<ArrayType, ::mlir::Type, detail::ArrayTypeStorage> {
public:
  using Base::Base;
  static constexpr ::llvm::StringLiteral name = "smt.array";
  static constexpr ::llvm::StringLiteral dialectName = "smt";
  using Base::getChecked;
  static ArrayType get(::mlir::MLIRContext *context, mlir::Type domainType, mlir::Type rangeType);
  static ArrayType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, mlir::Type domainType, mlir::Type rangeType);
  static ::llvm::LogicalResult verify(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::Type domainType, mlir::Type rangeType);
  static ::llvm::LogicalResult verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::Type domainType, mlir::Type rangeType);
  static constexpr ::llvm::StringLiteral getMnemonic() {
    return {"array"};
  }
 
  static ::mlir::Type parse(::mlir::AsmParser &odsParser);
  void print(::mlir::AsmPrinter &odsPrinter) const;
  mlir::Type getDomainType() const;
  mlir::Type getRangeType() const;
};
namespace detail {
struct SMTFuncTypeStorage;
} // namespace detail
class SMTFuncType : public ::mlir::Type::TypeBase<SMTFuncType, ::mlir::Type, detail::SMTFuncTypeStorage> {
public:
  using Base::Base;
  static constexpr ::llvm::StringLiteral name = "smt.func";
  static constexpr ::llvm::StringLiteral dialectName = "smt";
  using Base::getChecked;
  static SMTFuncType get(::mlir::MLIRContext *context, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType);
  static SMTFuncType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType);
  static SMTFuncType get(llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType);
  static SMTFuncType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType);
  static SMTFuncType get(mlir::Type rangeType);
  static SMTFuncType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::Type rangeType);
  static ::llvm::LogicalResult verify(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType);
  static ::llvm::LogicalResult verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::llvm::ArrayRef<mlir::Type> domainTypes, mlir::Type rangeType);
  static constexpr ::llvm::StringLiteral getMnemonic() {
    return {"func"};
  }
 
  static ::mlir::Type parse(::mlir::AsmParser &odsParser);
  void print(::mlir::AsmPrinter &odsPrinter) const;
  ::llvm::ArrayRef<mlir::Type> getDomainTypes() const;
  mlir::Type getRangeType() const;
};
namespace detail {
struct SortTypeStorage;
} // namespace detail
class SortType : public ::mlir::Type::TypeBase<SortType, ::mlir::Type, detail::SortTypeStorage> {
public:
  using Base::Base;
  static constexpr ::llvm::StringLiteral name = "smt.sort";
  static constexpr ::llvm::StringLiteral dialectName = "smt";
  using Base::getChecked;
  static SortType get(::mlir::MLIRContext *context, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams);
  static SortType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams);
  static SortType get(::mlir::MLIRContext *context, llvm::StringRef identifier, llvm::ArrayRef<mlir::Type> sortParams);
  static SortType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, llvm::StringRef identifier, llvm::ArrayRef<mlir::Type> sortParams);
  static SortType get(::mlir::MLIRContext *context, llvm::StringRef identifier);
  static SortType getChecked(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, ::mlir::MLIRContext *context, llvm::StringRef identifier);
  static ::llvm::LogicalResult verify(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams);
  static ::llvm::LogicalResult verifyInvariants(::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError, mlir::StringAttr identifier, ::llvm::ArrayRef<mlir::Type> sortParams);
  static constexpr ::llvm::StringLiteral getMnemonic() {
    return {"sort"};
  }
 
  static ::mlir::Type parse(::mlir::AsmParser &odsParser);
  void print(::mlir::AsmPrinter &odsPrinter) const;
  mlir::StringAttr getIdentifier() const;
  ::llvm::ArrayRef<mlir::Type> getSortParams() const;
};
} // namespace smt
} // namespace llzk
MLIR_DECLARE_EXPLICIT_TYPE_ID(::llzk::smt::BoolType)
MLIR_DECLARE_EXPLICIT_TYPE_ID(::llzk::smt::IntType)
MLIR_DECLARE_EXPLICIT_TYPE_ID(::llzk::smt::BitVectorType)
MLIR_DECLARE_EXPLICIT_TYPE_ID(::llzk::smt::ArrayType)
MLIR_DECLARE_EXPLICIT_TYPE_ID(::llzk::smt::SMTFuncType)
MLIR_DECLARE_EXPLICIT_TYPE_ID(::llzk::smt::SortType)
 
#endif  // GET_TYPEDEF_CLASSES