tiny.smt.choir.dialect.SmtDialect

1/// The SMT dialect: its name, its specification, one struct per operation, and the functions that2/// build and read its types. A caller names every operation, type getter and width reader of the3/// dialect through this struct, and names the dialect by its `name` when it asks a context to load4/// it. Its 42 operation structs are the declarations that end in `Op`. The namespace re-exports it5/// as `SmtDialect`.6pub const SmtDialect = struct {7    /// The dialect's name, `smt`. A caller asks a context for the dialect by this name after8    /// registering it. Every operation name and type name of the dialect starts with `smt.`.9    /// `registry` records the dialect's loader under this name.10    pub const name = "smt";11    /// The dialect's specification: its name, its 42 operations, its three type names, and the12    /// function that reads the widths of the bit-vector and array types. `loadDialect` and the type13    /// getters load the dialect into a context from this value, and a test loads it directly. The14    /// list of operations comes from every declaration of `SmtDialect` that carries an operation15    /// specification. Loading it a second time into one context returns at once and leaves the16    /// context as it was.17    pub const spec = ir.dialects.DialectSpec{18        .name = name,19        .operations = ir.dialects.operations(@This()),20        .types = &.{21            ir.dialects.typeName(type_names.boolean),22            ir.dialects.typeName(type_names.bv),23            ir.dialects.typeName(type_names.array),24        },25        .type_interface_fallbacks = &.{26            .{ .id = interfaces.TypeParamInterface.id, .fallback = typeParamFallback },27        },28    };2930    const same_operands_and_result_type_trait = ir.dialects.trait(ir.traits.SameOperandsAndResultType);31    const same_type_operands_trait = ir.dialects.trait(ir.traits.SameTypeOperands);32    const operand0_is_bool_constraint = ir.dialects.typeConstraint.exact(0, type_names.boolean);33    const operand1_is_bool_constraint = ir.dialects.typeConstraint.exact(1, type_names.boolean);34    const result0_is_bool_constraint = ir.dialects.typeConstraint.exact(0, type_names.boolean);35    const op_specs = ir.dialects.opSpec.dialect(@This());36    const op_templates = ir.dialects.operationTemplate.dialect(@This());3738    /// The width of a bit-vector type, parsed from the decimal text the type carries. `bitVecWidth`39    /// reads a bit-vector type's width through this struct, and a caller reads the width through40    /// `bitVecWidth`. The context parses it the first time a caller asks for the type's width and41    /// keeps it for the type. The struct holds one field, `width`, the number of bits, at least 1.42    /// A type whose text is empty, fails to parse as a decimal number or is 0 gets no payload, so43    /// `bitVecWidth` returns `null` for it.44    pub const BitVecTypePayload = struct {45        width: u32,46    };4748    /// The index width and the element width of an array type, parsed from the text `index:element`49    /// the type carries. `arrayShape` returns an array type's two widths in this struct, and a50    /// caller reads the widths from it to pick the sort of an array. The context parses it the51    /// first time a caller asks for the type's widths and keeps it for the type. An array type maps52    /// bit-vectors of the index width to bit-vectors of the element width. A type whose text53    /// differs from two decimal numbers joined by one colon, or holds a 0, gets no payload, so54    /// `arrayShape` returns `null` for it.55    pub const ArrayTypePayload = struct {56        /// The width in bits of the bit-vectors that index the array, at least 1.57        /// `ArraySelectOp.create` and `ArrayStoreOp.create` require an index of this width. A58        /// caller reads it to build the array's sort.59        index_width: u32,60        /// The width in bits of the bit-vectors the array holds, at least 1. `ArraySelectOp.create`61        /// gives its result this width, and `ArrayStoreOp.create` requires a stored value of this62        /// width. A caller reads it to build the array's sort.63        element_width: u32,64    };6566    const type_param_vtable = interfaces.TypeParamInterface.VTable{67        .parse = parseTypeParams,68    };6970    /// A named variable of a given type: the operation `smt.var`, with one result and the71    /// variable's name in its `name` attribute. A checker declares each free variable of its72    /// formula, such as a parameter or an input of the program it checks, as one of these73    /// operations. The struct holds the operation in `op`, creates it with `create`, and reads it74    /// with `getResult` and `getName`.75    pub const VarOp = struct {76        /// The operation the struct holds. `create` sets it, and a caller reads it to add the77        /// operation to a block. A caller that finds an operation named `operation_name` builds the78        /// struct around it and reads the variable through the getters.79        op: *ir.Operation,8081        /// The specification of `smt.var`: its full name, its one attribute key `name`, and its82        /// side effects declared as unknown. The dialect's specification gathers this value, so83        /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it84        /// among the dialect's operations.85        pub const operation_spec = op_specs.define(.{86            .mnemonic = "var",87            .attrs = &.{attr_names.name},8889            .interfaces = &.{unknown_effects},90        });91        /// The full name of the operation, `smt.var`. Code that walks operations compares each92        /// operation's name with this constant to find the variables. `create` creates operations93        /// under this name.94        pub const operation_name = operation_spec.name;9596        /// Creates an `smt.var` operation named `symbol`, with one result of type `result_type` and97        /// the source location `loc`, and returns the struct holding it. A checker calls it once98        /// for each parameter or input of the program it checks, with the type of that parameter or99        /// input. The context keeps its own copy of `symbol`. Neither the call nor100        /// `ir.verifyOperation` checks `result_type`, and a variable may have any type of the101        /// context, the dialect's three types included. The new operation belongs to no block until102        /// the caller adds `op` to one. The call returns the errors of creating the operation and103        /// its attribute in `ctx`.104        pub fn create(ctx: *ir.Context, loc: ir.Location, symbol: []const u8, result_type: ir.Type) !VarOp {105            var builder = ir.OperationBuilder.init(ctx);106            var state = ir.Operation.State.init(operation_name, loc);107            state.addTypes(&.{result_type});108            const op = try builder.create(state);109            try op.setAttr(attr_names.name, try ctx.getStringAttr(symbol));110            return .{ .op = op };111        }112113        /// Returns the operation's one result, the variable's value. A caller passes the variable's114        /// value to the operations that use the variable.115        pub fn getResult(self: *const VarOp) *ir.Value {116            return self.op.getResult(0).?;117        }118119        /// Returns the variable's name from its `name` attribute. Code that reads a formula back120        /// turns each variable into a named constant of the solver under this name. The slice121        /// points into the context's copy of the name. The call returns `null` when the operation122        /// lacks a string attribute under `name`.123        pub fn getName(self: VarOp) ?[]const u8 {124            const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.name) orelse return null;125            return attr.getValue();126        }127    };128129    /// A Boolean constant: the operation `smt.bool.const`, with one Boolean result and the value in130    /// its `value` attribute. A checker states a fixed truth value, for example an obligation that131    /// holds for every input, as one of these operations. The struct holds the operation in `op`,132    /// creates it with `create`, and reads it with `getResult` and `getValue`.133    pub const BoolConstOp = struct {134        /// The operation the struct holds. `create` sets it, and a caller reads it to inspect the135        /// operation or add it to a block. A caller that finds an operation named `operation_name`136        /// builds the struct around it and reads the constant through `getValue`.137        op: *ir.Operation,138139        /// The specification of `smt.bool.const`: its full name, its one attribute key `value`, and140        /// its side effects declared as unknown. The dialect's specification gathers this value, so141        /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it142        /// among the dialect's operations.143        pub const operation_spec = op_specs.define(.{144            .mnemonic = "bool.const",145            .attrs = &.{attr_names.value},146147            .interfaces = &.{unknown_effects},148        });149        /// The full name of the operation, `smt.bool.const`. Code that walks operations compares150        /// each operation's name with this constant to find the Boolean constants. `create` creates151        /// operations under this name.152        pub const operation_name = operation_spec.name;153154        /// Creates an `smt.bool.const` operation holding `value`, with one result of the Boolean155        /// type and the source location `loc`, and returns the struct holding it. A checker creates156        /// the constant `true` or `false` for an obligation whose answer it knows while it builds157        /// the formula. The call builds the Boolean type first, which loads the dialect into `ctx`158        /// when unloaded. The new operation belongs to no block until the caller adds `op` to one.159        /// The call returns the errors of `getBoolType` and of creating the operation and its160        /// attribute in `ctx`.161        pub fn create(ctx: *ir.Context, loc: ir.Location, value: bool) !BoolConstOp {162            var builder = ir.OperationBuilder.init(ctx);163            var state = ir.Operation.State.init(operation_name, loc);164            state.addTypes(&.{try getBoolType(ctx)});165            const op = try builder.create(state);166            try op.setAttr(attr_names.value, try ctx.getBoolAttr(value));167            return .{ .op = op };168        }169170        /// Returns the operation's one result, the constant's value. A caller passes the constant's171        /// value to the operations that use it.172        pub fn getResult(self: *const BoolConstOp) *ir.Value {173            return self.op.getResult(0).?;174        }175176        /// Returns the constant from its `value` attribute. Code that reads a formula back turns177        /// each Boolean constant into the solver's `true` or `false`. The call returns `null` when178        /// the operation lacks a Boolean attribute under `value`.179        pub fn getValue(self: BoolConstOp) ?bool {180            const attr = self.op.getAttrAs(ir.Attribute.BoolAttr, attr_names.value) orelse return null;181            return attr.getValue();182        }183    };184185    /// A bit-vector constant: the operation `smt.bv.const`, with one result of a bit-vector type186    /// and the value in its `value` attribute as decimal text. A checker states a fixed bit-vector,187    /// such as a literal of the program it checks or a limit to compare against, as one of these188    /// operations. The struct holds the operation in `op`, creates it with `create`, and reads it189    /// with `getResult` and `getValue`. The width lives in the result's type, and the attribute190    /// holds only the value.191    pub const BitVecConstOp = struct {192        /// The operation the struct holds. `create` sets it, and a caller reads it to add the193        /// operation to a block. A caller that finds an operation named `operation_name` builds the194        /// struct around it and reads the constant through `getValue`.195        op: *ir.Operation,196197        /// The specification of `smt.bv.const`: its full name, its one attribute key `value`, and198        /// its side effects declared as unknown. The dialect's specification gathers this value, so199        /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it200        /// among the dialect's operations.201        pub const operation_spec = op_specs.define(.{202            .mnemonic = "bv.const",203            .attrs = &.{attr_names.value},204205            .interfaces = &.{unknown_effects},206        });207        /// The full name of the operation, `smt.bv.const`. Code that walks operations compares each208        /// operation's name with this constant to find the bit-vector constants. `create` creates209        /// operations under this name.210        pub const operation_name = operation_spec.name;211212        /// Creates an `smt.bv.const` operation holding `value`, with one result of the bit-vector213        /// type of width `width` and the source location `loc`, and returns the struct holding it.214        /// A checker creates one constant for each literal of the program it checks, and for limits215        /// such as the width of a shifted value. The call writes `value` as decimal text into the216        /// `value` attribute. The call builds the bit-vector type first, which loads the dialect217        /// into `ctx` when unloaded. The call checks neither that `value` fits in `width` bits nor218        /// that `width` is above 0. The new operation belongs to no block until the caller adds219        /// `op` to one. The call returns the errors of building the type and of creating the220        /// operation and its attribute in `ctx`.221        pub fn create(ctx: *ir.Context, loc: ir.Location, width: u32, value: u128) !BitVecConstOp {222            var builder = ir.OperationBuilder.init(ctx);223            var state = ir.Operation.State.init(operation_name, loc);224            state.addTypes(&.{try getBitVecType(ctx, width)});225            const op = try builder.create(state);226            var buf: [40]u8 = undefined;227            try op.setAttr(attr_names.value, try ctx.getStringAttr(try std.fmt.bufPrint(&buf, "{d}", .{value})));228            return .{ .op = op };229        }230231        /// Returns the operation's one result, the constant's value. A caller passes the constant's232        /// value to the operations that use it.233        pub fn getResult(self: *const BitVecConstOp) *ir.Value {234            return self.op.getResult(0).?;235        }236237        /// Returns the constant, parsed from the decimal text of its `value` attribute. Code that238        /// reads a formula back turns each bit-vector constant into a solver constant of the239        /// result's width. The call returns `null` when the operation lacks a string attribute240        /// under `value` or its text fails to parse as a decimal number that fits in a `u128`.241        pub fn getValue(self: BitVecConstOp) ?u128 {242            const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.value) orelse return null;243            return std.fmt.parseInt(u128, attr.getValue(), 10) catch null;244        }245    };246247    /// The application of a function to the operation's operands: the operation `smt.apply`, with248    /// one result and the function's name in its `name` attribute. A checker states facts about a249    /// function it leaves undefined by applying the function by name to its arguments. The dialect250    /// declares no function: the operand types are the argument types, and the result's type is the251    /// function's result type. The struct holds the operation in `op`, creates it with `create`,252    /// and reads it with `getResult` and `getName`.253    pub const ApplyOp = struct {254        /// The operation the struct holds. `create` sets it, and a caller reads it to add the255        /// operation to a block. A caller that finds an operation named `operation_name` builds the256        /// struct around it and reads the function's name through `getName`.257        op: *ir.Operation,258259        /// The specification of `smt.apply`: its full name, its one attribute key `name`, and its260        /// side effects declared as unknown. The dialect's specification gathers this value, so261        /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it262        /// among the dialect's operations.263        pub const operation_spec = op_specs.define(.{264            .mnemonic = "apply",265            .attrs = &.{attr_names.name},266267            .interfaces = &.{unknown_effects},268        });269        /// The full name of the operation, `smt.apply`. Code that walks operations compares each270        /// operation's name with this constant to find the function applications. `create` creates271        /// operations under this name.272        pub const operation_name = operation_spec.name;273274        /// Creates an `smt.apply` operation that applies the function `function_name` to275        /// `operands`, with one result of type `result_type` and the source location `loc`, and276        /// returns the struct holding it. A checker applies a function it leaves undefined to the277        /// values it passes as arguments. The operation copies `operands`, and the context keeps278        /// its own copy of `function_name`. The call checks no types, and `operands` may be empty.279        /// The new operation belongs to no block until the caller adds `op` to one. The call280        /// returns the errors of creating the operation and its attribute in `ctx`.281        pub fn create(ctx: *ir.Context, loc: ir.Location, function_name: []const u8, operands: []const *ir.Value, result_type: ir.Type) !ApplyOp {282            var builder = ir.OperationBuilder.init(ctx);283            var state = ir.Operation.State.init(operation_name, loc);284            state.addOperands(operands);285            state.addTypes(&.{result_type});286            const op = try builder.create(state);287            try op.setAttr(attr_names.name, try ctx.getStringAttr(function_name));288            return .{ .op = op };289        }290291        /// Returns the operation's one result, the value of the application. A caller passes the292        /// application's value to the operations that use it.293        pub fn getResult(self: *const ApplyOp) *ir.Value {294            return self.op.getResult(0).?;295        }296297        /// Returns the name of the applied function from the `name` attribute. Code that reads a298        /// formula back declares an uninterpreted function under this name. The slice points into299        /// the context's copy of the name. The call returns `null` when the operation lacks a300        /// string attribute under `name`.301        pub fn getName(self: ApplyOp) ?[]const u8 {302            const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.name) orelse return null;303            return attr.getValue();304        }305    };306307    /// A Boolean formula that must hold: the operation `smt.assert`, with one Boolean operand, no308    /// result, and an optional name and group label in its `name` and `group` attributes. A checker309    /// states each property it must check as one assertion, names it after the check, and gives it310    /// a group label so that a report can sort the answers. The struct holds the operation in `op`,311    /// creates it with `create`, `createNamed` or `createGrouped`, and reads it with312    /// `getAssertion`, `getName` and `getGroup`. A caller keeps a list of the assertion operations,313    /// and code that reads the formula back walks that list.314    pub const AssertOp = struct {315        /// The operation the struct holds. `create` sets it, and a caller appends it to its list of316        /// assertions. A caller that reads its list back builds the struct around each operation317        /// named `operation_name`.318        op: *ir.Operation,319320        /// The specification of `smt.assert`: its full name, its attribute keys `name` and `group`,321        /// its side effects declared as unknown, and the rule that its operand is Boolean.322        /// `SmtDialect.spec` lists it among the dialect's operations, so loading the dialect323        /// registers the operation with the context, and `ir.verifyOperation` checks the operand324        /// rule.325        pub const operation_spec = op_specs.define(.{326            .mnemonic = "assert",327            .attrs = &.{ attr_names.name, attr_names.group },328329            .interfaces = &.{unknown_effects},330            .operand_types = &.{operand0_is_bool_constraint},331        });332        /// The full name of the operation, `smt.assert`. Code that reads a list of assertions back333        /// checks each operation's name against this constant before it builds the struct. `create`334        /// creates operations under this name. A caller refuses an operation of another name in its335        /// list of assertions.336        pub const operation_name = operation_spec.name;337338        /// Creates an `smt.assert` operation on `assertion` at the source location `loc`, leaves339        /// its name and group label unset, and returns the struct holding it. A caller asserts a340        /// background fact that its reports leave unnamed, such as an equation that fixes a341        /// variable to a witness value. The call checks no type, and `ir.verifyOperation` checks342        /// that `assertion` is Boolean. The new operation belongs to no block until the caller adds343        /// `op` to one. The call returns the errors of creating the operation in `ctx`.344        pub fn create(ctx: *ir.Context, loc: ir.Location, assertion: *ir.Value) !AssertOp {345            var builder = ir.OperationBuilder.init(ctx);346            var state = ir.Operation.State.init(operation_name, loc);347            state.addOperands(&.{assertion});348            const op = try builder.create(state);349            return .{ .op = op };350        }351352        /// Creates an `smt.assert` operation on `assertion` with the name `assertion_name`, and353        /// leaves its group label unset. A caller asserts a formula under a name, so a report can354        /// say which assertion an answer concerns. The call calls `create` and then sets the `name`355        /// attribute. The context keeps its own copy of `assertion_name`. The call returns the356        /// errors of `create` and of setting the attribute in `ctx`.357        pub fn createNamed(ctx: *ir.Context, loc: ir.Location, assertion_name: []const u8, assertion: *ir.Value) !AssertOp {358            const op = try create(ctx, loc, assertion);359            try op.op.setAttr(attr_names.name, try ctx.getStringAttr(assertion_name));360            return op;361        }362363        /// Creates an `smt.assert` operation on `assertion` with the name `assertion_name` and the364        /// group label `group`. A checker asserts each property under a name and a group label such365        /// as `bounds` or `overflow`, so a report can sort the answers by kind. The call calls366        /// `createNamed` and then sets the `group` attribute. The context keeps its own copies of367        /// `assertion_name` and `group`. The call returns the errors of `createNamed` and of368        /// setting the attribute in `ctx`.369        pub fn createGrouped(ctx: *ir.Context, loc: ir.Location, assertion_name: []const u8, group: []const u8, assertion: *ir.Value) !AssertOp {370            const op = try createNamed(ctx, loc, assertion_name, assertion);371            try op.op.setAttr(attr_names.group, try ctx.getStringAttr(group));372            return op;373        }374375        /// Returns the operation's one operand, the asserted formula, so code that reads the376        /// assertions back turns each asserted formula into a solver term. On an operation with no377        /// operand, the call panics in Debug and ReleaseSafe builds, and its behavior is undefined378        /// in ReleaseFast and ReleaseSmall builds.379        pub fn getAssertion(self: AssertOp) *ir.Value {380            return self.op.getOperand(0).?;381        }382383        /// Returns the assertion's name from its `name` attribute, so code that reports an answer384        /// names the assertion it concerns. The call returns `null` whenever the operation lacks a385        /// string attribute under `name`, such as for an assertion made by `create`.386        pub fn getName(self: AssertOp) ?[]const u8 {387            const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.name) orelse return null;388            return attr.getValue();389        }390391        /// Returns the assertion's group label from its `group` attribute, so code that reports392        /// answers sorts them by this label. The call returns `null` whenever the operation lacks a393        /// string attribute under `group`, such as for an assertion made by `create` or394        /// `createNamed`.395        pub fn getGroup(self: AssertOp) ?[]const u8 {396            const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.group) orelse return null;397            return attr.getValue();398        }399    };400401    /// The negation of a Boolean formula, as the operation `smt.not`. A checker negates a formula,402    /// for example to turn a condition that must hold into a search for an input that breaks it.403    /// `create(ctx, loc, input)` creates the operation with one result of the Boolean type.404    /// `getResult` returns the result, and `getInput` returns the operand. `operation_name` holds405    /// `smt.not`, and the struct holds the operation in `op`. `create` checks no type, and406    /// `ir.verifyOperation` checks the rule the dialect registered: the operand and the result are407    /// Boolean. `create` returns the errors of building the Boolean type and of creating the408    /// operation in `ctx`.409    pub const NotOp: type = op_templates.unaryFixedResult(410        "not",411        boolUnaryOptions(.{}),412        getBoolType,413    );414415    /// The conjunction of two Boolean formulas, as the operation `smt.and`. A checker joins two416    /// conditions that must both hold. `create(ctx, loc, lhs, rhs)` creates the operation with one417    /// result of the Boolean type. `getResult` returns the result, and `getLhs` and `getRhs` return418    /// the operands. `operation_name` holds `smt.and`, and the struct holds the operation in `op`.419    /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:420    /// both operands and the result are Boolean. The context records the operation as commutative.421    /// `create` returns the errors of building the Boolean type and of creating the operation in422    /// `ctx`.423    pub const AndOp: type = op_templates.binaryFixedResult(424        "and",425        boolBinaryOptions(commutative_op_traits),426        getBoolType,427    );428429    /// The disjunction of two Boolean formulas, as the operation `smt.or`. A checker joins two430    /// conditions of which one must hold. `create(ctx, loc, lhs, rhs)` creates the operation with431    /// one result of the Boolean type. `getResult` returns the result, and `getLhs` and `getRhs`432    /// return the operands. `operation_name` holds `smt.or`, and the struct holds the operation in433    /// `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect434    /// registered: both operands and the result are Boolean. The context records the operation as435    /// commutative. `create` returns the errors of building the Boolean type and of creating the436    /// operation in `ctx`.437    pub const OrOp: type = op_templates.binaryFixedResult(438        "or",439        boolBinaryOptions(commutative_op_traits),440        getBoolType,441    );442443    /// The implication from the first Boolean formula to the second, as the operation444    /// `smt.implies`. A checker states that one condition implies another, for example that a445    /// precondition implies a bound. `create(ctx, loc, lhs, rhs)` creates the operation with one446    /// result of the Boolean type. `getResult` returns the result, and `getLhs` and `getRhs` return447    /// the operands. `operation_name` holds `smt.implies`, and the struct holds the operation in448    /// `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect449    /// registered: both operands and the result are Boolean. `create` returns the errors of450    /// building the Boolean type and of creating the operation in `ctx`.451    pub const ImpliesOp: type = op_templates.binaryFixedResult(452        "implies",453        boolBinaryOptions(.{}),454        getBoolType,455    );456457    /// The equality of two values of one type, as the operation `smt.eq`. A checker states that two458    /// values are equal, for example that a variable holds a given constant or that a result is459    /// zero. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean460    /// type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.461    /// `operation_name` holds `smt.eq`, and the struct holds the operation in `op`. The operands462    /// may be Boolean values, bit-vectors or arrays. `create` checks no types, and463    /// `ir.verifyOperation` checks the rule the dialect registered: the two operands share one type464    /// and the result is Boolean. The context records the operation as commutative. `create`465    /// returns the errors of building the Boolean type and of creating the operation in `ctx`.466    pub const EqOp: type = op_templates.binaryFixedResult(467        "eq",468        sameOperandBoolResultOptions(commutative_op_traits),469        getBoolType,470    );471472    /// The element of an array at an index, as the operation `smt.array.select`, with the array and473    /// the index as operands and one result of the element type. A checker reads a memory modeled474    /// as an array at an index. The struct holds the operation in `op`, creates it with `create`,475    /// and returns the result with `getResult`.476    pub const ArraySelectOp = struct {477        op: *ir.Operation,478479        /// The specification of `smt.array.select`: its full name and its side effects declared as480        /// unknown. `SmtDialect.spec` lists it among the dialect's operations, so loading the481        /// dialect registers the operation with the context. The specification registers no type482        /// rule, so `create` alone checks the operand types.483        pub const operation_spec = op_specs.define(.{484            .mnemonic = "array.select",485486            .interfaces = &.{unknown_effects},487        });488        /// The full name of the operation, `smt.array.select`. Code that walks operations compares489        /// each operation's name with this constant to find the array reads. `create` creates490        /// operations under this name.491        pub const operation_name = operation_spec.name;492493        /// Creates an `smt.array.select` operation that reads `array` at `index` at the source494        /// location `loc`, and returns the struct holding it. A checker reads an element of a495        /// modeled memory and gets a value of the element's width. The result is a bit-vector of496        /// the array's element width. The call returns `error.UnsupportedArrayType` when497        /// `arrayShape` returns `null` for the type of `array`, `error.UnsupportedBitVectorType`498        /// when `bitVecWidth` returns `null` for the type of `index`, and499        /// `error.InvalidArrayIndexType` when the index width differs from the array's index width.500        /// The new operation belongs to no block until the caller adds `op` to one. The call also501        /// returns the errors of building the element type and of creating the operation in `ctx`.502        pub fn create(ctx: *ir.Context, loc: ir.Location, array: *ir.Value, index: *ir.Value) !ArraySelectOp {503            const shape = arrayShape(ctx, array.type) orelse return error.UnsupportedArrayType;504            const index_width = bitVecWidth(ctx, index.type) orelse return error.UnsupportedBitVectorType;505            if (index_width != shape.index_width) return error.InvalidArrayIndexType;506            return .{ .op = try binary(ctx, loc, operation_name, array, index, try getBitVecType(ctx, shape.element_width)) };507        }508509        /// Returns the operation's one result, the element read, so a caller passes it to the510        /// operations that use it.511        pub fn getResult(self: *const ArraySelectOp) *ir.Value {512            return self.op.getResult(0).?;513        }514    };515516    /// The array equal to a given array except that one index holds a new value, as the operation517    /// `smt.array.store`, with the array, the index and the value as operands and one result of the518    /// array's type. A checker writes an element into a memory modeled as an array and gets the new519    /// array. The struct holds the operation in `op`, creates it with `create`, and returns the520    /// result with `getResult`.521    pub const ArrayStoreOp = struct {522        op: *ir.Operation,523524        /// The specification of `smt.array.store`: its full name and its side effects declared as525        /// unknown. `SmtDialect.spec` lists it among the dialect's operations, so loading the526        /// dialect registers the operation with the context. The specification registers no type527        /// rule, so `create` alone checks the operand types.528        pub const operation_spec = op_specs.define(.{529            .mnemonic = "array.store",530531            .interfaces = &.{unknown_effects},532        });533        /// The full name of the operation, `smt.array.store`. Code that walks operations compares534        /// each operation's name with this constant to find the array writes. `create` creates535        /// operations under this name.536        pub const operation_name = operation_spec.name;537538        /// Creates an `smt.array.store` operation that writes `value` into `array` at `index` at539        /// the source location `loc`, and returns the struct holding it. A checker records a write540        /// into a modeled memory as a new array value. The result has the type of `array`. The call541        /// returns `error.UnsupportedArrayType` when `arrayShape` returns `null` for the type of542        /// `array`, and `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the543        /// type of `index` or of `value`. The call returns `error.InvalidArrayIndexType` when the544        /// index width differs from the array's index width, and `error.InvalidArrayElementType`545        /// when the value's width differs from the array's element width. The new operation belongs546        /// to no block until the caller adds `op` to one. The call also returns the errors of547        /// creating the operation in `ctx`.548        pub fn create(ctx: *ir.Context, loc: ir.Location, array: *ir.Value, index: *ir.Value, value: *ir.Value) !ArrayStoreOp {549            const shape = arrayShape(ctx, array.type) orelse return error.UnsupportedArrayType;550            const index_width = bitVecWidth(ctx, index.type) orelse return error.UnsupportedBitVectorType;551            const element_width = bitVecWidth(ctx, value.type) orelse return error.UnsupportedBitVectorType;552            if (index_width != shape.index_width) return error.InvalidArrayIndexType;553            if (element_width != shape.element_width) return error.InvalidArrayElementType;554            var builder = ir.OperationBuilder.init(ctx);555            var state = ir.Operation.State.init(operation_name, loc);556            state.addOperands(&.{ array, index, value });557            state.addTypes(&.{array.type});558            const op = try builder.create(state);559            return .{ .op = op };560        }561562        /// Returns the operation's one result, the array after the write, so a caller passes it to563        /// the operations that read or write it next.564        pub fn getResult(self: *const ArrayStoreOp) *ir.Value {565            return self.op.getResult(0).?;566        }567    };568569    /// The sum of two bit-vectors of one width, modulo 2 to the power of the width, as the570    /// operation `smt.bvadd`. A checker lowers a program's addition into this operation.571    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.572    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.573    /// `operation_name` holds `smt.bvadd`, and the struct holds the operation in `op`. `create`574    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both575    /// operands and the result share one type. The context records the operation as commutative.576    /// `create` returns the errors of creating the operation in `ctx`.577    pub const BvAddOp: type = op_templates.binarySameType(578        "bvadd",579        sameOperandsResultOptions(commutative_op_traits),580    );581582    /// The difference of two bit-vectors of one width, the first minus the second, modulo 2 to the583    /// power of the width, as the operation `smt.bvsub`. A checker lowers a program's subtraction584    /// into this operation. `create(ctx, loc, lhs, rhs)` creates the operation with one result of585    /// the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the586    /// operands. `operation_name` holds `smt.bvsub`, and the struct holds the operation in `op`.587    /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:588    /// both operands and the result share one type. `create` returns the errors of creating the589    /// operation in `ctx`.590    pub const BvSubOp: type = op_templates.binarySameType("bvsub", sameOperandsResultOptions(.{}));591592    /// The product of two bit-vectors of one width, modulo 2 to the power of the width, as the593    /// operation `smt.bvmul`. A checker lowers a program's multiplication into this operation.594    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.595    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.596    /// `operation_name` holds `smt.bvmul`, and the struct holds the operation in `op`. `create`597    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both598    /// operands and the result share one type. The context records the operation as commutative.599    /// `create` returns the errors of creating the operation in `ctx`.600    pub const BvMulOp: type = op_templates.binarySameType(601        "bvmul",602        sameOperandsResultOptions(commutative_op_traits),603    );604605    /// The bitwise complement of a bit-vector, as the operation `smt.bvnot`. A checker complements606    /// every bit of a bit-vector. `create(ctx, loc, input)` creates the operation with one result607    /// of the type of `input`. `getResult` returns the result, and `getInput` returns the operand.608    /// `operation_name` holds `smt.bvnot`, and the struct holds the operation in `op`. `create`609    /// checks no type, and `ir.verifyOperation` checks the rule the dialect registered: the operand610    /// and the result share one type. `create` returns the errors of creating the operation in611    /// `ctx`.612    pub const BvNotOp: type = op_templates.unarySameType("bvnot", sameOperandsResultOptions(.{}));613614    /// The bitwise and of two bit-vectors of one width, as the operation `smt.bvand`. A checker615    /// masks the bits of a bit-vector. `create(ctx, loc, lhs, rhs)` creates the operation with one616    /// result of the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs`617    /// return the operands. `operation_name` holds `smt.bvand`, and the struct holds the operation618    /// in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect619    /// registered: both operands and the result share one type. The context records the operation620    /// as commutative. `create` returns the errors of creating the operation in `ctx`.621    pub const BvAndOp: type = op_templates.binarySameType(622        "bvand",623        sameOperandsResultOptions(commutative_op_traits),624    );625626    /// The bitwise or of two bit-vectors of one width, as the operation `smt.bvor`. A checker sets627    /// bits of a bit-vector. `create(ctx, loc, lhs, rhs)` creates the operation with one result of628    /// the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the629    /// operands. `operation_name` holds `smt.bvor`, and the struct holds the operation in `op`.630    /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:631    /// both operands and the result share one type. The context records the operation as632    /// commutative. `create` returns the errors of creating the operation in `ctx`.633    pub const BvOrOp: type = op_templates.binarySameType(634        "bvor",635        sameOperandsResultOptions(commutative_op_traits),636    );637638    /// The bitwise exclusive or of two bit-vectors of one width, as the operation `smt.bvxor`. A639    /// checker flips bits of a bit-vector. `create(ctx, loc, lhs, rhs)` creates the operation with640    /// one result of the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs`641    /// return the operands. `operation_name` holds `smt.bvxor`, and the struct holds the operation642    /// in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect643    /// registered: both operands and the result share one type. The context records the operation644    /// as commutative. `create` returns the errors of creating the operation in `ctx`.645    pub const BvXorOp: type = op_templates.binarySameType(646        "bvxor",647        sameOperandsResultOptions(commutative_op_traits),648    );649650    /// The first bit-vector shifted toward its most significant bit by the value of the second, as651    /// the operation `smt.bvshl`. A checker lowers a program's left shift into this operation. The652    /// shift amount is a bit-vector of the shifted value's width. `create(ctx, loc, lhs, rhs)`653    /// creates the operation with one result of the type of `lhs`. `getResult` returns the result,654    /// and `getLhs` and `getRhs` return the operands. `operation_name` holds `smt.bvshl`, and the655    /// struct holds the operation in `op`. `create` checks no types, and `ir.verifyOperation`656    /// checks the rule the dialect registered: both operands and the result share one type.657    /// `create` returns the errors of creating the operation in `ctx`.658    pub const BvShlOp: type = op_templates.binarySameType("bvshl", sameOperandsResultOptions(.{}));659660    /// The first bit-vector shifted toward its least significant bit by the value of the second,661    /// with zeros shifted in, as the operation `smt.bvlshr`. A checker lowers a program's unsigned662    /// right shift into this operation. The shift amount is a bit-vector of the shifted value's663    /// width. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of664    /// `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.665    /// `operation_name` holds `smt.bvlshr`, and the struct holds the operation in `op`. `create`666    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both667    /// operands and the result share one type. `create` returns the errors of creating the668    /// operation in `ctx`.669    pub const BvLshrOp: type = op_templates.binarySameType(670        "bvlshr",671        sameOperandsResultOptions(.{}),672    );673674    /// The first bit-vector shifted toward its least significant bit by the value of the second,675    /// with copies of its sign bit shifted in, as the operation `smt.bvashr`. A checker lowers a676    /// program's signed right shift into this operation. The shift amount is a bit-vector of the677    /// shifted value's width. `create(ctx, loc, lhs, rhs)` creates the operation with one result of678    /// the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the679    /// operands. `operation_name` holds `smt.bvashr`, and the struct holds the operation in `op`.680    /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:681    /// both operands and the result share one type. `create` returns the errors of creating the682    /// operation in `ctx`.683    pub const BvAshrOp: type = op_templates.binarySameType(684        "bvashr",685        sameOperandsResultOptions(.{}),686    );687688    /// The rotation of a bit-vector toward its most significant bit by a fixed number of positions,689    /// as the operation `smt.bvrotl`, with the number of positions in its `amount` attribute, for a690    /// checker that rotates a bit-vector left. The result has the operand's type. The struct holds691    /// the operation in `op`, creates it with `create`, and reads it with `getResult` and692    /// `getAmount`.693    pub const BvRotlOp = struct {694        /// The operation the struct holds. `create` sets it, and a caller reads it to add the695        /// operation to a block. A caller that finds an operation named `operation_name` builds the696        /// struct around it and reads the rotation amount through `getAmount`.697        op: *ir.Operation,698699        /// The specification of `smt.bvrotl`: its full name, its one attribute key `amount`, its700        /// side effects declared as unknown, and the rule that the operand and the result share one701        /// type. `SmtDialect.spec` lists it among the dialect's operations, so loading the dialect702        /// registers the operation with the context, and `ir.verifyOperation` checks the type rule.703        pub const operation_spec = op_specs.define(.{704            .mnemonic = "bvrotl",705            .attrs = &.{attr_names.amount},706707            .interfaces = &.{unknown_effects},708            .dynamic_traits = &.{same_operands_and_result_type_trait},709        });710        /// The full name of the operation, `smt.bvrotl`, so code that walks operations can compare711        /// each operation's name with this constant to find the left rotations. `create` creates712        /// operations under this name.713        pub const operation_name = operation_spec.name;714715        /// Creates an `smt.bvrotl` operation that rotates `operand` by `amount` positions at the716        /// source location `loc`, and returns the struct holding it, so a checker can rotate a717        /// value left by the number of positions it knows when it builds the formula. The call718        /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type719        /// of `operand`. The call accepts an `amount` at or above the operand's width. The new720        /// operation belongs to no block until the caller adds `op` to one. The call also returns721        /// the errors of creating the operation and its attribute in `ctx`.722        pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, amount: u32) !BvRotlOp {723            return .{ .op = try rotate(ctx, loc, operation_name, operand, amount) };724        }725726        /// Returns the operation's one result, the rotated value, so a caller can pass it to the727        /// operations that use it.728        pub fn getResult(self: *const BvRotlOp) *ir.Value {729            return self.op.getResult(0).?;730        }731732        /// Returns the rotation amount from the `amount` attribute, so code that reads a formula733        /// back can build the solver's rotation term. The call returns `null` when the operation734        /// lacks an integer attribute under `amount` or its value lies outside the range of a735        /// `u32`.736        pub fn getAmount(self: BvRotlOp) ?u32 {737            return getU32Attr(self.op, attr_names.amount);738        }739    };740741    /// The rotation of a bit-vector toward its least significant bit by a fixed number of742    /// positions, as the operation `smt.bvrotr`, with the number of positions in its `amount`743    /// attribute, for a checker that rotates a bit-vector right. The result has the operand's type.744    /// The struct holds the operation in `op`, creates it with `create`, and reads it with745    /// `getResult` and `getAmount`.746    pub const BvRotrOp = struct {747        /// The operation the struct holds. `create` sets it, and a caller reads it to add the748        /// operation to a block. A caller that finds an operation named `operation_name` builds the749        /// struct around it and reads the rotation amount through `getAmount`.750        op: *ir.Operation,751752        /// The specification of `smt.bvrotr`: its full name, its one attribute key `amount`, its753        /// side effects declared as unknown, and the rule that the operand and the result share one754        /// type. `SmtDialect.spec` lists it among the dialect's operations, so loading the dialect755        /// registers the operation with the context, and `ir.verifyOperation` checks the type rule.756        pub const operation_spec = op_specs.define(.{757            .mnemonic = "bvrotr",758            .attrs = &.{attr_names.amount},759760            .interfaces = &.{unknown_effects},761            .dynamic_traits = &.{same_operands_and_result_type_trait},762        });763        /// The full name of the operation, `smt.bvrotr`, so code that walks operations can compare764        /// each operation's name with this constant to find the right rotations. `create` creates765        /// operations under this name.766        pub const operation_name = operation_spec.name;767768        /// Creates an `smt.bvrotr` operation that rotates `operand` by `amount` positions at the769        /// source location `loc`, and returns the struct holding it, so a checker can rotate a770        /// value right by the number of positions it knows when it builds the formula. The call771        /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type772        /// of `operand`. The call accepts an `amount` at or above the operand's width. The new773        /// operation belongs to no block until the caller adds `op` to one. The call also returns774        /// the errors of creating the operation and its attribute in `ctx`.775        pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, amount: u32) !BvRotrOp {776            return .{ .op = try rotate(ctx, loc, operation_name, operand, amount) };777        }778779        /// Returns the operation's one result, the rotated value, so a caller can pass it to the780        /// operations that use it.781        pub fn getResult(self: *const BvRotrOp) *ir.Value {782            return self.op.getResult(0).?;783        }784785        /// Returns the rotation amount from the `amount` attribute, so code that reads a formula786        /// back can build the solver's rotation term. The call returns `null` when the operation787        /// lacks an integer attribute under `amount` or its value lies outside the range of a788        /// `u32`.789        pub fn getAmount(self: BvRotrOp) ?u32 {790            return getU32Attr(self.op, attr_names.amount);791        }792    };793794    /// The unsigned quotient of the first bit-vector by the second, as the operation `smt.bvudiv`,795    /// for a checker lowering a program's unsigned division into this operation.796    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.797    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.798    /// `operation_name` holds `smt.bvudiv`, and the struct holds the operation in `op`. `create`799    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both800    /// operands and the result share one type. `create` returns the errors of creating the801    /// operation in `ctx`.802    pub const BvUdivOp: type = op_templates.binarySameType(803        "bvudiv",804        sameOperandsResultOptions(.{}),805    );806807    /// The unsigned remainder of the first bit-vector by the second, as the operation `smt.bvurem`,808    /// for a checker taking the unsigned remainder of a program's division.809    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.810    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.811    /// `operation_name` holds `smt.bvurem`, and the struct holds the operation in `op`. `create`812    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both813    /// operands and the result share one type. `create` returns the errors of creating the814    /// operation in `ctx`.815    pub const BvUremOp: type = op_templates.binarySameType(816        "bvurem",817        sameOperandsResultOptions(.{}),818    );819820    /// The two's-complement quotient of the first bit-vector by the second, rounded toward zero, as821    /// the operation `smt.bvsdiv`, for a checker lowering a program's signed division into this822    /// operation. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of823    /// `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.824    /// `operation_name` holds `smt.bvsdiv`, and the struct holds the operation in `op`. `create`825    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both826    /// operands and the result share one type. `create` returns the errors of creating the827    /// operation in `ctx`.828    pub const BvSdivOp: type = op_templates.binarySameType(829        "bvsdiv",830        sameOperandsResultOptions(.{}),831    );832833    /// The remainder of the first bit-vector by the second with the sign of the first, as the834    /// operation `smt.bvsrem`, for a checker taking the signed remainder of a program's division.835    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.836    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.837    /// `operation_name` holds `smt.bvsrem`, and the struct holds the operation in `op`. `create`838    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both839    /// operands and the result share one type. `create` returns the errors of creating the840    /// operation in `ctx`.841    pub const BvSremOp: type = op_templates.binarySameType(842        "bvsrem",843        sameOperandsResultOptions(.{}),844    );845846    /// The modulo of the first bit-vector by the second with the sign of the second, as the847    /// operation `smt.bvsmod`, for a checker taking a signed modulo whose result follows the848    /// divisor's sign. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the849    /// type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the850    /// operands. `operation_name` holds `smt.bvsmod`, and the struct holds the operation in `op`.851    /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:852    /// both operands and the result share one type. `create` returns the errors of creating the853    /// operation in `ctx`.854    pub const BvSmodOp: type = op_templates.binarySameType(855        "bvsmod",856        sameOperandsResultOptions(.{}),857    );858859    /// The bits of the first bit-vector above the bits of the second, as the operation860    /// `smt.bvconcat`, with one result whose width is the sum of the two widths, for a checker861    /// joining two bit-vectors into a wider one, for example two halves of a word. The struct holds862    /// the operation in `op`, creates it with `create`, and returns the result with `getResult`.863    pub const BvConcatOp = struct {864        op: *ir.Operation,865866        /// The specification of `smt.bvconcat`: its full name and its side effects declared as867        /// unknown. `SmtDialect.spec` lists it among the dialect's operations, so loading the868        /// dialect registers the operation with the context. The specification registers no type869        /// rule, so `create` alone checks the operand types.870        pub const operation_spec = op_specs.define(.{871            .mnemonic = "bvconcat",872873            .interfaces = &.{unknown_effects},874        });875        /// The full name of the operation, `smt.bvconcat`, so code that walks operations can876        /// compare each operation's name with this constant to find the concatenations. `create`877        /// creates operations under this name.878        pub const operation_name = operation_spec.name;879880        /// Creates an `smt.bvconcat` operation that joins `lhs` above `rhs` at the source location881        /// `loc`, and returns the struct holding it, for a checker building a wider value from two882        /// parts with `lhs` as the high part. The result is a bit-vector whose width is the width883        /// of `lhs` plus the width of `rhs`. The call returns `error.UnsupportedBitVectorType` when884        /// `bitVecWidth` returns `null` for the type of either operand, and885        /// `error.InvalidBitVectorWidth` when the sum of the widths overflows a `u32`. The new886        /// operation belongs to no block until the caller adds `op` to one. The call also returns887        /// the errors of building the result type and of creating the operation in `ctx`.888        pub fn create(ctx: *ir.Context, loc: ir.Location, lhs: *ir.Value, rhs: *ir.Value) !BvConcatOp {889            const lhs_width = bitVecWidth(ctx, lhs.type) orelse return error.UnsupportedBitVectorType;890            const rhs_width = bitVecWidth(ctx, rhs.type) orelse return error.UnsupportedBitVectorType;891            const result_width = std.math.add(u32, lhs_width, rhs_width) catch return error.InvalidBitVectorWidth;892            return .{ .op = try binary(ctx, loc, operation_name, lhs, rhs, try getBitVecType(ctx, result_width)) };893        }894895        /// Returns the operation's one result, the joined value, so a caller can pass it to the896        /// operations that use it.897        pub fn getResult(self: *const BvConcatOp) *ir.Value {898            return self.op.getResult(0).?;899        }900    };901902    /// The bits of a bit-vector from a high position down to a low position, both included, as the903    /// operation `smt.bvextract`, with the positions in its `high` and `low` attributes, for a904    /// checker taking a range of bits from a bit-vector, for example to narrow a value to a smaller905    /// width. The result is a bit-vector of `high - low + 1` bits. The struct holds the operation906    /// in `op`, creates it with `create`, and reads it with `getResult`, `getHigh` and `getLow`.907    pub const BvExtractOp = struct {908        /// The operation the struct holds. `create` sets it, and a caller reads it to add the909        /// operation to a block. A caller that finds an operation named `operation_name` builds the910        /// struct around it and reads the positions through `getHigh` and `getLow`.911        op: *ir.Operation,912913        /// The specification of `smt.bvextract`: its full name, its attribute keys `high` and914        /// `low`, and its side effects declared as unknown. `SmtDialect.spec` lists it among the915        /// dialect's operations, so loading the dialect registers the operation with the context.916        /// The specification registers no type rule, so `create` alone checks the operand type and917        /// the range.918        pub const operation_spec = op_specs.define(.{919            .mnemonic = "bvextract",920            .attrs = &.{ attr_names.high, attr_names.low },921922            .interfaces = &.{unknown_effects},923        });924        /// The full name of the operation, `smt.bvextract`, so code that walks operations can925        /// compare each operation's name with this constant to find the extractions. `create`926        /// creates operations under this name.927        pub const operation_name = operation_spec.name;928929        /// Creates an `smt.bvextract` operation that keeps the bits of `operand` from position930        /// `high` down to position `low` at the source location `loc`, and returns the struct931        /// holding it, so a checker can narrow a value to fewer bits by keeping its low bits, such932        /// as positions `7` down to `0`. Position 0 is the least significant bit. The result is a933        /// bit-vector of `high - low + 1` bits. The call returns `error.UnsupportedBitVectorType`934        /// when `bitVecWidth` returns `null` for the type of `operand`, and935        /// `error.InvalidBitVectorRange` when `low` is above `high` or `high` is at or above the936        /// operand's width. The new operation belongs to no block until the caller adds `op` to937        /// one. The call also returns the errors of building the result type and of creating the938        /// operation and its attributes in `ctx`.939        pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, high: u32, low: u32) !BvExtractOp {940            const source_width = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;941            if (low > high or high >= source_width) return error.InvalidBitVectorRange;942            var builder = ir.OperationBuilder.init(ctx);943            var state = ir.Operation.State.init(operation_name, loc);944            state.addOperands(&.{operand});945            state.addTypes(&.{try getBitVecType(ctx, high - low + 1)});946            const op = try builder.create(state);947            try op.setAttr(attr_names.high, try ctx.getI64Attr(high));948            try op.setAttr(attr_names.low, try ctx.getI64Attr(low));949            return .{ .op = op };950        }951952        /// Returns the operation's one result, the extracted bits, so a caller can pass them to the953        /// operations that use them.954        pub fn getResult(self: *const BvExtractOp) *ir.Value {955            return self.op.getResult(0).?;956        }957958        /// Returns the highest bit position the extraction keeps, from the `high` attribute, so959        /// code that reads a formula back can build the solver's extraction term. The call returns960        /// `null` when the operation lacks an integer attribute under `high` or its value lies961        /// outside the range of a `u32`.962        pub fn getHigh(self: BvExtractOp) ?u32 {963            return getU32Attr(self.op, attr_names.high);964        }965966        /// Returns the lowest bit position the extraction keeps, from the `low` attribute, so code967        /// that reads a formula back can build the solver's extraction term. The call returns968        /// `null` when the operation lacks an integer attribute under `low` or its value lies969        /// outside the range of a `u32`.970        pub fn getLow(self: BvExtractOp) ?u32 {971            return getU32Attr(self.op, attr_names.low);972        }973    };974975    /// A bit-vector widened by zero bits above its most significant bit, as the operation976    /// `smt.bvzeroext`, with the number of added bits in its `extra` attribute, for a checker977    /// widening an unsigned value to a larger width, for example before comparing it with a wider978    /// value. The result is a bit-vector of the operand's width plus `extra` bits. The struct holds979    /// the operation in `op`, creates it with `create`, and reads it with `getResult` and980    /// `getExtra`.981    pub const BvZeroExtOp = struct {982        /// The operation the struct holds. `create` sets it, and a caller reads it to add the983        /// operation to a block. A caller that finds an operation named `operation_name` builds the984        /// struct around it and reads the added width through `getExtra`.985        op: *ir.Operation,986987        /// The specification of `smt.bvzeroext`: its full name, its one attribute key `extra`, and988        /// its side effects declared as unknown. `SmtDialect.spec` lists it among the dialect's989        /// operations, so loading the dialect registers the operation with the context. The990        /// specification registers no type rule, so `create` alone checks the operand type.991        pub const operation_spec = op_specs.define(.{992            .mnemonic = "bvzeroext",993            .attrs = &.{attr_names.extra},994995            .interfaces = &.{unknown_effects},996        });997        /// The full name of the operation, `smt.bvzeroext`, so code that walks operations can998        /// compare each operation's name with this constant to find the zero extensions. `create`999        /// creates operations under this name.1000        pub const operation_name = operation_spec.name;10011002        /// Creates an `smt.bvzeroext` operation that adds `extra` zero bits above `operand` at the1003        /// source location `loc`, and returns the struct holding it, so a checker can widen an1004        /// unsigned value by the number of bits the target width needs. The result is a bit-vector1005        /// of the operand's width plus `extra` bits, and an `extra` of 0 keeps the width. The call1006        /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type1007        /// of `operand`, and `error.InvalidBitVectorWidth` when the new width overflows a `u32`.1008        /// The new operation belongs to no block until the caller adds `op` to one. The call also1009        /// returns the errors of building the result type and of creating the operation and its1010        /// attribute in `ctx`.1011        pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, extra: u32) !BvZeroExtOp {1012            const source_width = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;1013            const result_width = std.math.add(u32, source_width, extra) catch return error.InvalidBitVectorWidth;1014            var builder = ir.OperationBuilder.init(ctx);1015            var state = ir.Operation.State.init(operation_name, loc);1016            state.addOperands(&.{operand});1017            state.addTypes(&.{try getBitVecType(ctx, result_width)});1018            const op = try builder.create(state);1019            try op.setAttr(attr_names.extra, try ctx.getI64Attr(extra));1020            return .{ .op = op };1021        }10221023        /// Returns the operation's one result, the widened value, so a caller can pass it to the1024        /// operations that use it.1025        pub fn getResult(self: *const BvZeroExtOp) *ir.Value {1026            return self.op.getResult(0).?;1027        }10281029        /// Returns the number of added bits from the `extra` attribute, so code that reads a1030        /// formula back can build the solver's extension term. The call returns `null` when the1031        /// operation lacks an integer attribute under `extra` or its value lies outside the range1032        /// of a `u32`.1033        pub fn getExtra(self: BvZeroExtOp) ?u32 {1034            return getU32Attr(self.op, attr_names.extra);1035        }1036    };10371038    /// A bit-vector widened by copies of its sign bit, as the operation `smt.bvsignext`, with the1039    /// number of added bits in its `extra` attribute. A checker widens a signed value to a larger1040    /// width and keeps its sign. The result is a bit-vector of the operand's width plus `extra`1041    /// bits. The struct holds the operation in `op`, creates it with `create`, and reads it with1042    /// `getResult` and `getExtra`.1043    pub const BvSignExtOp = struct {1044        /// The operation the struct holds. `create` sets it, and a caller reads it to add the1045        /// operation to a block. A caller that finds an operation named `operation_name` builds the1046        /// struct around it and reads the added width through `getExtra`.1047        op: *ir.Operation,10481049        /// The specification of `smt.bvsignext`: its full name, its one attribute key `extra`, and1050        /// its side effects declared as unknown. `SmtDialect.spec` lists it among the dialect's1051        /// operations, so loading the dialect registers the operation with the context. The1052        /// specification registers no type rule, so `create` alone checks the operand type.1053        pub const operation_spec = op_specs.define(.{1054            .mnemonic = "bvsignext",1055            .attrs = &.{attr_names.extra},10561057            .interfaces = &.{unknown_effects},1058        });1059        /// The full name of the operation, `smt.bvsignext`. Code that walks operations compares1060        /// each operation's name with this constant to find the sign extensions, and `create`1061        /// creates operations under this name.1062        pub const operation_name = operation_spec.name;10631064        /// Creates an `smt.bvsignext` operation that adds `extra` copies of the sign bit of1065        /// `operand` above it at the source location `loc`, and returns the struct holding it. A1066        /// checker widens a signed value by the number of bits the target width needs. The result1067        /// is a bit-vector of the operand's width plus `extra` bits, and an `extra` of 0 keeps the1068        /// width. The new operation belongs to no block until the caller adds `op` to one. The call1069        /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type1070        /// of `operand`, and `error.InvalidBitVectorWidth` when the new width overflows a `u32`.1071        /// The call also returns the errors of building the result type and of creating the1072        /// operation and its attribute in `ctx`.1073        pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, extra: u32) !BvSignExtOp {1074            const source_width = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;1075            const result_width = std.math.add(u32, source_width, extra) catch return error.InvalidBitVectorWidth;1076            var builder = ir.OperationBuilder.init(ctx);1077            var state = ir.Operation.State.init(operation_name, loc);1078            state.addOperands(&.{operand});1079            state.addTypes(&.{try getBitVecType(ctx, result_width)});1080            const op = try builder.create(state);1081            try op.setAttr(attr_names.extra, try ctx.getI64Attr(extra));1082            return .{ .op = op };1083        }10841085        /// Returns the operation's one result, the widened value, so a caller can pass the value to1086        /// the operations that use it.1087        pub fn getResult(self: *const BvSignExtOp) *ir.Value {1088            return self.op.getResult(0).?;1089        }10901091        /// Returns the number of added bits from the `extra` attribute, so code that reads a1092        /// formula back can build the solver's extension term. The call returns `null` when the1093        /// operation lacks an integer attribute under `extra` or its value lies outside the range1094        /// of a `u32`.1095        pub fn getExtra(self: BvSignExtOp) ?u32 {1096            return getU32Attr(self.op, attr_names.extra);1097        }1098    };10991100    /// Whether the first bit-vector is less than the second as unsigned numbers, as the operation1101    /// `smt.bvult`, for a checker that states an unsigned bound, for example that an index is below1102    /// a length. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean1103    /// type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.1104    /// `operation_name` holds `smt.bvult`, and the struct holds the operation in `op`. `create`1105    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two1106    /// operands share one type and the result is Boolean. `create` returns the errors of building1107    /// the Boolean type and of creating the operation in `ctx`.1108    pub const BvUltOp: type = op_templates.binaryFixedResult(1109        "bvult",1110        sameOperandBoolResultOptions(.{}),1111        getBoolType,1112    );11131114    /// Whether the first bit-vector is at most the second as unsigned numbers, as the operation1115    /// `smt.bvule`, for a checker that states an unsigned bound that includes its limit, for1116    /// example that an end offset is at most a length. `create(ctx, loc, lhs, rhs)` creates the1117    /// operation with one result of the Boolean type. `getResult` returns the result, and `getLhs`1118    /// and `getRhs` return the operands. `operation_name` holds `smt.bvule`, and the struct holds1119    /// the operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule1120    /// the dialect registered: the two operands share one type and the result is Boolean. `create`1121    /// returns the errors of building the Boolean type and of creating the operation in `ctx`.1122    pub const BvUleOp: type = op_templates.binaryFixedResult(1123        "bvule",1124        sameOperandBoolResultOptions(.{}),1125        getBoolType,1126    );11271128    /// Whether the first bit-vector is less than the second as two's-complement numbers, as the1129    /// operation `smt.bvslt`, for a checker that states a signed bound, for example that a value is1130    /// below a limit as a two's-complement number. `create(ctx, loc, lhs, rhs)` creates the1131    /// operation with one result of the Boolean type. `getResult` returns the result, and `getLhs`1132    /// and `getRhs` return the operands. `operation_name` holds `smt.bvslt`, and the struct holds1133    /// the operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule1134    /// the dialect registered: the two operands share one type and the result is Boolean. `create`1135    /// returns the errors of building the Boolean type and of creating the operation in `ctx`.1136    pub const BvSltOp: type = op_templates.binaryFixedResult(1137        "bvslt",1138        sameOperandBoolResultOptions(.{}),1139        getBoolType,1140    );11411142    /// Whether the first bit-vector is at most the second as two's-complement numbers, as the1143    /// operation `smt.bvsle`, for a checker that states a signed bound that includes its limit, for1144    /// example that an offset is at least zero. `create(ctx, loc, lhs, rhs)` creates the operation1145    /// with one result of the Boolean type. `getResult` returns the result, and `getLhs` and1146    /// `getRhs` return the operands. `operation_name` holds `smt.bvsle`, and the struct holds the1147    /// operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the1148    /// dialect registered: the two operands share one type and the result is Boolean. `create`1149    /// returns the errors of building the Boolean type and of creating the operation in `ctx`.1150    pub const BvSleOp: type = op_templates.binaryFixedResult(1151        "bvsle",1152        sameOperandBoolResultOptions(.{}),1153        getBoolType,1154    );11551156    /// Whether the unsigned sum of two bit-vectors overflows their width, as the operation1157    /// `smt.bvuaddo`, for a checker that asks whether a program's unsigned addition can overflow.1158    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean type.1159    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.1160    /// `operation_name` holds `smt.bvuaddo`, and the struct holds the operation in `op`. `create`1161    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two1162    /// operands share one type and the result is Boolean. The context records the operation as1163    /// commutative. Common subexpression elimination keeps two of these operations with swapped1164    /// operands as two, because every SMT operation declares its side effects as unknown. `create`1165    /// returns the errors of building the Boolean type and of creating the operation in `ctx`.1166    pub const BvUaddoOp: type = op_templates.binaryFixedResult(1167        "bvuaddo",1168        sameOperandBoolResultOptions(commutative_op_traits),1169        getBoolType,1170    );11711172    /// Whether the two's-complement sum of two bit-vectors overflows their width, as the operation1173    /// `smt.bvsaddo`, for a checker that asks whether a program's signed addition can overflow.1174    /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean type.1175    /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.1176    /// `operation_name` holds `smt.bvsaddo`, and the struct holds the operation in `op`. `create`1177    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two1178    /// operands share one type and the result is Boolean. The context records the operation as1179    /// commutative. `create` returns the errors of building the Boolean type and of creating the1180    /// operation in `ctx`.1181    pub const BvSaddoOp: type = op_templates.binaryFixedResult(1182        "bvsaddo",1183        sameOperandBoolResultOptions(commutative_op_traits),1184        getBoolType,1185    );11861187    /// Whether the two's-complement difference of two bit-vectors, the first minus the second,1188    /// overflows their width, as the operation `smt.bvssubo`, for a checker that asks whether a1189    /// program's signed subtraction can overflow. `create(ctx, loc, lhs, rhs)` creates the1190    /// operation with one result of the Boolean type. `getResult` returns the result, and `getLhs`1191    /// and `getRhs` return the operands. `operation_name` holds `smt.bvssubo`, and the struct holds1192    /// the operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule1193    /// the dialect registered: the two operands share one type and the result is Boolean. The1194    /// context records the operation as not commutative. `create` returns the errors of building1195    /// the Boolean type and of creating the operation in `ctx`.1196    pub const BvSsuboOp: type = op_templates.binaryFixedResult(1197        "bvssubo",1198        sameOperandBoolResultOptions(.{}),1199        getBoolType,1200    );12011202    /// Whether the unsigned product of two bit-vectors overflows their width, as the operation1203    /// `smt.bvumulo`, for a checker that asks whether a program's unsigned multiplication can1204    /// overflow. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean1205    /// type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.1206    /// `operation_name` holds `smt.bvumulo`, and the struct holds the operation in `op`. `create`1207    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two1208    /// operands share one type and the result is Boolean. The context records the operation as1209    /// commutative. `create` returns the errors of building the Boolean type and of creating the1210    /// operation in `ctx`.1211    pub const BvUmuloOp: type = op_templates.binaryFixedResult(1212        "bvumulo",1213        sameOperandBoolResultOptions(commutative_op_traits),1214        getBoolType,1215    );12161217    /// Whether the two's-complement product of two bit-vectors overflows their width, as the1218    /// operation `smt.bvsmulo`, for a checker that asks whether a program's signed multiplication1219    /// can overflow. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the1220    /// Boolean type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.1221    /// `operation_name` holds `smt.bvsmulo`, and the struct holds the operation in `op`. `create`1222    /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two1223    /// operands share one type and the result is Boolean. The context records the operation as1224    /// commutative. `create` returns the errors of building the Boolean type and of creating the1225    /// operation in `ctx`.1226    pub const BvSmuloOp: type = op_templates.binaryFixedResult(1227        "bvsmulo",1228        sameOperandBoolResultOptions(commutative_op_traits),1229        getBoolType,1230    );12311232    fn sameOperandsResultOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {1233        return .{1234            .traits = traits,1235            .interfaces = &.{unknown_effects},1236            .dynamic_traits = &.{same_operands_and_result_type_trait},1237        };1238    }12391240    fn boolUnaryOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {1241        return .{1242            .traits = traits,1243            .interfaces = &.{unknown_effects},1244            .operand_types = &.{operand0_is_bool_constraint},1245            .result_types = &.{result0_is_bool_constraint},1246        };1247    }12481249    fn boolBinaryOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {1250        return .{1251            .traits = traits,1252            .interfaces = &.{unknown_effects},1253            .operand_types = &.{ operand0_is_bool_constraint, operand1_is_bool_constraint },1254            .result_types = &.{result0_is_bool_constraint},1255        };1256    }12571258    fn sameOperandBoolResultOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {1259        return .{1260            .traits = traits,1261            .interfaces = &.{unknown_effects},1262            .result_types = &.{result0_is_bool_constraint},1263            .dynamic_traits = &.{same_type_operands_trait},1264        };1265    }12661267    fn deinitBitVecPayload(allocator: std.mem.Allocator, ptr: *anyopaque) void {1268        const payload: *BitVecTypePayload = @ptrCast(@alignCast(ptr));1269        allocator.destroy(payload);1270    }12711272    fn deinitArrayPayload(allocator: std.mem.Allocator, ptr: *anyopaque) void {1273        const payload: *ArrayTypePayload = @ptrCast(@alignCast(ptr));1274        allocator.destroy(payload);1275    }12761277    fn typeParamFallback(ctx: *const ir.Context, typ: ir.Type) ?*const anyopaque {1278        _ = ctx;1279        const type_name = typ.getDialectTypeName() orelse return null;1280        if (!std.mem.eql(u8, type_name, type_names.bv) and !std.mem.eql(u8, type_name, type_names.array)) return null;1281        return &type_param_vtable;1282    }12831284    fn parseTypeParams(type_ptr: *const anyopaque, ctx_opaque: *const interfaces.ContextOpaque) anyerror!?interfaces.TypeParamPayload {1285        const ctx = interfaces.castContext(ir.Context, ctx_opaque);1286        const storage: *const ir.Type.DialectTypeStorage = @ptrCast(@alignCast(type_ptr));1287        if (std.mem.eql(u8, storage.name, type_names.bv)) {1288            if (storage.param_key.len == 0) return null;1289            const width = std.fmt.parseInt(u32, storage.param_key, 10) catch return null;1290            if (width == 0) return null;1291            const payload = try ir.context.typePayloadAllocator(ctx).create(BitVecTypePayload);1292            payload.* = .{ .width = width };1293            return .{ .ptr = payload, .deinit = deinitBitVecPayload };1294        }1295        if (std.mem.eql(u8, storage.name, type_names.array)) {1296            const shape = parseArrayParamKey(storage.param_key) orelse return null;1297            const payload = try ir.context.typePayloadAllocator(ctx).create(ArrayTypePayload);1298            payload.* = shape;1299            return .{ .ptr = payload, .deinit = deinitArrayPayload };1300        }1301        return null;1302    }13031304    fn loadSpec(ctx: *ir.Context) !void {1305        ir.dialects.loadDialectSpec(ctx, spec) catch |err| switch (err) {1306            error.ContextFrozen => {},1307            else => return err,1308        };1309    }13101311    /// Returns the dialect's Boolean type, `smt.bool`, from `ctx`. A caller needs the Boolean type1312    /// to compare a value's type against it, and the Boolean operations' `create` functions build1313    /// it themselves. The call loads the dialect into `ctx` first when the dialect is unloaded.1314    /// Every call on one context returns the same type. On a frozen context that has not loaded the1315    /// dialect and refuses unregistered types (the default), the call returns `error.UnknownType`,1316    /// and the context keeps the dialect marked as loaded with no operations registered. The call1317    /// returns the errors of loading the dialect other than `error.ContextFrozen`, and the errors1318    /// of looking up the type in `ctx`.1319    pub fn getBoolType(ctx: *ir.Context) !ir.Type {1320        try loadSpec(ctx);1321        return ctx.getDialectTypeFromName(type_names.boolean);1322    }13231324    /// Returns the bit-vector type of `width` bits from `ctx`: the type `smt.bv` with `width` as1325    /// decimal text. A checker builds the type of each variable and constant from the width of the1326    /// program value it stands for. The call loads the dialect into `ctx` first when the dialect is1327    /// unloaded. Every call with one width on one context returns the same type. The call accepts a1328    /// `width` of 0 and returns a type whose width `bitVecWidth` reads as `null`. On a frozen1329    /// context that has not loaded the dialect and refuses unregistered types (the default), the1330    /// call returns `error.UnknownType`, and the context keeps the dialect marked as loaded with no1331    /// operations registered. The call returns the errors of loading the dialect other than1332    /// `error.ContextFrozen`, and the errors of looking up or creating the type in `ctx`.1333    pub fn getBitVecType(ctx: *ir.Context, width: u32) !ir.Type {1334        try loadSpec(ctx);1335        var buf: [16]u8 = undefined;1336        const key = try std.fmt.bufPrint(&buf, "{d}", .{width});1337        return ctx.getDialectTypeFromNameWithKey(type_names.bv, key);1338    }13391340    /// Returns the array type from `ctx` whose index is a bit-vector of `index_width` bits and1341    /// whose element is a bit-vector of `element_width` bits: the type `smt.array` with the text1342    /// `index_width:element_width`. A checker builds the type of a memory it models as an array1343    /// from the widths of its addresses and of its cells. The call loads the dialect into `ctx`1344    /// first when the dialect is unloaded. Every call with one pair of widths on one context1345    /// returns the same type. The call accepts a width of 0 and returns a type whose widths1346    /// `arrayShape` reads as `null`. On a frozen context that has not loaded the dialect and1347    /// refuses unregistered types (the default), the call returns `error.UnknownType`, and the1348    /// context keeps the dialect marked as loaded with no operations registered. The call returns1349    /// the errors of loading the dialect other than `error.ContextFrozen`, and the errors of1350    /// looking up or creating the type in `ctx`.1351    pub fn getArrayType(ctx: *ir.Context, index_width: u32, element_width: u32) !ir.Type {1352        try loadSpec(ctx);1353        var buf: [32]u8 = undefined;1354        const key = try std.fmt.bufPrint(&buf, "{d}:{d}", .{ index_width, element_width });1355        return ctx.getDialectTypeFromNameWithKey(type_names.array, key);1356    }13571358    /// Returns the width of the bit-vector type `typ`, so code that reads a formula back can pick a1359    /// solver sort and a constant's width from a value's type. The call returns `null` for a type1360    /// of another kind, for a bit-vector type whose width text fails to parse as a `u32` above 0,1361    /// and when the context fails to parse the width. The context parses the width once per type1362    /// and keeps it. The constructors of the rotation, width-changing and array operations call it1363    /// to check their operands.1364    pub fn bitVecWidth(ctx: *ir.Context, typ: ir.Type) ?u32 {1365        const payload = ctx.getTypeParamPayload(typ, BitVecTypePayload) catch return null;1366        return if (payload) |value| value.width else null;1367    }13681369    /// Returns the index width and the element width of the array type `typ`, as a copy of its1370    /// `ArrayTypePayload`, so code that reads a formula back can pick an array sort from a value's1371    /// type. The call returns `null` for a type of another kind, for an array type whose text fails1372    /// to parse as two `u32` values above 0 joined by one colon, and when the context fails to1373    /// parse the widths. The context parses the widths once per type and keeps them.1374    /// `ArraySelectOp.create` and `ArrayStoreOp.create` call it to check their array operand.1375    pub fn arrayShape(ctx: *ir.Context, typ: ir.Type) ?ArrayTypePayload {1376        const payload = ctx.getTypeParamPayload(typ, ArrayTypePayload) catch return null;1377        return if (payload) |value| value.* else null;1378    }13791380    fn parseArrayParamKey(param_key: []const u8) ?ArrayTypePayload {1381        var parts = std.mem.splitScalar(u8, param_key, ':');1382        const index_text = parts.next() orelse return null;1383        const element_text = parts.next() orelse return null;1384        if (parts.next() != null) return null;1385        const index_width = std.fmt.parseInt(u32, index_text, 10) catch return null;1386        const element_width = std.fmt.parseInt(u32, element_text, 10) catch return null;1387        if (index_width == 0 or element_width == 0) return null;1388        return .{ .index_width = index_width, .element_width = element_width };1389    }13901391    fn getU32Attr(op: *const ir.Operation, attr_name: []const u8) ?u32 {1392        const attr = op.getAttrAs(ir.Attribute.IntegerAttr, attr_name) orelse return null;1393        const value = attr.getValue();1394        if (value < 0 or value > std.math.maxInt(u32)) return null;1395        return @intCast(value);1396    }13971398    fn unary(ctx: *ir.Context, loc: ir.Location, operation_name: []const u8, operand: *ir.Value, result_type: ir.Type) !*ir.Operation {1399        var builder = ir.OperationBuilder.init(ctx);1400        var state = ir.Operation.State.init(operation_name, loc);1401        state.addOperands(&.{operand});1402        state.addTypes(&.{result_type});1403        return builder.create(state);1404    }14051406    fn rotate(ctx: *ir.Context, loc: ir.Location, operation_name: []const u8, operand: *ir.Value, amount: u32) !*ir.Operation {1407        _ = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;1408        const op = try unary(ctx, loc, operation_name, operand, operand.type);1409        try op.setAttr(attr_names.amount, try ctx.getI64Attr(amount));1410        return op;1411    }14121413    fn binary(ctx: *ir.Context, loc: ir.Location, operation_name: []const u8, lhs: *ir.Value, rhs: *ir.Value, result_type: ir.Type) !*ir.Operation {1414        var builder = ir.OperationBuilder.init(ctx);1415        var state = ir.Operation.State.init(operation_name, loc);1416        state.addOperands(&.{ lhs, rhs });1417        state.addTypes(&.{result_type});1418        return builder.create(state);1419    }1420};