46template <
typename RangeT>
48 using ValueT = ::llvm::detail::ValueOfRange<RangeT>;
51 NonDetOpGenericAdaptor(RangeT values, ::mlir::DictionaryAttr attrs = {}, const ::mlir::EmptyProperties &properties = {}, ::mlir::RegionRange regions = {}) : Base(attrs, properties, regions), odsOperands(values) {}
53 NonDetOpGenericAdaptor(RangeT values, ::mlir::DictionaryAttr attrs, ::mlir::OpaqueProperties properties, ::mlir::RegionRange regions = {}) :
NonDetOpGenericAdaptor(values, attrs, (properties ? *properties.as<::
mlir::EmptyProperties *>() : ::
mlir::EmptyProperties{}), regions) {}
57 template <
typename LateInst = NonDetOp,
typename = std::enable_if_t<std::is_same_v<LateInst, NonDetOp>>>
66 return {std::next(odsOperands.begin(), valueRange.first),
67 std::next(odsOperands.begin(), valueRange.first + valueRange.second)};
82 ::llvm::LogicalResult
verify(::mlir::Location loc);
84class NonDetOp :
public ::mlir::Op<NonDetOp, ::mlir::OpTrait::ZeroRegions, ::mlir::OpTrait::OneResult, ::mlir::OpTrait::OneTypedResult<::mlir::Type>::Impl, ::mlir::OpTrait::ZeroSuccessors, ::mlir::OpTrait::ZeroOperands, ::mlir::OpTrait::OpInvariants, ::mlir::OpTrait::ConstantLike, ::mlir::ConditionallySpeculatable::Trait, ::mlir::OpTrait::AlwaysSpeculatableImplTrait, ::mlir::MemoryEffectOpInterface::Trait, ::mlir::OpAsmOpInterface::Trait> {
89 template <
typename RangeT>
97 return ::llvm::StringLiteral(
"llzk.nondet");
106 return {std::next(getOperation()->operand_begin(), valueRange.first),
107 std::next(getOperation()->operand_begin(), valueRange.first + valueRange.second)};
116 return {std::next(getOperation()->result_begin(), valueRange.first),
117 std::next(getOperation()->result_begin(), valueRange.first + valueRange.second)};
120 ::mlir::TypedValue<::mlir::Type>
getRes() {
121 return ::llvm::cast<::mlir::TypedValue<::mlir::Type>>(*
getODSResults(0).begin());
124 static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type res);
125 static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes);
126 static void build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
130 static ::mlir::ParseResult
parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result);
131 void print(::mlir::OpAsmPrinter &_odsPrinter);
132 void getEffects(::llvm::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects);
NonDetOpGenericAdaptor(RangeT values, ::mlir::DictionaryAttr attrs={}, const ::mlir::EmptyProperties &properties={}, ::mlir::RegionRange regions={})
::llvm::LogicalResult verify(::mlir::Location loc)
NonDetOpAdaptor(NonDetOp op)
std::pair< unsigned, unsigned > getODSOperandIndexAndLength(unsigned index)
NonDetOpGenericAdaptor(RangeT values, ::mlir::DictionaryAttr attrs={}, const ::mlir::EmptyProperties &properties={}, ::mlir::RegionRange regions={})
NonDetOpGenericAdaptor(RangeT values, LateInst op)
NonDetOpGenericAdaptor(RangeT values, ::mlir::DictionaryAttr attrs, ::mlir::OpaqueProperties properties, ::mlir::RegionRange regions={})
RangeT getODSOperands(unsigned index)
NonDetOpGenericAdaptor(RangeT values, const NonDetOpGenericAdaptorBase &base)
::mlir::Operation::operand_range getODSOperands(unsigned index)
::mlir::Operation::result_range getODSResults(unsigned index)
::mlir::TypedValue<::mlir::Type > getRes()
::llvm::LogicalResult verifyInvariantsImpl()
std::pair< unsigned, unsigned > getODSOperandIndexAndLength(unsigned index)
void print(::mlir::OpAsmPrinter &_odsPrinter)
NonDetOpGenericAdaptor< RangeT > GenericAdaptor
std::pair< unsigned, unsigned > getODSResultIndexAndLength(unsigned index)
static constexpr ::llvm::StringLiteral getOperationName()
static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type res)
::llvm::LogicalResult verifyInvariants()
::mlir::ParseResult parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result)
GenericAdaptor<::llvm::ArrayRef<::mlir::Attribute > > FoldAdaptor
void getAsmResultNames(::mlir::OpAsmSetValueNameFn setNameFn)
void getEffects(::llvm::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect > > &effects)
static ::llvm::ArrayRef<::llvm::StringRef > getAttributeNames()
::mlir::DictionaryAttr getAttributes()
::mlir::DictionaryAttr odsAttrs
NonDetOpGenericAdaptorBase(::mlir::Operation *op)
NonDetOpGenericAdaptorBase(::mlir::DictionaryAttr attrs={}, const ::mlir::EmptyProperties &properties={}, ::mlir::RegionRange regions={})
::std::optional<::mlir::OperationName > odsOpName
::mlir::RegionRange odsRegions
std::pair< unsigned, unsigned > getODSOperandIndexAndLength(unsigned index, unsigned odsOperandsSize)