tiny.smt.choir.names

1//! Code that reads a formula back from an intermediate representation tells its types apart and2//! finds each operation's extra data by comparing names as text, so those names live in one place.3//! The file holds the names of the dialect's three types and the keys of the seven attributes its4//! operations carry. The dialect registers its types and builds its operations under these names,5//! and a reader of those types and operations has to use the same spelling.6//!7//! Each type name starts with the dialect's name and a dot (`smt.bool`, `smt.bv` and `smt.array`),8//! and the intermediate representation finds the dialect that owns a type from that first part. The9//! attribute keys are plain words with no prefix. `name` belongs to variables, function10//! applications and assertions, `group` to assertions, `value` to constants, `high` and `low` to11//! extractions, `extra` to zero and sign extensions, and `amount` to rotations. `AssertOp.create`12//! sets no attribute, `createNamed` sets `name`, and `createGrouped` sets `group`. Every other13//! struct with attributes in `SmtDialect` sets them in `create`, and each operation's struct reads14//! them through getters, so a caller uses the keys to set or read an attribute on an operation it15//! builds or holds without that struct.16/// The names of the dialect's three types, `boolean`, `bv` and `array`. Code that turns a type back17/// into a solver sort compares the type's name with these constants to tell the three types apart.18/// The dialect registers its types under these names, and the type getters of `SmtDialect` build19/// types under them. The namespace and the `dialect` file re-export it.20pub const type_names = struct {21    /// The name of the Boolean type, `smt.bool`. Code that turns a type into a solver sort compares22    /// the type's name with this constant to recognize a Boolean value. `SmtDialect.getBoolType`23    /// returns the type.24    pub const boolean = "smt.bool";25    /// The name every bit-vector type shares, `smt.bv`. Code compares a type's name with this26    /// constant before it reads a bit-vector's width. Each bit-vector type carries its width as27    /// decimal text, such as `64`, in a key separate from this name, and this name stays the same28    /// for every width. `SmtDialect.getBitVecType` builds these types, and `SmtDialect.bitVecWidth`29    /// reads the width back.30    pub const bv = "smt.bv";31    /// The name every array type shares, `smt.array`. Code compares a type's name with this32    /// constant before it reads an array's widths. Each array type carries its index width and its33    /// element width as text, such as `8:32`, in a key separate from this name, and this name stays34    /// the same for every pair of widths. `SmtDialect.getArrayType` builds these types, and35    /// `SmtDialect.arrayShape` reads the widths back.36    pub const array = "smt.array";37};3839/// The keys of the seven attributes the dialect's operations carry. The operation structs of40/// `SmtDialect` set and read every attribute under these keys, and a caller that reads an attribute41/// straight from an `ir.Operation` uses the same key. Each operation's specification lists the keys42/// of its attributes, and its struct's getters read the attributes back. The namespace and the43/// `dialect` file re-export it.44pub const attr_names = struct {45    /// The key of a name, `name`, held as a string attribute. The structs of variables, function46    /// applications and assertions store and read a name under this key. It names a variable47    /// (`VarOp`), the function an application applies (`ApplyOp`), and an assertion (`AssertOp`).48    pub const name = "name";49    /// The key of an assertion's group label, `group`, held as a string attribute.50    /// `AssertOp.createGrouped` stores an assertion's group label under this key, and51    /// `AssertOp.getGroup` reads it back.52    pub const group = "group";53    /// The key of a constant's value, `value`. The two constant operations store their value under54    /// this key, and their `getValue` functions read it back. `BoolConstOp` holds the value as a55    /// Boolean attribute. `BitVecConstOp` holds the value as decimal text in a string attribute.56    pub const value = "value";57    /// The key of the highest bit position an extraction keeps, `high`, held as an integer58    /// attribute. `BvExtractOp.create` stores the extraction's upper bit position under this key,59    /// and `BvExtractOp.getHigh` reads it back.60    pub const high = "high";61    /// The key of the lowest bit position an extraction keeps, `low`, held as an integer attribute.62    /// `BvExtractOp.create` stores the extraction's lower bit position under this key, and63    /// `BvExtractOp.getLow` reads it back.64    pub const low = "low";65    /// The key of the number of bits an extension adds, `extra`, held as an integer attribute. The66    /// zero and sign extension operations store the number of added bits under this key, and their67    /// `getExtra` functions read it back. `BvZeroExtOp` and `BvSignExtOp` carry it.68    pub const extra = "extra";69    /// The key of the number of positions a rotation turns a bit-vector, `amount`, held as an70    /// integer attribute. The two rotation operations store the rotation amount under this key, and71    /// their `getAmount` functions read it back. `BvRotlOp` and `BvRotrOp` carry it.72    pub const amount = "amount";73};

1pub const names = @import("names.zig");