102 using ValueT = ::llvm::detail::ValueOfRange<RangeT>;
113 template <
typename LateInst = SMTInfoSetOp,
typename = std::enable_if_t<std::is_same_v<LateInst, SMTInfoSetOp>>>
122 return {std::next(odsOperands.begin(), valueRange.first),
123 std::next(odsOperands.begin(), valueRange.first + valueRange.second)};
140class SMTInfoSetOp :
public ::mlir::Op<SMTInfoSetOp, ::mlir::OpTrait::ZeroRegions, ::mlir::OpTrait::ZeroResults, ::mlir::OpTrait::ZeroSuccessors, ::mlir::OpTrait::ZeroOperands, ::mlir::OpTrait::OpInvariants, ::mlir::BytecodeOpInterface::Trait> {
145 template <
typename RangeT>
150 static ::llvm::StringRef attrNames[] = {::llvm::StringRef(
"key"), ::llvm::StringRef(
"value")};
151 return ::llvm::ArrayRef(attrNames);
155 return getAttributeNameForIndex(0);
159 return getAttributeNameForIndex(name, 0);
163 return getAttributeNameForIndex(1);
167 return getAttributeNameForIndex(name, 1);
171 return ::llvm::StringLiteral(
"smt_info.set");
180 return {std::next(getOperation()->operand_begin(), valueRange.first),
181 std::next(getOperation()->operand_begin(), valueRange.first + valueRange.second)};
190 return {std::next(getOperation()->result_begin(), valueRange.first),
191 std::next(getOperation()->result_begin(), valueRange.first + valueRange.second)};
194 static ::llvm::LogicalResult
setPropertiesFromAttr(
Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError);
197 static std::optional<mlir::Attribute>
getInherentAttr(::mlir::MLIRContext *ctx,
const Properties &prop, llvm::StringRef name);
200 static ::llvm::LogicalResult
verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError);
201 static ::llvm::LogicalResult
readProperties(::mlir::DialectBytecodeReader &reader, ::mlir::OperationState &state);
204 return ::llvm::cast<::llzk::smt_info::KeywordAttr>(getProperties().key);
207 ::llzk::smt_info::KeywordAttr
getKey();
209 return ::llvm::cast<::mlir::Attribute>(getProperties().value);
214 getProperties().key = attr;
218 getProperties().value = attr;
221 static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::llzk::smt_info::KeywordAttr key, ::mlir::Attribute value);
222 static SMTInfoSetOp create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llzk::smt_info::KeywordAttr key, ::mlir::Attribute value);
223 static SMTInfoSetOp create(::mlir::ImplicitLocOpBuilder &builder, ::llzk::smt_info::KeywordAttr key, ::mlir::Attribute value);
224 static void build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::llzk::smt_info::KeywordAttr key, ::mlir::Attribute value);
225 static SMTInfoSetOp create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::llzk::smt_info::KeywordAttr key, ::mlir::Attribute value);
226 static SMTInfoSetOp create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::llzk::smt_info::KeywordAttr key, ::mlir::Attribute value);
227 static void build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
228 static SMTInfoSetOp
create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
229 static SMTInfoSetOp
create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes = {});
230 static void build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands,
const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes = {});
231 static SMTInfoSetOp
create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands,
const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes = {});
232 static SMTInfoSetOp
create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands,
const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes = {});
233 static ::mlir::ParseResult
parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result);
234 void print(::mlir::OpAsmPrinter &p);
237 ::llvm::LogicalResult
verify();
240 ::mlir::StringAttr getAttributeNameForIndex(
unsigned index) {
241 return getAttributeNameForIndex((*this)->getName(), index);
244 static ::mlir::StringAttr getAttributeNameForIndex(::mlir::OperationName name,
unsigned index) {
245 assert(index < 2 &&
"invalid attribute index");
246 assert(name.getStringRef() ==
getOperationName() &&
"invalid operation name");
247 assert(name.isRegistered() &&
"Operation isn't registered, missing a "
248 "dependent dialect loading?");
249 return name.getAttributeNames()[index];