lib/smt/src/choir/dialect.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

   1 //! Code that builds formulas in a compiler's intermediate representation needs, for each operator,
   2 //! a way to create the operation and a way to read its parts back. The code defines the SMT
   3 //! dialect: its name and specification, one struct for each of its 42 operations, the functions
   4 //! that build and read its three types, and the functions that make it known to a context. A caller
   5 //! creates each operation from typed values, reads its results and attributes back, and recognizes
   6 //! an operation made elsewhere by the operation's name.
   7 //!
   8 //! Each operation has one struct in `SmtDialect`. The struct holds the operation in `op`, carries
   9 //! the operation's full name in `operation_name`, creates the operation with `create`, and reads
  10 //! its attributes with getters. Every struct except `AssertOp` returns the operation's one result
  11 //! with `getResult`, and an `AssertOp` operation has no result and `getAssertion` returns its one
  12 //! operand. Twenty-nine of the structs come from templates of the intermediate representation, in
  13 //! four shapes: one operand or two, and a result of the first operand's type or a Boolean result.
  14 //! These structs return their operands with `getInput`, or with `getLhs` and `getRhs`.
  15 //!
  16 //! Only the constructors of the rotation, width-changing and array operations check the types of
  17 //! their operands, and they return `error.UnsupportedBitVectorType`, `error.UnsupportedArrayType`,
  18 //! `error.InvalidBitVectorRange`, `error.InvalidBitVectorWidth`, `error.InvalidArrayIndexType` or
  19 //! `error.InvalidArrayElementType`. Every other constructor accepts any values, and the verifier
  20 //! `ir.verifyOperation` checks the rules the dialect registered for the operation. Every
  21 //! constructor returns an operation that belongs to no block, and a caller adds `op` to a block
  22 //! when it needs the operation there. Sixteen constructors build their result type through a type
  23 //! getter first, which loads the dialect: `BoolConstOp`, `BitVecConstOp` and the 14 operations with
  24 //! a Boolean result. On a mutable context that has neither loaded nor registered the dialect, they
  25 //! succeed. Eight constructors check their operands' types through `bitVecWidth` or `arrayShape`
  26 //! first, and return `error.UnsupportedBitVectorType` or `error.UnsupportedArrayType` when that
  27 //! check returns `null`: the two rotations, the two array operations, concatenation, extraction and
  28 //! the two extensions. Eighteen constructors build no type and check none: `VarOp`, `ApplyOp`,
  29 //! `AssertOp` and the 15 operations whose result takes the first operand's type. On a context that
  30 //! has not loaded the dialect, these return `error.ContextFrozen` when the context is frozen, and
  31 //! `error.UnknownDialect` when the context has no loader for `smt` and refuses unregistered
  32 //! dialects, which is the default.
  33 //!
  34 //! The attribute getters return `null` when the operation lacks the attribute or holds another kind
  35 //! of value under its key. The getters that return a result or an operand take it without a check.
  36 //! On a struct built around an operation that lacks that result or operand, the call panics in
  37 //! Debug and ReleaseSafe builds, and its behavior is undefined in ReleaseFast and ReleaseSmall
  38 //! builds. A caller compares the operation's name with `operation_name` before it builds the
  39 //! struct.
  40 //!
  41 //! Every operation declares its side effects as unknown, so the IR's generic optimizations leave it
  42 //! in place. Common subexpression elimination merges no two SMT operations, commutative ones with
  43 //! swapped operands included, and no pass may discard one. The functions `getBoolType`,
  44 //! `getBitVecType` and `getArrayType` build the three types. The functions `bitVecWidth` and
  45 //! `arrayShape` read a type's widths back from a parsed copy that the context keeps for the type
  46 //! (`BitVecTypePayload`, `ArrayTypePayload`). The function `registerDialect` adds the dialect's
  47 //! loader to a context (`registry`), and `loadDialect` loads the dialect at once.
  48 const std = @import("std");
  49 const choir = @import("choir");
  50 const ir = choir.ir;
  51 const interfaces = choir.ir.interfaces;
  52 const names = @import("names.zig");
  53 
  54 pub const attr_names = names.attr_names;
  55 pub const type_names = names.type_names;
  56 
  57 const commutative_op_traits = ir.OperationTraits{ .is_commutative = true };
  58 const unknown_effects = interfaces.EffectOpInterface.entryFor(.{});
  59 
  60 /// The SMT dialect: its name, its specification, one struct per operation, and the functions that
  61 /// build and read its types. A caller names every operation, type getter and width reader of the
  62 /// dialect through this struct, and names the dialect by its `name` when it asks a context to load
  63 /// it. Its 42 operation structs are the declarations that end in `Op`. The namespace re-exports it
  64 /// as `SmtDialect`.
  65 pub const SmtDialect = struct {
  66     /// The dialect's name, `smt`. A caller asks a context for the dialect by this name after
  67     /// registering it. Every operation name and type name of the dialect starts with `smt.`.
  68     /// `registry` records the dialect's loader under this name.
  69     pub const name = "smt";
  70     /// The dialect's specification: its name, its 42 operations, its three type names, and the
  71     /// function that reads the widths of the bit-vector and array types. `loadDialect` and the type
  72     /// getters load the dialect into a context from this value, and a test loads it directly. The
  73     /// list of operations comes from every declaration of `SmtDialect` that carries an operation
  74     /// specification. Loading it a second time into one context returns at once and leaves the
  75     /// context as it was.
  76     pub const spec = ir.dialects.DialectSpec{
  77         .name = name,
  78         .operations = ir.dialects.operations(@This()),
  79         .types = &.{
  80             ir.dialects.typeName(type_names.boolean),
  81             ir.dialects.typeName(type_names.bv),
  82             ir.dialects.typeName(type_names.array),
  83         },
  84         .type_interface_fallbacks = &.{
  85             .{ .id = interfaces.TypeParamInterface.id, .fallback = typeParamFallback },
  86         },
  87     };
  88 
  89     const same_operands_and_result_type_trait = ir.dialects.trait(ir.traits.SameOperandsAndResultType);
  90     const same_type_operands_trait = ir.dialects.trait(ir.traits.SameTypeOperands);
  91     const operand0_is_bool_constraint = ir.dialects.typeConstraint.exact(0, type_names.boolean);
  92     const operand1_is_bool_constraint = ir.dialects.typeConstraint.exact(1, type_names.boolean);
  93     const result0_is_bool_constraint = ir.dialects.typeConstraint.exact(0, type_names.boolean);
  94     const op_specs = ir.dialects.opSpec.dialect(@This());
  95     const op_templates = ir.dialects.operationTemplate.dialect(@This());
  96 
  97     /// The width of a bit-vector type, parsed from the decimal text the type carries. `bitVecWidth`
  98     /// reads a bit-vector type's width through this struct, and a caller reads the width through
  99     /// `bitVecWidth`. The context parses it the first time a caller asks for the type's width and
 100     /// keeps it for the type. The struct holds one field, `width`, the number of bits, at least 1.
 101     /// A type whose text is empty, fails to parse as a decimal number or is 0 gets no payload, so
 102     /// `bitVecWidth` returns `null` for it.
 103     pub const BitVecTypePayload = struct {
 104         width: u32,
 105     };
 106 
 107     /// The index width and the element width of an array type, parsed from the text `index:element`
 108     /// the type carries. `arrayShape` returns an array type's two widths in this struct, and a
 109     /// caller reads the widths from it to pick the sort of an array. The context parses it the
 110     /// first time a caller asks for the type's widths and keeps it for the type. An array type maps
 111     /// bit-vectors of the index width to bit-vectors of the element width. A type whose text
 112     /// differs from two decimal numbers joined by one colon, or holds a 0, gets no payload, so
 113     /// `arrayShape` returns `null` for it.
 114     pub const ArrayTypePayload = struct {
 115         /// The width in bits of the bit-vectors that index the array, at least 1.
 116         /// `ArraySelectOp.create` and `ArrayStoreOp.create` require an index of this width. A
 117         /// caller reads it to build the array's sort.
 118         index_width: u32,
 119         /// The width in bits of the bit-vectors the array holds, at least 1. `ArraySelectOp.create`
 120         /// gives its result this width, and `ArrayStoreOp.create` requires a stored value of this
 121         /// width. A caller reads it to build the array's sort.
 122         element_width: u32,
 123     };
 124 
 125     const type_param_vtable = interfaces.TypeParamInterface.VTable{
 126         .parse = parseTypeParams,
 127     };
 128 
 129     /// A named variable of a given type: the operation `smt.var`, with one result and the
 130     /// variable's name in its `name` attribute. A checker declares each free variable of its
 131     /// formula, such as a parameter or an input of the program it checks, as one of these
 132     /// operations. The struct holds the operation in `op`, creates it with `create`, and reads it
 133     /// with `getResult` and `getName`.
 134     pub const VarOp = struct {
 135         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
 136         /// operation to a block. A caller that finds an operation named `operation_name` builds the
 137         /// struct around it and reads the variable through the getters.
 138         op: *ir.Operation,
 139 
 140         /// The specification of `smt.var`: its full name, its one attribute key `name`, and its
 141         /// side effects declared as unknown. The dialect's specification gathers this value, so
 142         /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it
 143         /// among the dialect's operations.
 144         pub const operation_spec = op_specs.define(.{
 145             .mnemonic = "var",
 146             .attrs = &.{attr_names.name},
 147 
 148             .interfaces = &.{unknown_effects},
 149         });
 150         /// The full name of the operation, `smt.var`. Code that walks operations compares each
 151         /// operation's name with this constant to find the variables. `create` creates operations
 152         /// under this name.
 153         pub const operation_name = operation_spec.name;
 154 
 155         /// Creates an `smt.var` operation named `symbol`, with one result of type `result_type` and
 156         /// the source location `loc`, and returns the struct holding it. A checker calls it once
 157         /// for each parameter or input of the program it checks, with the type of that parameter or
 158         /// input. The context keeps its own copy of `symbol`. Neither the call nor
 159         /// `ir.verifyOperation` checks `result_type`, and a variable may have any type of the
 160         /// context, the dialect's three types included. The new operation belongs to no block until
 161         /// the caller adds `op` to one. The call returns the errors of creating the operation and
 162         /// its attribute in `ctx`.
 163         pub fn create(ctx: *ir.Context, loc: ir.Location, symbol: []const u8, result_type: ir.Type) !VarOp {
 164             var builder = ir.OperationBuilder.init(ctx);
 165             var state = ir.Operation.State.init(operation_name, loc);
 166             state.addTypes(&.{result_type});
 167             const op = try builder.create(state);
 168             try op.setAttr(attr_names.name, try ctx.getStringAttr(symbol));
 169             return .{ .op = op };
 170         }
 171 
 172         /// Returns the operation's one result, the variable's value. A caller passes the variable's
 173         /// value to the operations that use the variable.
 174         pub fn getResult(self: *const VarOp) *ir.Value {
 175             return self.op.getResult(0).?;
 176         }
 177 
 178         /// Returns the variable's name from its `name` attribute. Code that reads a formula back
 179         /// turns each variable into a named constant of the solver under this name. The slice
 180         /// points into the context's copy of the name. The call returns `null` when the operation
 181         /// lacks a string attribute under `name`.
 182         pub fn getName(self: VarOp) ?[]const u8 {
 183             const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.name) orelse return null;
 184             return attr.getValue();
 185         }
 186     };
 187 
 188     /// A Boolean constant: the operation `smt.bool.const`, with one Boolean result and the value in
 189     /// its `value` attribute. A checker states a fixed truth value, for example an obligation that
 190     /// holds for every input, as one of these operations. The struct holds the operation in `op`,
 191     /// creates it with `create`, and reads it with `getResult` and `getValue`.
 192     pub const BoolConstOp = struct {
 193         /// The operation the struct holds. `create` sets it, and a caller reads it to inspect the
 194         /// operation or add it to a block. A caller that finds an operation named `operation_name`
 195         /// builds the struct around it and reads the constant through `getValue`.
 196         op: *ir.Operation,
 197 
 198         /// The specification of `smt.bool.const`: its full name, its one attribute key `value`, and
 199         /// its side effects declared as unknown. The dialect's specification gathers this value, so
 200         /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it
 201         /// among the dialect's operations.
 202         pub const operation_spec = op_specs.define(.{
 203             .mnemonic = "bool.const",
 204             .attrs = &.{attr_names.value},
 205 
 206             .interfaces = &.{unknown_effects},
 207         });
 208         /// The full name of the operation, `smt.bool.const`. Code that walks operations compares
 209         /// each operation's name with this constant to find the Boolean constants. `create` creates
 210         /// operations under this name.
 211         pub const operation_name = operation_spec.name;
 212 
 213         /// Creates an `smt.bool.const` operation holding `value`, with one result of the Boolean
 214         /// type and the source location `loc`, and returns the struct holding it. A checker creates
 215         /// the constant `true` or `false` for an obligation whose answer it knows while it builds
 216         /// the formula. The call builds the Boolean type first, which loads the dialect into `ctx`
 217         /// when unloaded. The new operation belongs to no block until the caller adds `op` to one.
 218         /// The call returns the errors of `getBoolType` and of creating the operation and its
 219         /// attribute in `ctx`.
 220         pub fn create(ctx: *ir.Context, loc: ir.Location, value: bool) !BoolConstOp {
 221             var builder = ir.OperationBuilder.init(ctx);
 222             var state = ir.Operation.State.init(operation_name, loc);
 223             state.addTypes(&.{try getBoolType(ctx)});
 224             const op = try builder.create(state);
 225             try op.setAttr(attr_names.value, try ctx.getBoolAttr(value));
 226             return .{ .op = op };
 227         }
 228 
 229         /// Returns the operation's one result, the constant's value. A caller passes the constant's
 230         /// value to the operations that use it.
 231         pub fn getResult(self: *const BoolConstOp) *ir.Value {
 232             return self.op.getResult(0).?;
 233         }
 234 
 235         /// Returns the constant from its `value` attribute. Code that reads a formula back turns
 236         /// each Boolean constant into the solver's `true` or `false`. The call returns `null` when
 237         /// the operation lacks a Boolean attribute under `value`.
 238         pub fn getValue(self: BoolConstOp) ?bool {
 239             const attr = self.op.getAttrAs(ir.Attribute.BoolAttr, attr_names.value) orelse return null;
 240             return attr.getValue();
 241         }
 242     };
 243 
 244     /// A bit-vector constant: the operation `smt.bv.const`, with one result of a bit-vector type
 245     /// and the value in its `value` attribute as decimal text. A checker states a fixed bit-vector,
 246     /// such as a literal of the program it checks or a limit to compare against, as one of these
 247     /// operations. The struct holds the operation in `op`, creates it with `create`, and reads it
 248     /// with `getResult` and `getValue`. The width lives in the result's type, and the attribute
 249     /// holds only the value.
 250     pub const BitVecConstOp = struct {
 251         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
 252         /// operation to a block. A caller that finds an operation named `operation_name` builds the
 253         /// struct around it and reads the constant through `getValue`.
 254         op: *ir.Operation,
 255 
 256         /// The specification of `smt.bv.const`: its full name, its one attribute key `value`, and
 257         /// its side effects declared as unknown. The dialect's specification gathers this value, so
 258         /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it
 259         /// among the dialect's operations.
 260         pub const operation_spec = op_specs.define(.{
 261             .mnemonic = "bv.const",
 262             .attrs = &.{attr_names.value},
 263 
 264             .interfaces = &.{unknown_effects},
 265         });
 266         /// The full name of the operation, `smt.bv.const`. Code that walks operations compares each
 267         /// operation's name with this constant to find the bit-vector constants. `create` creates
 268         /// operations under this name.
 269         pub const operation_name = operation_spec.name;
 270 
 271         /// Creates an `smt.bv.const` operation holding `value`, with one result of the bit-vector
 272         /// type of width `width` and the source location `loc`, and returns the struct holding it.
 273         /// A checker creates one constant for each literal of the program it checks, and for limits
 274         /// such as the width of a shifted value. The call writes `value` as decimal text into the
 275         /// `value` attribute. The call builds the bit-vector type first, which loads the dialect
 276         /// into `ctx` when unloaded. The call checks neither that `value` fits in `width` bits nor
 277         /// that `width` is above 0. The new operation belongs to no block until the caller adds
 278         /// `op` to one. The call returns the errors of building the type and of creating the
 279         /// operation and its attribute in `ctx`.
 280         pub fn create(ctx: *ir.Context, loc: ir.Location, width: u32, value: u128) !BitVecConstOp {
 281             var builder = ir.OperationBuilder.init(ctx);
 282             var state = ir.Operation.State.init(operation_name, loc);
 283             state.addTypes(&.{try getBitVecType(ctx, width)});
 284             const op = try builder.create(state);
 285             var buf: [40]u8 = undefined;
 286             try op.setAttr(attr_names.value, try ctx.getStringAttr(try std.fmt.bufPrint(&buf, "{d}", .{value})));
 287             return .{ .op = op };
 288         }
 289 
 290         /// Returns the operation's one result, the constant's value. A caller passes the constant's
 291         /// value to the operations that use it.
 292         pub fn getResult(self: *const BitVecConstOp) *ir.Value {
 293             return self.op.getResult(0).?;
 294         }
 295 
 296         /// Returns the constant, parsed from the decimal text of its `value` attribute. Code that
 297         /// reads a formula back turns each bit-vector constant into a solver constant of the
 298         /// result's width. The call returns `null` when the operation lacks a string attribute
 299         /// under `value` or its text fails to parse as a decimal number that fits in a `u128`.
 300         pub fn getValue(self: BitVecConstOp) ?u128 {
 301             const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.value) orelse return null;
 302             return std.fmt.parseInt(u128, attr.getValue(), 10) catch null;
 303         }
 304     };
 305 
 306     /// The application of a function to the operation's operands: the operation `smt.apply`, with
 307     /// one result and the function's name in its `name` attribute. A checker states facts about a
 308     /// function it leaves undefined by applying the function by name to its arguments. The dialect
 309     /// declares no function: the operand types are the argument types, and the result's type is the
 310     /// function's result type. The struct holds the operation in `op`, creates it with `create`,
 311     /// and reads it with `getResult` and `getName`.
 312     pub const ApplyOp = struct {
 313         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
 314         /// operation to a block. A caller that finds an operation named `operation_name` builds the
 315         /// struct around it and reads the function's name through `getName`.
 316         op: *ir.Operation,
 317 
 318         /// The specification of `smt.apply`: its full name, its one attribute key `name`, and its
 319         /// side effects declared as unknown. The dialect's specification gathers this value, so
 320         /// loading the dialect registers the operation with the context. `SmtDialect.spec` lists it
 321         /// among the dialect's operations.
 322         pub const operation_spec = op_specs.define(.{
 323             .mnemonic = "apply",
 324             .attrs = &.{attr_names.name},
 325 
 326             .interfaces = &.{unknown_effects},
 327         });
 328         /// The full name of the operation, `smt.apply`. Code that walks operations compares each
 329         /// operation's name with this constant to find the function applications. `create` creates
 330         /// operations under this name.
 331         pub const operation_name = operation_spec.name;
 332 
 333         /// Creates an `smt.apply` operation that applies the function `function_name` to
 334         /// `operands`, with one result of type `result_type` and the source location `loc`, and
 335         /// returns the struct holding it. A checker applies a function it leaves undefined to the
 336         /// values it passes as arguments. The operation copies `operands`, and the context keeps
 337         /// its own copy of `function_name`. The call checks no types, and `operands` may be empty.
 338         /// The new operation belongs to no block until the caller adds `op` to one. The call
 339         /// returns the errors of creating the operation and its attribute in `ctx`.
 340         pub fn create(ctx: *ir.Context, loc: ir.Location, function_name: []const u8, operands: []const *ir.Value, result_type: ir.Type) !ApplyOp {
 341             var builder = ir.OperationBuilder.init(ctx);
 342             var state = ir.Operation.State.init(operation_name, loc);
 343             state.addOperands(operands);
 344             state.addTypes(&.{result_type});
 345             const op = try builder.create(state);
 346             try op.setAttr(attr_names.name, try ctx.getStringAttr(function_name));
 347             return .{ .op = op };
 348         }
 349 
 350         /// Returns the operation's one result, the value of the application. A caller passes the
 351         /// application's value to the operations that use it.
 352         pub fn getResult(self: *const ApplyOp) *ir.Value {
 353             return self.op.getResult(0).?;
 354         }
 355 
 356         /// Returns the name of the applied function from the `name` attribute. Code that reads a
 357         /// formula back declares an uninterpreted function under this name. The slice points into
 358         /// the context's copy of the name. The call returns `null` when the operation lacks a
 359         /// string attribute under `name`.
 360         pub fn getName(self: ApplyOp) ?[]const u8 {
 361             const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.name) orelse return null;
 362             return attr.getValue();
 363         }
 364     };
 365 
 366     /// A Boolean formula that must hold: the operation `smt.assert`, with one Boolean operand, no
 367     /// result, and an optional name and group label in its `name` and `group` attributes. A checker
 368     /// states each property it must check as one assertion, names it after the check, and gives it
 369     /// a group label so that a report can sort the answers. The struct holds the operation in `op`,
 370     /// creates it with `create`, `createNamed` or `createGrouped`, and reads it with
 371     /// `getAssertion`, `getName` and `getGroup`. A caller keeps a list of the assertion operations,
 372     /// and code that reads the formula back walks that list.
 373     pub const AssertOp = struct {
 374         /// The operation the struct holds. `create` sets it, and a caller appends it to its list of
 375         /// assertions. A caller that reads its list back builds the struct around each operation
 376         /// named `operation_name`.
 377         op: *ir.Operation,
 378 
 379         /// The specification of `smt.assert`: its full name, its attribute keys `name` and `group`,
 380         /// its side effects declared as unknown, and the rule that its operand is Boolean.
 381         /// `SmtDialect.spec` lists it among the dialect's operations, so loading the dialect
 382         /// registers the operation with the context, and `ir.verifyOperation` checks the operand
 383         /// rule.
 384         pub const operation_spec = op_specs.define(.{
 385             .mnemonic = "assert",
 386             .attrs = &.{ attr_names.name, attr_names.group },
 387 
 388             .interfaces = &.{unknown_effects},
 389             .operand_types = &.{operand0_is_bool_constraint},
 390         });
 391         /// The full name of the operation, `smt.assert`. Code that reads a list of assertions back
 392         /// checks each operation's name against this constant before it builds the struct. `create`
 393         /// creates operations under this name. A caller refuses an operation of another name in its
 394         /// list of assertions.
 395         pub const operation_name = operation_spec.name;
 396 
 397         /// Creates an `smt.assert` operation on `assertion` at the source location `loc`, leaves
 398         /// its name and group label unset, and returns the struct holding it. A caller asserts a
 399         /// background fact that its reports leave unnamed, such as an equation that fixes a
 400         /// variable to a witness value. The call checks no type, and `ir.verifyOperation` checks
 401         /// that `assertion` is Boolean. The new operation belongs to no block until the caller adds
 402         /// `op` to one. The call returns the errors of creating the operation in `ctx`.
 403         pub fn create(ctx: *ir.Context, loc: ir.Location, assertion: *ir.Value) !AssertOp {
 404             var builder = ir.OperationBuilder.init(ctx);
 405             var state = ir.Operation.State.init(operation_name, loc);
 406             state.addOperands(&.{assertion});
 407             const op = try builder.create(state);
 408             return .{ .op = op };
 409         }
 410 
 411         /// Creates an `smt.assert` operation on `assertion` with the name `assertion_name`, and
 412         /// leaves its group label unset. A caller asserts a formula under a name, so a report can
 413         /// say which assertion an answer concerns. The call calls `create` and then sets the `name`
 414         /// attribute. The context keeps its own copy of `assertion_name`. The call returns the
 415         /// errors of `create` and of setting the attribute in `ctx`.
 416         pub fn createNamed(ctx: *ir.Context, loc: ir.Location, assertion_name: []const u8, assertion: *ir.Value) !AssertOp {
 417             const op = try create(ctx, loc, assertion);
 418             try op.op.setAttr(attr_names.name, try ctx.getStringAttr(assertion_name));
 419             return op;
 420         }
 421 
 422         /// Creates an `smt.assert` operation on `assertion` with the name `assertion_name` and the
 423         /// group label `group`. A checker asserts each property under a name and a group label such
 424         /// as `bounds` or `overflow`, so a report can sort the answers by kind. The call calls
 425         /// `createNamed` and then sets the `group` attribute. The context keeps its own copies of
 426         /// `assertion_name` and `group`. The call returns the errors of `createNamed` and of
 427         /// setting the attribute in `ctx`.
 428         pub fn createGrouped(ctx: *ir.Context, loc: ir.Location, assertion_name: []const u8, group: []const u8, assertion: *ir.Value) !AssertOp {
 429             const op = try createNamed(ctx, loc, assertion_name, assertion);
 430             try op.op.setAttr(attr_names.group, try ctx.getStringAttr(group));
 431             return op;
 432         }
 433 
 434         /// Returns the operation's one operand, the asserted formula, so code that reads the
 435         /// assertions back turns each asserted formula into a solver term. On an operation with no
 436         /// operand, the call panics in Debug and ReleaseSafe builds, and its behavior is undefined
 437         /// in ReleaseFast and ReleaseSmall builds.
 438         pub fn getAssertion(self: AssertOp) *ir.Value {
 439             return self.op.getOperand(0).?;
 440         }
 441 
 442         /// Returns the assertion's name from its `name` attribute, so code that reports an answer
 443         /// names the assertion it concerns. The call returns `null` whenever the operation lacks a
 444         /// string attribute under `name`, such as for an assertion made by `create`.
 445         pub fn getName(self: AssertOp) ?[]const u8 {
 446             const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.name) orelse return null;
 447             return attr.getValue();
 448         }
 449 
 450         /// Returns the assertion's group label from its `group` attribute, so code that reports
 451         /// answers sorts them by this label. The call returns `null` whenever the operation lacks a
 452         /// string attribute under `group`, such as for an assertion made by `create` or
 453         /// `createNamed`.
 454         pub fn getGroup(self: AssertOp) ?[]const u8 {
 455             const attr = self.op.getAttrAs(ir.Attribute.StringAttr, attr_names.group) orelse return null;
 456             return attr.getValue();
 457         }
 458     };
 459 
 460     /// The negation of a Boolean formula, as the operation `smt.not`. A checker negates a formula,
 461     /// for example to turn a condition that must hold into a search for an input that breaks it.
 462     /// `create(ctx, loc, input)` creates the operation with one result of the Boolean type.
 463     /// `getResult` returns the result, and `getInput` returns the operand. `operation_name` holds
 464     /// `smt.not`, and the struct holds the operation in `op`. `create` checks no type, and
 465     /// `ir.verifyOperation` checks the rule the dialect registered: the operand and the result are
 466     /// Boolean. `create` returns the errors of building the Boolean type and of creating the
 467     /// operation in `ctx`.
 468     pub const NotOp: type = op_templates.unaryFixedResult(
 469         "not",
 470         boolUnaryOptions(.{}),
 471         getBoolType,
 472     );
 473 
 474     /// The conjunction of two Boolean formulas, as the operation `smt.and`. A checker joins two
 475     /// conditions that must both hold. `create(ctx, loc, lhs, rhs)` creates the operation with one
 476     /// result of the Boolean type. `getResult` returns the result, and `getLhs` and `getRhs` return
 477     /// the operands. `operation_name` holds `smt.and`, and the struct holds the operation in `op`.
 478     /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:
 479     /// both operands and the result are Boolean. The context records the operation as commutative.
 480     /// `create` returns the errors of building the Boolean type and of creating the operation in
 481     /// `ctx`.
 482     pub const AndOp: type = op_templates.binaryFixedResult(
 483         "and",
 484         boolBinaryOptions(commutative_op_traits),
 485         getBoolType,
 486     );
 487 
 488     /// The disjunction of two Boolean formulas, as the operation `smt.or`. A checker joins two
 489     /// conditions of which one must hold. `create(ctx, loc, lhs, rhs)` creates the operation with
 490     /// one result of the Boolean type. `getResult` returns the result, and `getLhs` and `getRhs`
 491     /// return the operands. `operation_name` holds `smt.or`, and the struct holds the operation in
 492     /// `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect
 493     /// registered: both operands and the result are Boolean. The context records the operation as
 494     /// commutative. `create` returns the errors of building the Boolean type and of creating the
 495     /// operation in `ctx`.
 496     pub const OrOp: type = op_templates.binaryFixedResult(
 497         "or",
 498         boolBinaryOptions(commutative_op_traits),
 499         getBoolType,
 500     );
 501 
 502     /// The implication from the first Boolean formula to the second, as the operation
 503     /// `smt.implies`. A checker states that one condition implies another, for example that a
 504     /// precondition implies a bound. `create(ctx, loc, lhs, rhs)` creates the operation with one
 505     /// result of the Boolean type. `getResult` returns the result, and `getLhs` and `getRhs` return
 506     /// the operands. `operation_name` holds `smt.implies`, and the struct holds the operation in
 507     /// `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect
 508     /// registered: both operands and the result are Boolean. `create` returns the errors of
 509     /// building the Boolean type and of creating the operation in `ctx`.
 510     pub const ImpliesOp: type = op_templates.binaryFixedResult(
 511         "implies",
 512         boolBinaryOptions(.{}),
 513         getBoolType,
 514     );
 515 
 516     /// The equality of two values of one type, as the operation `smt.eq`. A checker states that two
 517     /// values are equal, for example that a variable holds a given constant or that a result is
 518     /// zero. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean
 519     /// type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 520     /// `operation_name` holds `smt.eq`, and the struct holds the operation in `op`. The operands
 521     /// may be Boolean values, bit-vectors or arrays. `create` checks no types, and
 522     /// `ir.verifyOperation` checks the rule the dialect registered: the two operands share one type
 523     /// and the result is Boolean. The context records the operation as commutative. `create`
 524     /// returns the errors of building the Boolean type and of creating the operation in `ctx`.
 525     pub const EqOp: type = op_templates.binaryFixedResult(
 526         "eq",
 527         sameOperandBoolResultOptions(commutative_op_traits),
 528         getBoolType,
 529     );
 530 
 531     /// The element of an array at an index, as the operation `smt.array.select`, with the array and
 532     /// the index as operands and one result of the element type. A checker reads a memory modeled
 533     /// as an array at an index. The struct holds the operation in `op`, creates it with `create`,
 534     /// and returns the result with `getResult`.
 535     pub const ArraySelectOp = struct {
 536         op: *ir.Operation,
 537 
 538         /// The specification of `smt.array.select`: its full name and its side effects declared as
 539         /// unknown. `SmtDialect.spec` lists it among the dialect's operations, so loading the
 540         /// dialect registers the operation with the context. The specification registers no type
 541         /// rule, so `create` alone checks the operand types.
 542         pub const operation_spec = op_specs.define(.{
 543             .mnemonic = "array.select",
 544 
 545             .interfaces = &.{unknown_effects},
 546         });
 547         /// The full name of the operation, `smt.array.select`. Code that walks operations compares
 548         /// each operation's name with this constant to find the array reads. `create` creates
 549         /// operations under this name.
 550         pub const operation_name = operation_spec.name;
 551 
 552         /// Creates an `smt.array.select` operation that reads `array` at `index` at the source
 553         /// location `loc`, and returns the struct holding it. A checker reads an element of a
 554         /// modeled memory and gets a value of the element's width. The result is a bit-vector of
 555         /// the array's element width. The call returns `error.UnsupportedArrayType` when
 556         /// `arrayShape` returns `null` for the type of `array`, `error.UnsupportedBitVectorType`
 557         /// when `bitVecWidth` returns `null` for the type of `index`, and
 558         /// `error.InvalidArrayIndexType` when the index width differs from the array's index width.
 559         /// The new operation belongs to no block until the caller adds `op` to one. The call also
 560         /// returns the errors of building the element type and of creating the operation in `ctx`.
 561         pub fn create(ctx: *ir.Context, loc: ir.Location, array: *ir.Value, index: *ir.Value) !ArraySelectOp {
 562             const shape = arrayShape(ctx, array.type) orelse return error.UnsupportedArrayType;
 563             const index_width = bitVecWidth(ctx, index.type) orelse return error.UnsupportedBitVectorType;
 564             if (index_width != shape.index_width) return error.InvalidArrayIndexType;
 565             return .{ .op = try binary(ctx, loc, operation_name, array, index, try getBitVecType(ctx, shape.element_width)) };
 566         }
 567 
 568         /// Returns the operation's one result, the element read, so a caller passes it to the
 569         /// operations that use it.
 570         pub fn getResult(self: *const ArraySelectOp) *ir.Value {
 571             return self.op.getResult(0).?;
 572         }
 573     };
 574 
 575     /// The array equal to a given array except that one index holds a new value, as the operation
 576     /// `smt.array.store`, with the array, the index and the value as operands and one result of the
 577     /// array's type. A checker writes an element into a memory modeled as an array and gets the new
 578     /// array. The struct holds the operation in `op`, creates it with `create`, and returns the
 579     /// result with `getResult`.
 580     pub const ArrayStoreOp = struct {
 581         op: *ir.Operation,
 582 
 583         /// The specification of `smt.array.store`: its full name and its side effects declared as
 584         /// unknown. `SmtDialect.spec` lists it among the dialect's operations, so loading the
 585         /// dialect registers the operation with the context. The specification registers no type
 586         /// rule, so `create` alone checks the operand types.
 587         pub const operation_spec = op_specs.define(.{
 588             .mnemonic = "array.store",
 589 
 590             .interfaces = &.{unknown_effects},
 591         });
 592         /// The full name of the operation, `smt.array.store`. Code that walks operations compares
 593         /// each operation's name with this constant to find the array writes. `create` creates
 594         /// operations under this name.
 595         pub const operation_name = operation_spec.name;
 596 
 597         /// Creates an `smt.array.store` operation that writes `value` into `array` at `index` at
 598         /// the source location `loc`, and returns the struct holding it. A checker records a write
 599         /// into a modeled memory as a new array value. The result has the type of `array`. The call
 600         /// returns `error.UnsupportedArrayType` when `arrayShape` returns `null` for the type of
 601         /// `array`, and `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the
 602         /// type of `index` or of `value`. The call returns `error.InvalidArrayIndexType` when the
 603         /// index width differs from the array's index width, and `error.InvalidArrayElementType`
 604         /// when the value's width differs from the array's element width. The new operation belongs
 605         /// to no block until the caller adds `op` to one. The call also returns the errors of
 606         /// creating the operation in `ctx`.
 607         pub fn create(ctx: *ir.Context, loc: ir.Location, array: *ir.Value, index: *ir.Value, value: *ir.Value) !ArrayStoreOp {
 608             const shape = arrayShape(ctx, array.type) orelse return error.UnsupportedArrayType;
 609             const index_width = bitVecWidth(ctx, index.type) orelse return error.UnsupportedBitVectorType;
 610             const element_width = bitVecWidth(ctx, value.type) orelse return error.UnsupportedBitVectorType;
 611             if (index_width != shape.index_width) return error.InvalidArrayIndexType;
 612             if (element_width != shape.element_width) return error.InvalidArrayElementType;
 613             var builder = ir.OperationBuilder.init(ctx);
 614             var state = ir.Operation.State.init(operation_name, loc);
 615             state.addOperands(&.{ array, index, value });
 616             state.addTypes(&.{array.type});
 617             const op = try builder.create(state);
 618             return .{ .op = op };
 619         }
 620 
 621         /// Returns the operation's one result, the array after the write, so a caller passes it to
 622         /// the operations that read or write it next.
 623         pub fn getResult(self: *const ArrayStoreOp) *ir.Value {
 624             return self.op.getResult(0).?;
 625         }
 626     };
 627 
 628     /// The sum of two bit-vectors of one width, modulo 2 to the power of the width, as the
 629     /// operation `smt.bvadd`. A checker lowers a program's addition into this operation.
 630     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.
 631     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 632     /// `operation_name` holds `smt.bvadd`, and the struct holds the operation in `op`. `create`
 633     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 634     /// operands and the result share one type. The context records the operation as commutative.
 635     /// `create` returns the errors of creating the operation in `ctx`.
 636     pub const BvAddOp: type = op_templates.binarySameType(
 637         "bvadd",
 638         sameOperandsResultOptions(commutative_op_traits),
 639     );
 640 
 641     /// The difference of two bit-vectors of one width, the first minus the second, modulo 2 to the
 642     /// power of the width, as the operation `smt.bvsub`. A checker lowers a program's subtraction
 643     /// into this operation. `create(ctx, loc, lhs, rhs)` creates the operation with one result of
 644     /// the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the
 645     /// operands. `operation_name` holds `smt.bvsub`, and the struct holds the operation in `op`.
 646     /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:
 647     /// both operands and the result share one type. `create` returns the errors of creating the
 648     /// operation in `ctx`.
 649     pub const BvSubOp: type = op_templates.binarySameType("bvsub", sameOperandsResultOptions(.{}));
 650 
 651     /// The product of two bit-vectors of one width, modulo 2 to the power of the width, as the
 652     /// operation `smt.bvmul`. A checker lowers a program's multiplication into this operation.
 653     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.
 654     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 655     /// `operation_name` holds `smt.bvmul`, and the struct holds the operation in `op`. `create`
 656     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 657     /// operands and the result share one type. The context records the operation as commutative.
 658     /// `create` returns the errors of creating the operation in `ctx`.
 659     pub const BvMulOp: type = op_templates.binarySameType(
 660         "bvmul",
 661         sameOperandsResultOptions(commutative_op_traits),
 662     );
 663 
 664     /// The bitwise complement of a bit-vector, as the operation `smt.bvnot`. A checker complements
 665     /// every bit of a bit-vector. `create(ctx, loc, input)` creates the operation with one result
 666     /// of the type of `input`. `getResult` returns the result, and `getInput` returns the operand.
 667     /// `operation_name` holds `smt.bvnot`, and the struct holds the operation in `op`. `create`
 668     /// checks no type, and `ir.verifyOperation` checks the rule the dialect registered: the operand
 669     /// and the result share one type. `create` returns the errors of creating the operation in
 670     /// `ctx`.
 671     pub const BvNotOp: type = op_templates.unarySameType("bvnot", sameOperandsResultOptions(.{}));
 672 
 673     /// The bitwise and of two bit-vectors of one width, as the operation `smt.bvand`. A checker
 674     /// masks the bits of a bit-vector. `create(ctx, loc, lhs, rhs)` creates the operation with one
 675     /// result of the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs`
 676     /// return the operands. `operation_name` holds `smt.bvand`, and the struct holds the operation
 677     /// in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect
 678     /// registered: both operands and the result share one type. The context records the operation
 679     /// as commutative. `create` returns the errors of creating the operation in `ctx`.
 680     pub const BvAndOp: type = op_templates.binarySameType(
 681         "bvand",
 682         sameOperandsResultOptions(commutative_op_traits),
 683     );
 684 
 685     /// The bitwise or of two bit-vectors of one width, as the operation `smt.bvor`. A checker sets
 686     /// bits of a bit-vector. `create(ctx, loc, lhs, rhs)` creates the operation with one result of
 687     /// the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the
 688     /// operands. `operation_name` holds `smt.bvor`, and the struct holds the operation in `op`.
 689     /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:
 690     /// both operands and the result share one type. The context records the operation as
 691     /// commutative. `create` returns the errors of creating the operation in `ctx`.
 692     pub const BvOrOp: type = op_templates.binarySameType(
 693         "bvor",
 694         sameOperandsResultOptions(commutative_op_traits),
 695     );
 696 
 697     /// The bitwise exclusive or of two bit-vectors of one width, as the operation `smt.bvxor`. A
 698     /// checker flips bits of a bit-vector. `create(ctx, loc, lhs, rhs)` creates the operation with
 699     /// one result of the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs`
 700     /// return the operands. `operation_name` holds `smt.bvxor`, and the struct holds the operation
 701     /// in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the dialect
 702     /// registered: both operands and the result share one type. The context records the operation
 703     /// as commutative. `create` returns the errors of creating the operation in `ctx`.
 704     pub const BvXorOp: type = op_templates.binarySameType(
 705         "bvxor",
 706         sameOperandsResultOptions(commutative_op_traits),
 707     );
 708 
 709     /// The first bit-vector shifted toward its most significant bit by the value of the second, as
 710     /// the operation `smt.bvshl`. A checker lowers a program's left shift into this operation. The
 711     /// shift amount is a bit-vector of the shifted value's width. `create(ctx, loc, lhs, rhs)`
 712     /// creates the operation with one result of the type of `lhs`. `getResult` returns the result,
 713     /// and `getLhs` and `getRhs` return the operands. `operation_name` holds `smt.bvshl`, and the
 714     /// struct holds the operation in `op`. `create` checks no types, and `ir.verifyOperation`
 715     /// checks the rule the dialect registered: both operands and the result share one type.
 716     /// `create` returns the errors of creating the operation in `ctx`.
 717     pub const BvShlOp: type = op_templates.binarySameType("bvshl", sameOperandsResultOptions(.{}));
 718 
 719     /// The first bit-vector shifted toward its least significant bit by the value of the second,
 720     /// with zeros shifted in, as the operation `smt.bvlshr`. A checker lowers a program's unsigned
 721     /// right shift into this operation. The shift amount is a bit-vector of the shifted value's
 722     /// width. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of
 723     /// `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 724     /// `operation_name` holds `smt.bvlshr`, and the struct holds the operation in `op`. `create`
 725     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 726     /// operands and the result share one type. `create` returns the errors of creating the
 727     /// operation in `ctx`.
 728     pub const BvLshrOp: type = op_templates.binarySameType(
 729         "bvlshr",
 730         sameOperandsResultOptions(.{}),
 731     );
 732 
 733     /// The first bit-vector shifted toward its least significant bit by the value of the second,
 734     /// with copies of its sign bit shifted in, as the operation `smt.bvashr`. A checker lowers a
 735     /// program's signed right shift into this operation. The shift amount is a bit-vector of the
 736     /// shifted value's width. `create(ctx, loc, lhs, rhs)` creates the operation with one result of
 737     /// the type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the
 738     /// operands. `operation_name` holds `smt.bvashr`, and the struct holds the operation in `op`.
 739     /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:
 740     /// both operands and the result share one type. `create` returns the errors of creating the
 741     /// operation in `ctx`.
 742     pub const BvAshrOp: type = op_templates.binarySameType(
 743         "bvashr",
 744         sameOperandsResultOptions(.{}),
 745     );
 746 
 747     /// The rotation of a bit-vector toward its most significant bit by a fixed number of positions,
 748     /// as the operation `smt.bvrotl`, with the number of positions in its `amount` attribute, for a
 749     /// checker that rotates a bit-vector left. The result has the operand's type. The struct holds
 750     /// the operation in `op`, creates it with `create`, and reads it with `getResult` and
 751     /// `getAmount`.
 752     pub const BvRotlOp = struct {
 753         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
 754         /// operation to a block. A caller that finds an operation named `operation_name` builds the
 755         /// struct around it and reads the rotation amount through `getAmount`.
 756         op: *ir.Operation,
 757 
 758         /// The specification of `smt.bvrotl`: its full name, its one attribute key `amount`, its
 759         /// side effects declared as unknown, and the rule that the operand and the result share one
 760         /// type. `SmtDialect.spec` lists it among the dialect's operations, so loading the dialect
 761         /// registers the operation with the context, and `ir.verifyOperation` checks the type rule.
 762         pub const operation_spec = op_specs.define(.{
 763             .mnemonic = "bvrotl",
 764             .attrs = &.{attr_names.amount},
 765 
 766             .interfaces = &.{unknown_effects},
 767             .dynamic_traits = &.{same_operands_and_result_type_trait},
 768         });
 769         /// The full name of the operation, `smt.bvrotl`, so code that walks operations can compare
 770         /// each operation's name with this constant to find the left rotations. `create` creates
 771         /// operations under this name.
 772         pub const operation_name = operation_spec.name;
 773 
 774         /// Creates an `smt.bvrotl` operation that rotates `operand` by `amount` positions at the
 775         /// source location `loc`, and returns the struct holding it, so a checker can rotate a
 776         /// value left by the number of positions it knows when it builds the formula. The call
 777         /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type
 778         /// of `operand`. The call accepts an `amount` at or above the operand's width. The new
 779         /// operation belongs to no block until the caller adds `op` to one. The call also returns
 780         /// the errors of creating the operation and its attribute in `ctx`.
 781         pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, amount: u32) !BvRotlOp {
 782             return .{ .op = try rotate(ctx, loc, operation_name, operand, amount) };
 783         }
 784 
 785         /// Returns the operation's one result, the rotated value, so a caller can pass it to the
 786         /// operations that use it.
 787         pub fn getResult(self: *const BvRotlOp) *ir.Value {
 788             return self.op.getResult(0).?;
 789         }
 790 
 791         /// Returns the rotation amount from the `amount` attribute, so code that reads a formula
 792         /// back can build the solver's rotation term. The call returns `null` when the operation
 793         /// lacks an integer attribute under `amount` or its value lies outside the range of a
 794         /// `u32`.
 795         pub fn getAmount(self: BvRotlOp) ?u32 {
 796             return getU32Attr(self.op, attr_names.amount);
 797         }
 798     };
 799 
 800     /// The rotation of a bit-vector toward its least significant bit by a fixed number of
 801     /// positions, as the operation `smt.bvrotr`, with the number of positions in its `amount`
 802     /// attribute, for a checker that rotates a bit-vector right. The result has the operand's type.
 803     /// The struct holds the operation in `op`, creates it with `create`, and reads it with
 804     /// `getResult` and `getAmount`.
 805     pub const BvRotrOp = struct {
 806         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
 807         /// operation to a block. A caller that finds an operation named `operation_name` builds the
 808         /// struct around it and reads the rotation amount through `getAmount`.
 809         op: *ir.Operation,
 810 
 811         /// The specification of `smt.bvrotr`: its full name, its one attribute key `amount`, its
 812         /// side effects declared as unknown, and the rule that the operand and the result share one
 813         /// type. `SmtDialect.spec` lists it among the dialect's operations, so loading the dialect
 814         /// registers the operation with the context, and `ir.verifyOperation` checks the type rule.
 815         pub const operation_spec = op_specs.define(.{
 816             .mnemonic = "bvrotr",
 817             .attrs = &.{attr_names.amount},
 818 
 819             .interfaces = &.{unknown_effects},
 820             .dynamic_traits = &.{same_operands_and_result_type_trait},
 821         });
 822         /// The full name of the operation, `smt.bvrotr`, so code that walks operations can compare
 823         /// each operation's name with this constant to find the right rotations. `create` creates
 824         /// operations under this name.
 825         pub const operation_name = operation_spec.name;
 826 
 827         /// Creates an `smt.bvrotr` operation that rotates `operand` by `amount` positions at the
 828         /// source location `loc`, and returns the struct holding it, so a checker can rotate a
 829         /// value right by the number of positions it knows when it builds the formula. The call
 830         /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type
 831         /// of `operand`. The call accepts an `amount` at or above the operand's width. The new
 832         /// operation belongs to no block until the caller adds `op` to one. The call also returns
 833         /// the errors of creating the operation and its attribute in `ctx`.
 834         pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, amount: u32) !BvRotrOp {
 835             return .{ .op = try rotate(ctx, loc, operation_name, operand, amount) };
 836         }
 837 
 838         /// Returns the operation's one result, the rotated value, so a caller can pass it to the
 839         /// operations that use it.
 840         pub fn getResult(self: *const BvRotrOp) *ir.Value {
 841             return self.op.getResult(0).?;
 842         }
 843 
 844         /// Returns the rotation amount from the `amount` attribute, so code that reads a formula
 845         /// back can build the solver's rotation term. The call returns `null` when the operation
 846         /// lacks an integer attribute under `amount` or its value lies outside the range of a
 847         /// `u32`.
 848         pub fn getAmount(self: BvRotrOp) ?u32 {
 849             return getU32Attr(self.op, attr_names.amount);
 850         }
 851     };
 852 
 853     /// The unsigned quotient of the first bit-vector by the second, as the operation `smt.bvudiv`,
 854     /// for a checker lowering a program's unsigned division into this operation.
 855     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.
 856     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 857     /// `operation_name` holds `smt.bvudiv`, and the struct holds the operation in `op`. `create`
 858     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 859     /// operands and the result share one type. `create` returns the errors of creating the
 860     /// operation in `ctx`.
 861     pub const BvUdivOp: type = op_templates.binarySameType(
 862         "bvudiv",
 863         sameOperandsResultOptions(.{}),
 864     );
 865 
 866     /// The unsigned remainder of the first bit-vector by the second, as the operation `smt.bvurem`,
 867     /// for a checker taking the unsigned remainder of a program's division.
 868     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.
 869     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 870     /// `operation_name` holds `smt.bvurem`, and the struct holds the operation in `op`. `create`
 871     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 872     /// operands and the result share one type. `create` returns the errors of creating the
 873     /// operation in `ctx`.
 874     pub const BvUremOp: type = op_templates.binarySameType(
 875         "bvurem",
 876         sameOperandsResultOptions(.{}),
 877     );
 878 
 879     /// The two's-complement quotient of the first bit-vector by the second, rounded toward zero, as
 880     /// the operation `smt.bvsdiv`, for a checker lowering a program's signed division into this
 881     /// operation. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of
 882     /// `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 883     /// `operation_name` holds `smt.bvsdiv`, and the struct holds the operation in `op`. `create`
 884     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 885     /// operands and the result share one type. `create` returns the errors of creating the
 886     /// operation in `ctx`.
 887     pub const BvSdivOp: type = op_templates.binarySameType(
 888         "bvsdiv",
 889         sameOperandsResultOptions(.{}),
 890     );
 891 
 892     /// The remainder of the first bit-vector by the second with the sign of the first, as the
 893     /// operation `smt.bvsrem`, for a checker taking the signed remainder of a program's division.
 894     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the type of `lhs`.
 895     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
 896     /// `operation_name` holds `smt.bvsrem`, and the struct holds the operation in `op`. `create`
 897     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: both
 898     /// operands and the result share one type. `create` returns the errors of creating the
 899     /// operation in `ctx`.
 900     pub const BvSremOp: type = op_templates.binarySameType(
 901         "bvsrem",
 902         sameOperandsResultOptions(.{}),
 903     );
 904 
 905     /// The modulo of the first bit-vector by the second with the sign of the second, as the
 906     /// operation `smt.bvsmod`, for a checker taking a signed modulo whose result follows the
 907     /// divisor's sign. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the
 908     /// type of `lhs`. `getResult` returns the result, and `getLhs` and `getRhs` return the
 909     /// operands. `operation_name` holds `smt.bvsmod`, and the struct holds the operation in `op`.
 910     /// `create` checks no types, and `ir.verifyOperation` checks the rule the dialect registered:
 911     /// both operands and the result share one type. `create` returns the errors of creating the
 912     /// operation in `ctx`.
 913     pub const BvSmodOp: type = op_templates.binarySameType(
 914         "bvsmod",
 915         sameOperandsResultOptions(.{}),
 916     );
 917 
 918     /// The bits of the first bit-vector above the bits of the second, as the operation
 919     /// `smt.bvconcat`, with one result whose width is the sum of the two widths, for a checker
 920     /// joining two bit-vectors into a wider one, for example two halves of a word. The struct holds
 921     /// the operation in `op`, creates it with `create`, and returns the result with `getResult`.
 922     pub const BvConcatOp = struct {
 923         op: *ir.Operation,
 924 
 925         /// The specification of `smt.bvconcat`: its full name and its side effects declared as
 926         /// unknown. `SmtDialect.spec` lists it among the dialect's operations, so loading the
 927         /// dialect registers the operation with the context. The specification registers no type
 928         /// rule, so `create` alone checks the operand types.
 929         pub const operation_spec = op_specs.define(.{
 930             .mnemonic = "bvconcat",
 931 
 932             .interfaces = &.{unknown_effects},
 933         });
 934         /// The full name of the operation, `smt.bvconcat`, so code that walks operations can
 935         /// compare each operation's name with this constant to find the concatenations. `create`
 936         /// creates operations under this name.
 937         pub const operation_name = operation_spec.name;
 938 
 939         /// Creates an `smt.bvconcat` operation that joins `lhs` above `rhs` at the source location
 940         /// `loc`, and returns the struct holding it, for a checker building a wider value from two
 941         /// parts with `lhs` as the high part. The result is a bit-vector whose width is the width
 942         /// of `lhs` plus the width of `rhs`. The call returns `error.UnsupportedBitVectorType` when
 943         /// `bitVecWidth` returns `null` for the type of either operand, and
 944         /// `error.InvalidBitVectorWidth` when the sum of the widths overflows a `u32`. The new
 945         /// operation belongs to no block until the caller adds `op` to one. The call also returns
 946         /// the errors of building the result type and of creating the operation in `ctx`.
 947         pub fn create(ctx: *ir.Context, loc: ir.Location, lhs: *ir.Value, rhs: *ir.Value) !BvConcatOp {
 948             const lhs_width = bitVecWidth(ctx, lhs.type) orelse return error.UnsupportedBitVectorType;
 949             const rhs_width = bitVecWidth(ctx, rhs.type) orelse return error.UnsupportedBitVectorType;
 950             const result_width = std.math.add(u32, lhs_width, rhs_width) catch return error.InvalidBitVectorWidth;
 951             return .{ .op = try binary(ctx, loc, operation_name, lhs, rhs, try getBitVecType(ctx, result_width)) };
 952         }
 953 
 954         /// Returns the operation's one result, the joined value, so a caller can pass it to the
 955         /// operations that use it.
 956         pub fn getResult(self: *const BvConcatOp) *ir.Value {
 957             return self.op.getResult(0).?;
 958         }
 959     };
 960 
 961     /// The bits of a bit-vector from a high position down to a low position, both included, as the
 962     /// operation `smt.bvextract`, with the positions in its `high` and `low` attributes, for a
 963     /// checker taking a range of bits from a bit-vector, for example to narrow a value to a smaller
 964     /// width. The result is a bit-vector of `high - low + 1` bits. The struct holds the operation
 965     /// in `op`, creates it with `create`, and reads it with `getResult`, `getHigh` and `getLow`.
 966     pub const BvExtractOp = struct {
 967         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
 968         /// operation to a block. A caller that finds an operation named `operation_name` builds the
 969         /// struct around it and reads the positions through `getHigh` and `getLow`.
 970         op: *ir.Operation,
 971 
 972         /// The specification of `smt.bvextract`: its full name, its attribute keys `high` and
 973         /// `low`, and its side effects declared as unknown. `SmtDialect.spec` lists it among the
 974         /// dialect's operations, so loading the dialect registers the operation with the context.
 975         /// The specification registers no type rule, so `create` alone checks the operand type and
 976         /// the range.
 977         pub const operation_spec = op_specs.define(.{
 978             .mnemonic = "bvextract",
 979             .attrs = &.{ attr_names.high, attr_names.low },
 980 
 981             .interfaces = &.{unknown_effects},
 982         });
 983         /// The full name of the operation, `smt.bvextract`, so code that walks operations can
 984         /// compare each operation's name with this constant to find the extractions. `create`
 985         /// creates operations under this name.
 986         pub const operation_name = operation_spec.name;
 987 
 988         /// Creates an `smt.bvextract` operation that keeps the bits of `operand` from position
 989         /// `high` down to position `low` at the source location `loc`, and returns the struct
 990         /// holding it, so a checker can narrow a value to fewer bits by keeping its low bits, such
 991         /// as positions `7` down to `0`. Position 0 is the least significant bit. The result is a
 992         /// bit-vector of `high - low + 1` bits. The call returns `error.UnsupportedBitVectorType`
 993         /// when `bitVecWidth` returns `null` for the type of `operand`, and
 994         /// `error.InvalidBitVectorRange` when `low` is above `high` or `high` is at or above the
 995         /// operand's width. The new operation belongs to no block until the caller adds `op` to
 996         /// one. The call also returns the errors of building the result type and of creating the
 997         /// operation and its attributes in `ctx`.
 998         pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, high: u32, low: u32) !BvExtractOp {
 999             const source_width = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;
1000             if (low > high or high >= source_width) return error.InvalidBitVectorRange;
1001             var builder = ir.OperationBuilder.init(ctx);
1002             var state = ir.Operation.State.init(operation_name, loc);
1003             state.addOperands(&.{operand});
1004             state.addTypes(&.{try getBitVecType(ctx, high - low + 1)});
1005             const op = try builder.create(state);
1006             try op.setAttr(attr_names.high, try ctx.getI64Attr(high));
1007             try op.setAttr(attr_names.low, try ctx.getI64Attr(low));
1008             return .{ .op = op };
1009         }
1010 
1011         /// Returns the operation's one result, the extracted bits, so a caller can pass them to the
1012         /// operations that use them.
1013         pub fn getResult(self: *const BvExtractOp) *ir.Value {
1014             return self.op.getResult(0).?;
1015         }
1016 
1017         /// Returns the highest bit position the extraction keeps, from the `high` attribute, so
1018         /// code that reads a formula back can build the solver's extraction term. The call returns
1019         /// `null` when the operation lacks an integer attribute under `high` or its value lies
1020         /// outside the range of a `u32`.
1021         pub fn getHigh(self: BvExtractOp) ?u32 {
1022             return getU32Attr(self.op, attr_names.high);
1023         }
1024 
1025         /// Returns the lowest bit position the extraction keeps, from the `low` attribute, so code
1026         /// that reads a formula back can build the solver's extraction term. The call returns
1027         /// `null` when the operation lacks an integer attribute under `low` or its value lies
1028         /// outside the range of a `u32`.
1029         pub fn getLow(self: BvExtractOp) ?u32 {
1030             return getU32Attr(self.op, attr_names.low);
1031         }
1032     };
1033 
1034     /// A bit-vector widened by zero bits above its most significant bit, as the operation
1035     /// `smt.bvzeroext`, with the number of added bits in its `extra` attribute, for a checker
1036     /// widening an unsigned value to a larger width, for example before comparing it with a wider
1037     /// value. The result is a bit-vector of the operand's width plus `extra` bits. The struct holds
1038     /// the operation in `op`, creates it with `create`, and reads it with `getResult` and
1039     /// `getExtra`.
1040     pub const BvZeroExtOp = struct {
1041         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
1042         /// operation to a block. A caller that finds an operation named `operation_name` builds the
1043         /// struct around it and reads the added width through `getExtra`.
1044         op: *ir.Operation,
1045 
1046         /// The specification of `smt.bvzeroext`: its full name, its one attribute key `extra`, and
1047         /// its side effects declared as unknown. `SmtDialect.spec` lists it among the dialect's
1048         /// operations, so loading the dialect registers the operation with the context. The
1049         /// specification registers no type rule, so `create` alone checks the operand type.
1050         pub const operation_spec = op_specs.define(.{
1051             .mnemonic = "bvzeroext",
1052             .attrs = &.{attr_names.extra},
1053 
1054             .interfaces = &.{unknown_effects},
1055         });
1056         /// The full name of the operation, `smt.bvzeroext`, so code that walks operations can
1057         /// compare each operation's name with this constant to find the zero extensions. `create`
1058         /// creates operations under this name.
1059         pub const operation_name = operation_spec.name;
1060 
1061         /// Creates an `smt.bvzeroext` operation that adds `extra` zero bits above `operand` at the
1062         /// source location `loc`, and returns the struct holding it, so a checker can widen an
1063         /// unsigned value by the number of bits the target width needs. The result is a bit-vector
1064         /// of the operand's width plus `extra` bits, and an `extra` of 0 keeps the width. The call
1065         /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type
1066         /// of `operand`, and `error.InvalidBitVectorWidth` when the new width overflows a `u32`.
1067         /// The new operation belongs to no block until the caller adds `op` to one. The call also
1068         /// returns the errors of building the result type and of creating the operation and its
1069         /// attribute in `ctx`.
1070         pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, extra: u32) !BvZeroExtOp {
1071             const source_width = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;
1072             const result_width = std.math.add(u32, source_width, extra) catch return error.InvalidBitVectorWidth;
1073             var builder = ir.OperationBuilder.init(ctx);
1074             var state = ir.Operation.State.init(operation_name, loc);
1075             state.addOperands(&.{operand});
1076             state.addTypes(&.{try getBitVecType(ctx, result_width)});
1077             const op = try builder.create(state);
1078             try op.setAttr(attr_names.extra, try ctx.getI64Attr(extra));
1079             return .{ .op = op };
1080         }
1081 
1082         /// Returns the operation's one result, the widened value, so a caller can pass it to the
1083         /// operations that use it.
1084         pub fn getResult(self: *const BvZeroExtOp) *ir.Value {
1085             return self.op.getResult(0).?;
1086         }
1087 
1088         /// Returns the number of added bits from the `extra` attribute, so code that reads a
1089         /// formula back can build the solver's extension term. The call returns `null` when the
1090         /// operation lacks an integer attribute under `extra` or its value lies outside the range
1091         /// of a `u32`.
1092         pub fn getExtra(self: BvZeroExtOp) ?u32 {
1093             return getU32Attr(self.op, attr_names.extra);
1094         }
1095     };
1096 
1097     /// A bit-vector widened by copies of its sign bit, as the operation `smt.bvsignext`, with the
1098     /// number of added bits in its `extra` attribute. A checker widens a signed value to a larger
1099     /// width and keeps its sign. The result is a bit-vector of the operand's width plus `extra`
1100     /// bits. The struct holds the operation in `op`, creates it with `create`, and reads it with
1101     /// `getResult` and `getExtra`.
1102     pub const BvSignExtOp = struct {
1103         /// The operation the struct holds. `create` sets it, and a caller reads it to add the
1104         /// operation to a block. A caller that finds an operation named `operation_name` builds the
1105         /// struct around it and reads the added width through `getExtra`.
1106         op: *ir.Operation,
1107 
1108         /// The specification of `smt.bvsignext`: its full name, its one attribute key `extra`, and
1109         /// its side effects declared as unknown. `SmtDialect.spec` lists it among the dialect's
1110         /// operations, so loading the dialect registers the operation with the context. The
1111         /// specification registers no type rule, so `create` alone checks the operand type.
1112         pub const operation_spec = op_specs.define(.{
1113             .mnemonic = "bvsignext",
1114             .attrs = &.{attr_names.extra},
1115 
1116             .interfaces = &.{unknown_effects},
1117         });
1118         /// The full name of the operation, `smt.bvsignext`. Code that walks operations compares
1119         /// each operation's name with this constant to find the sign extensions, and `create`
1120         /// creates operations under this name.
1121         pub const operation_name = operation_spec.name;
1122 
1123         /// Creates an `smt.bvsignext` operation that adds `extra` copies of the sign bit of
1124         /// `operand` above it at the source location `loc`, and returns the struct holding it. A
1125         /// checker widens a signed value by the number of bits the target width needs. The result
1126         /// is a bit-vector of the operand's width plus `extra` bits, and an `extra` of 0 keeps the
1127         /// width. The new operation belongs to no block until the caller adds `op` to one. The call
1128         /// returns `error.UnsupportedBitVectorType` when `bitVecWidth` returns `null` for the type
1129         /// of `operand`, and `error.InvalidBitVectorWidth` when the new width overflows a `u32`.
1130         /// The call also returns the errors of building the result type and of creating the
1131         /// operation and its attribute in `ctx`.
1132         pub fn create(ctx: *ir.Context, loc: ir.Location, operand: *ir.Value, extra: u32) !BvSignExtOp {
1133             const source_width = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;
1134             const result_width = std.math.add(u32, source_width, extra) catch return error.InvalidBitVectorWidth;
1135             var builder = ir.OperationBuilder.init(ctx);
1136             var state = ir.Operation.State.init(operation_name, loc);
1137             state.addOperands(&.{operand});
1138             state.addTypes(&.{try getBitVecType(ctx, result_width)});
1139             const op = try builder.create(state);
1140             try op.setAttr(attr_names.extra, try ctx.getI64Attr(extra));
1141             return .{ .op = op };
1142         }
1143 
1144         /// Returns the operation's one result, the widened value, so a caller can pass the value to
1145         /// the operations that use it.
1146         pub fn getResult(self: *const BvSignExtOp) *ir.Value {
1147             return self.op.getResult(0).?;
1148         }
1149 
1150         /// Returns the number of added bits from the `extra` attribute, so code that reads a
1151         /// formula back can build the solver's extension term. The call returns `null` when the
1152         /// operation lacks an integer attribute under `extra` or its value lies outside the range
1153         /// of a `u32`.
1154         pub fn getExtra(self: BvSignExtOp) ?u32 {
1155             return getU32Attr(self.op, attr_names.extra);
1156         }
1157     };
1158 
1159     /// Whether the first bit-vector is less than the second as unsigned numbers, as the operation
1160     /// `smt.bvult`, for a checker that states an unsigned bound, for example that an index is below
1161     /// a length. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean
1162     /// type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
1163     /// `operation_name` holds `smt.bvult`, and the struct holds the operation in `op`. `create`
1164     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two
1165     /// operands share one type and the result is Boolean. `create` returns the errors of building
1166     /// the Boolean type and of creating the operation in `ctx`.
1167     pub const BvUltOp: type = op_templates.binaryFixedResult(
1168         "bvult",
1169         sameOperandBoolResultOptions(.{}),
1170         getBoolType,
1171     );
1172 
1173     /// Whether the first bit-vector is at most the second as unsigned numbers, as the operation
1174     /// `smt.bvule`, for a checker that states an unsigned bound that includes its limit, for
1175     /// example that an end offset is at most a length. `create(ctx, loc, lhs, rhs)` creates the
1176     /// operation with one result of the Boolean type. `getResult` returns the result, and `getLhs`
1177     /// and `getRhs` return the operands. `operation_name` holds `smt.bvule`, and the struct holds
1178     /// the operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule
1179     /// the dialect registered: the two operands share one type and the result is Boolean. `create`
1180     /// returns the errors of building the Boolean type and of creating the operation in `ctx`.
1181     pub const BvUleOp: type = op_templates.binaryFixedResult(
1182         "bvule",
1183         sameOperandBoolResultOptions(.{}),
1184         getBoolType,
1185     );
1186 
1187     /// Whether the first bit-vector is less than the second as two's-complement numbers, as the
1188     /// operation `smt.bvslt`, for a checker that states a signed bound, for example that a value is
1189     /// below a limit as a two's-complement number. `create(ctx, loc, lhs, rhs)` creates the
1190     /// operation with one result of the Boolean type. `getResult` returns the result, and `getLhs`
1191     /// and `getRhs` return the operands. `operation_name` holds `smt.bvslt`, and the struct holds
1192     /// the operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule
1193     /// the dialect registered: the two operands share one type and the result is Boolean. `create`
1194     /// returns the errors of building the Boolean type and of creating the operation in `ctx`.
1195     pub const BvSltOp: type = op_templates.binaryFixedResult(
1196         "bvslt",
1197         sameOperandBoolResultOptions(.{}),
1198         getBoolType,
1199     );
1200 
1201     /// Whether the first bit-vector is at most the second as two's-complement numbers, as the
1202     /// operation `smt.bvsle`, for a checker that states a signed bound that includes its limit, for
1203     /// example that an offset is at least zero. `create(ctx, loc, lhs, rhs)` creates the operation
1204     /// with one result of the Boolean type. `getResult` returns the result, and `getLhs` and
1205     /// `getRhs` return the operands. `operation_name` holds `smt.bvsle`, and the struct holds the
1206     /// operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule the
1207     /// dialect registered: the two operands share one type and the result is Boolean. `create`
1208     /// returns the errors of building the Boolean type and of creating the operation in `ctx`.
1209     pub const BvSleOp: type = op_templates.binaryFixedResult(
1210         "bvsle",
1211         sameOperandBoolResultOptions(.{}),
1212         getBoolType,
1213     );
1214 
1215     /// Whether the unsigned sum of two bit-vectors overflows their width, as the operation
1216     /// `smt.bvuaddo`, for a checker that asks whether a program's unsigned addition can overflow.
1217     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean type.
1218     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
1219     /// `operation_name` holds `smt.bvuaddo`, and the struct holds the operation in `op`. `create`
1220     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two
1221     /// operands share one type and the result is Boolean. The context records the operation as
1222     /// commutative. Common subexpression elimination keeps two of these operations with swapped
1223     /// operands as two, because every SMT operation declares its side effects as unknown. `create`
1224     /// returns the errors of building the Boolean type and of creating the operation in `ctx`.
1225     pub const BvUaddoOp: type = op_templates.binaryFixedResult(
1226         "bvuaddo",
1227         sameOperandBoolResultOptions(commutative_op_traits),
1228         getBoolType,
1229     );
1230 
1231     /// Whether the two's-complement sum of two bit-vectors overflows their width, as the operation
1232     /// `smt.bvsaddo`, for a checker that asks whether a program's signed addition can overflow.
1233     /// `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean type.
1234     /// `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
1235     /// `operation_name` holds `smt.bvsaddo`, and the struct holds the operation in `op`. `create`
1236     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two
1237     /// operands share one type and the result is Boolean. The context records the operation as
1238     /// commutative. `create` returns the errors of building the Boolean type and of creating the
1239     /// operation in `ctx`.
1240     pub const BvSaddoOp: type = op_templates.binaryFixedResult(
1241         "bvsaddo",
1242         sameOperandBoolResultOptions(commutative_op_traits),
1243         getBoolType,
1244     );
1245 
1246     /// Whether the two's-complement difference of two bit-vectors, the first minus the second,
1247     /// overflows their width, as the operation `smt.bvssubo`, for a checker that asks whether a
1248     /// program's signed subtraction can overflow. `create(ctx, loc, lhs, rhs)` creates the
1249     /// operation with one result of the Boolean type. `getResult` returns the result, and `getLhs`
1250     /// and `getRhs` return the operands. `operation_name` holds `smt.bvssubo`, and the struct holds
1251     /// the operation in `op`. `create` checks no types, and `ir.verifyOperation` checks the rule
1252     /// the dialect registered: the two operands share one type and the result is Boolean. The
1253     /// context records the operation as not commutative. `create` returns the errors of building
1254     /// the Boolean type and of creating the operation in `ctx`.
1255     pub const BvSsuboOp: type = op_templates.binaryFixedResult(
1256         "bvssubo",
1257         sameOperandBoolResultOptions(.{}),
1258         getBoolType,
1259     );
1260 
1261     /// Whether the unsigned product of two bit-vectors overflows their width, as the operation
1262     /// `smt.bvumulo`, for a checker that asks whether a program's unsigned multiplication can
1263     /// overflow. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the Boolean
1264     /// type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
1265     /// `operation_name` holds `smt.bvumulo`, and the struct holds the operation in `op`. `create`
1266     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two
1267     /// operands share one type and the result is Boolean. The context records the operation as
1268     /// commutative. `create` returns the errors of building the Boolean type and of creating the
1269     /// operation in `ctx`.
1270     pub const BvUmuloOp: type = op_templates.binaryFixedResult(
1271         "bvumulo",
1272         sameOperandBoolResultOptions(commutative_op_traits),
1273         getBoolType,
1274     );
1275 
1276     /// Whether the two's-complement product of two bit-vectors overflows their width, as the
1277     /// operation `smt.bvsmulo`, for a checker that asks whether a program's signed multiplication
1278     /// can overflow. `create(ctx, loc, lhs, rhs)` creates the operation with one result of the
1279     /// Boolean type. `getResult` returns the result, and `getLhs` and `getRhs` return the operands.
1280     /// `operation_name` holds `smt.bvsmulo`, and the struct holds the operation in `op`. `create`
1281     /// checks no types, and `ir.verifyOperation` checks the rule the dialect registered: the two
1282     /// operands share one type and the result is Boolean. The context records the operation as
1283     /// commutative. `create` returns the errors of building the Boolean type and of creating the
1284     /// operation in `ctx`.
1285     pub const BvSmuloOp: type = op_templates.binaryFixedResult(
1286         "bvsmulo",
1287         sameOperandBoolResultOptions(commutative_op_traits),
1288         getBoolType,
1289     );
1290 
1291     fn sameOperandsResultOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {
1292         return .{
1293             .traits = traits,
1294             .interfaces = &.{unknown_effects},
1295             .dynamic_traits = &.{same_operands_and_result_type_trait},
1296         };
1297     }
1298 
1299     fn boolUnaryOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {
1300         return .{
1301             .traits = traits,
1302             .interfaces = &.{unknown_effects},
1303             .operand_types = &.{operand0_is_bool_constraint},
1304             .result_types = &.{result0_is_bool_constraint},
1305         };
1306     }
1307 
1308     fn boolBinaryOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {
1309         return .{
1310             .traits = traits,
1311             .interfaces = &.{unknown_effects},
1312             .operand_types = &.{ operand0_is_bool_constraint, operand1_is_bool_constraint },
1313             .result_types = &.{result0_is_bool_constraint},
1314         };
1315     }
1316 
1317     fn sameOperandBoolResultOptions(comptime traits: ir.OperationTraits) ir.dialects.opSpec.Options {
1318         return .{
1319             .traits = traits,
1320             .interfaces = &.{unknown_effects},
1321             .result_types = &.{result0_is_bool_constraint},
1322             .dynamic_traits = &.{same_type_operands_trait},
1323         };
1324     }
1325 
1326     fn deinitBitVecPayload(allocator: std.mem.Allocator, ptr: *anyopaque) void {
1327         const payload: *BitVecTypePayload = @ptrCast(@alignCast(ptr));
1328         allocator.destroy(payload);
1329     }
1330 
1331     fn deinitArrayPayload(allocator: std.mem.Allocator, ptr: *anyopaque) void {
1332         const payload: *ArrayTypePayload = @ptrCast(@alignCast(ptr));
1333         allocator.destroy(payload);
1334     }
1335 
1336     fn typeParamFallback(ctx: *const ir.Context, typ: ir.Type) ?*const anyopaque {
1337         _ = ctx;
1338         const type_name = typ.getDialectTypeName() orelse return null;
1339         if (!std.mem.eql(u8, type_name, type_names.bv) and !std.mem.eql(u8, type_name, type_names.array)) return null;
1340         return &type_param_vtable;
1341     }
1342 
1343     fn parseTypeParams(type_ptr: *const anyopaque, ctx_opaque: *const interfaces.ContextOpaque) anyerror!?interfaces.TypeParamPayload {
1344         const ctx = interfaces.castContext(ir.Context, ctx_opaque);
1345         const storage: *const ir.Type.DialectTypeStorage = @ptrCast(@alignCast(type_ptr));
1346         if (std.mem.eql(u8, storage.name, type_names.bv)) {
1347             if (storage.param_key.len == 0) return null;
1348             const width = std.fmt.parseInt(u32, storage.param_key, 10) catch return null;
1349             if (width == 0) return null;
1350             const payload = try ir.context.typePayloadAllocator(ctx).create(BitVecTypePayload);
1351             payload.* = .{ .width = width };
1352             return .{ .ptr = payload, .deinit = deinitBitVecPayload };
1353         }
1354         if (std.mem.eql(u8, storage.name, type_names.array)) {
1355             const shape = parseArrayParamKey(storage.param_key) orelse return null;
1356             const payload = try ir.context.typePayloadAllocator(ctx).create(ArrayTypePayload);
1357             payload.* = shape;
1358             return .{ .ptr = payload, .deinit = deinitArrayPayload };
1359         }
1360         return null;
1361     }
1362 
1363     fn loadSpec(ctx: *ir.Context) !void {
1364         ir.dialects.loadDialectSpec(ctx, spec) catch |err| switch (err) {
1365             error.ContextFrozen => {},
1366             else => return err,
1367         };
1368     }
1369 
1370     /// Returns the dialect's Boolean type, `smt.bool`, from `ctx`. A caller needs the Boolean type
1371     /// to compare a value's type against it, and the Boolean operations' `create` functions build
1372     /// it themselves. The call loads the dialect into `ctx` first when the dialect is unloaded.
1373     /// Every call on one context returns the same type. On a frozen context that has not loaded the
1374     /// dialect and refuses unregistered types (the default), the call returns `error.UnknownType`,
1375     /// and the context keeps the dialect marked as loaded with no operations registered. The call
1376     /// returns the errors of loading the dialect other than `error.ContextFrozen`, and the errors
1377     /// of looking up the type in `ctx`.
1378     pub fn getBoolType(ctx: *ir.Context) !ir.Type {
1379         try loadSpec(ctx);
1380         return ctx.getDialectTypeFromName(type_names.boolean);
1381     }
1382 
1383     /// Returns the bit-vector type of `width` bits from `ctx`: the type `smt.bv` with `width` as
1384     /// decimal text. A checker builds the type of each variable and constant from the width of the
1385     /// program value it stands for. The call loads the dialect into `ctx` first when the dialect is
1386     /// unloaded. Every call with one width on one context returns the same type. The call accepts a
1387     /// `width` of 0 and returns a type whose width `bitVecWidth` reads as `null`. On a frozen
1388     /// context that has not loaded the dialect and refuses unregistered types (the default), the
1389     /// call returns `error.UnknownType`, and the context keeps the dialect marked as loaded with no
1390     /// operations registered. The call returns the errors of loading the dialect other than
1391     /// `error.ContextFrozen`, and the errors of looking up or creating the type in `ctx`.
1392     pub fn getBitVecType(ctx: *ir.Context, width: u32) !ir.Type {
1393         try loadSpec(ctx);
1394         var buf: [16]u8 = undefined;
1395         const key = try std.fmt.bufPrint(&buf, "{d}", .{width});
1396         return ctx.getDialectTypeFromNameWithKey(type_names.bv, key);
1397     }
1398 
1399     /// Returns the array type from `ctx` whose index is a bit-vector of `index_width` bits and
1400     /// whose element is a bit-vector of `element_width` bits: the type `smt.array` with the text
1401     /// `index_width:element_width`. A checker builds the type of a memory it models as an array
1402     /// from the widths of its addresses and of its cells. The call loads the dialect into `ctx`
1403     /// first when the dialect is unloaded. Every call with one pair of widths on one context
1404     /// returns the same type. The call accepts a width of 0 and returns a type whose widths
1405     /// `arrayShape` reads as `null`. On a frozen context that has not loaded the dialect and
1406     /// refuses unregistered types (the default), the call returns `error.UnknownType`, and the
1407     /// context keeps the dialect marked as loaded with no operations registered. The call returns
1408     /// the errors of loading the dialect other than `error.ContextFrozen`, and the errors of
1409     /// looking up or creating the type in `ctx`.
1410     pub fn getArrayType(ctx: *ir.Context, index_width: u32, element_width: u32) !ir.Type {
1411         try loadSpec(ctx);
1412         var buf: [32]u8 = undefined;
1413         const key = try std.fmt.bufPrint(&buf, "{d}:{d}", .{ index_width, element_width });
1414         return ctx.getDialectTypeFromNameWithKey(type_names.array, key);
1415     }
1416 
1417     /// Returns the width of the bit-vector type `typ`, so code that reads a formula back can pick a
1418     /// solver sort and a constant's width from a value's type. The call returns `null` for a type
1419     /// of another kind, for a bit-vector type whose width text fails to parse as a `u32` above 0,
1420     /// and when the context fails to parse the width. The context parses the width once per type
1421     /// and keeps it. The constructors of the rotation, width-changing and array operations call it
1422     /// to check their operands.
1423     pub fn bitVecWidth(ctx: *ir.Context, typ: ir.Type) ?u32 {
1424         const payload = ctx.getTypeParamPayload(typ, BitVecTypePayload) catch return null;
1425         return if (payload) |value| value.width else null;
1426     }
1427 
1428     /// Returns the index width and the element width of the array type `typ`, as a copy of its
1429     /// `ArrayTypePayload`, so code that reads a formula back can pick an array sort from a value's
1430     /// type. The call returns `null` for a type of another kind, for an array type whose text fails
1431     /// to parse as two `u32` values above 0 joined by one colon, and when the context fails to
1432     /// parse the widths. The context parses the widths once per type and keeps them.
1433     /// `ArraySelectOp.create` and `ArrayStoreOp.create` call it to check their array operand.
1434     pub fn arrayShape(ctx: *ir.Context, typ: ir.Type) ?ArrayTypePayload {
1435         const payload = ctx.getTypeParamPayload(typ, ArrayTypePayload) catch return null;
1436         return if (payload) |value| value.* else null;
1437     }
1438 
1439     fn parseArrayParamKey(param_key: []const u8) ?ArrayTypePayload {
1440         var parts = std.mem.splitScalar(u8, param_key, ':');
1441         const index_text = parts.next() orelse return null;
1442         const element_text = parts.next() orelse return null;
1443         if (parts.next() != null) return null;
1444         const index_width = std.fmt.parseInt(u32, index_text, 10) catch return null;
1445         const element_width = std.fmt.parseInt(u32, element_text, 10) catch return null;
1446         if (index_width == 0 or element_width == 0) return null;
1447         return .{ .index_width = index_width, .element_width = element_width };
1448     }
1449 
1450     fn getU32Attr(op: *const ir.Operation, attr_name: []const u8) ?u32 {
1451         const attr = op.getAttrAs(ir.Attribute.IntegerAttr, attr_name) orelse return null;
1452         const value = attr.getValue();
1453         if (value < 0 or value > std.math.maxInt(u32)) return null;
1454         return @intCast(value);
1455     }
1456 
1457     fn unary(ctx: *ir.Context, loc: ir.Location, operation_name: []const u8, operand: *ir.Value, result_type: ir.Type) !*ir.Operation {
1458         var builder = ir.OperationBuilder.init(ctx);
1459         var state = ir.Operation.State.init(operation_name, loc);
1460         state.addOperands(&.{operand});
1461         state.addTypes(&.{result_type});
1462         return builder.create(state);
1463     }
1464 
1465     fn rotate(ctx: *ir.Context, loc: ir.Location, operation_name: []const u8, operand: *ir.Value, amount: u32) !*ir.Operation {
1466         _ = bitVecWidth(ctx, operand.type) orelse return error.UnsupportedBitVectorType;
1467         const op = try unary(ctx, loc, operation_name, operand, operand.type);
1468         try op.setAttr(attr_names.amount, try ctx.getI64Attr(amount));
1469         return op;
1470     }
1471 
1472     fn binary(ctx: *ir.Context, loc: ir.Location, operation_name: []const u8, lhs: *ir.Value, rhs: *ir.Value, result_type: ir.Type) !*ir.Operation {
1473         var builder = ir.OperationBuilder.init(ctx);
1474         var state = ir.Operation.State.init(operation_name, loc);
1475         state.addOperands(&.{ lhs, rhs });
1476         state.addTypes(&.{result_type});
1477         return builder.create(state);
1478     }
1479 };
1480 
1481 fn loadSmtDialect(ctx: *ir.Context) !void {
1482     try ir.dialects.loadDialectSpec(ctx, SmtDialect.spec);
1483 }
1484 
1485 /// The dialect's registry entry: the name `smt` paired with the function that loads the dialect's
1486 /// specification. `registerDialect` hands this value to a context, so the context can load the
1487 /// dialect when it first meets the name `smt`. The namespace re-exports it as `registry`.
1488 pub const registry = ir.dialects.DialectRegistrySpec{
1489     .entries = &[_]ir.dialects.DialectRegistryEntry{
1490         .{ .name = SmtDialect.name, .load = loadSmtDialect },
1491     },
1492 };
1493 
1494 /// Adds the dialect's loader to the registry of `ctx` under the name `smt`, for a caller that
1495 /// prepares a context for the dialect so the context loads the dialect when it first meets the name
1496 /// `smt`. The call leaves the dialect unloaded, and the context loads it when code asks for the
1497 /// dialect by name or creates an operation or a type whose name starts with `smt.`. A second call
1498 /// on one context returns `error.DuplicateDialectLoader` and leaves the first loader in place, so a
1499 /// caller that may call it twice can treat that error as success. The call returns
1500 /// `error.ContextFrozen` on a frozen context, and the errors of recording the loader.
1501 pub fn registerDialect(ctx: *ir.Context) !void {
1502     try ctx.appendDialectRegistry(registry);
1503 }
1504 
1505 /// Loads the dialect's specification into `ctx`, registering its operations and types, for a caller
1506 /// that wants the dialect's operations registered with a context at once and for the package's
1507 /// tests before they build operations. A call on a context that already holds the dialect returns
1508 /// at once. The call needs no `registerDialect` first. The call returns the errors of loading the
1509 /// specification into `ctx`.
1510 pub fn loadDialect(ctx: *ir.Context) !void {
1511     try loadSmtDialect(ctx);
1512 }