108 using ValueT = ::llvm::detail::ValueOfRange<RangeT>;
119 template <
typename LateInst = NonDetOp,
typename = std::enable_if_t<std::is_same_v<LateInst, NonDetOp>>>
128 return {std::next(odsOperands.begin(), valueRange.first),
129 std::next(odsOperands.begin(), valueRange.first + valueRange.second)};
146class 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::ConditionallySpeculatable::Trait, ::mlir::OpTrait::AlwaysSpeculatableImplTrait, ::mlir::OpAsmOpInterface::Trait> {
151 template <
typename RangeT>
155 using ::mlir::OpAsmOpInterface::Trait<NonDetOp>::getAsmBlockArgumentNames;
156 using ::mlir::OpAsmOpInterface::Trait<NonDetOp>::getAsmBlockNames;
157 using ::mlir::OpAsmOpInterface::Trait<NonDetOp>::getDefaultDialect;
163 return ::llvm::StringLiteral(
"llzk.nondet");
172 return {std::next(getOperation()->operand_begin(), valueRange.first),
173 std::next(getOperation()->operand_begin(), valueRange.first + valueRange.second)};
182 return {std::next(getOperation()->result_begin(), valueRange.first),
183 std::next(getOperation()->result_begin(), valueRange.first + valueRange.second)};
186 ::mlir::TypedValue<::mlir::Type>
getRes() {
187 return ::llvm::cast<::mlir::TypedValue<::mlir::Type>>(*
getODSResults(0).begin());
190 static ::llvm::LogicalResult
setPropertiesFromAttr(
Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError);
193 static std::optional<mlir::Attribute>
getInherentAttr(::mlir::MLIRContext *ctx,
const Properties &prop, llvm::StringRef name);
196 static ::llvm::LogicalResult
verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError);
197 static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type res);
198 static NonDetOp create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Type res);
199 static NonDetOp create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Type res);
200 static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes);
201 static NonDetOp create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes);
202 static NonDetOp create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes);
203 static void build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
204 static NonDetOp
create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
205 static NonDetOp
create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
206 static void build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands,
const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes = {});
207 static NonDetOp
create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands,
const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes = {});
208 static NonDetOp
create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands,
const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes = {});
213 static ::mlir::ParseResult
parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result);
214 void print(::mlir::OpAsmPrinter &_odsPrinter);