tiny.smt.choir.names.type_names

1/// The names of the dialect's three types, `boolean`, `bv` and `array`. Code that turns a type back2/// into a solver sort compares the type's name with these constants to tell the three types apart.3/// The dialect registers its types under these names, and the type getters of `SmtDialect` build4/// types under them. The namespace and the `dialect` file re-export it.5pub const type_names = struct {6    /// The name of the Boolean type, `smt.bool`. Code that turns a type into a solver sort compares7    /// the type's name with this constant to recognize a Boolean value. `SmtDialect.getBoolType`8    /// returns the type.9    pub const boolean = "smt.bool";10    /// The name every bit-vector type shares, `smt.bv`. Code compares a type's name with this11    /// constant before it reads a bit-vector's width. Each bit-vector type carries its width as12    /// decimal text, such as `64`, in a key separate from this name, and this name stays the same13    /// for every width. `SmtDialect.getBitVecType` builds these types, and `SmtDialect.bitVecWidth`14    /// reads the width back.15    pub const bv = "smt.bv";16    /// The name every array type shares, `smt.array`. Code compares a type's name with this17    /// constant before it reads an array's widths. Each array type carries its index width and its18    /// element width as text, such as `8:32`, in a key separate from this name, and this name stays19    /// the same for every pair of widths. `SmtDialect.getArrayType` builds these types, and20    /// `SmtDialect.arrayShape` reads the widths back.21    pub const array = "smt.array";22};