lib/smt/src/choir/names.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! Code that reads a formula back from an intermediate representation tells its types apart and
 2 //! 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 its
 4 //! 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. The
 9 //! attribute keys are plain words with no prefix. `name` belongs to variables, function
10 //! applications and assertions, `group` to assertions, `value` to constants, `high` and `low` to
11 //! 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 other
13 //! struct with attributes in `SmtDialect` sets them in `create`, and each operation's struct reads
14 //! them through getters, so a caller uses the keys to set or read an attribute on an operation it
15 //! builds or holds without that struct.
16 /// The names of the dialect's three types, `boolean`, `bv` and `array`. Code that turns a type back
17 /// 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` build
19 /// types under them. The namespace and the `dialect` file re-export it.
20 pub const type_names = struct {
21     /// The name of the Boolean type, `smt.bool`. Code that turns a type into a solver sort compares
22     /// 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 this
26     /// constant before it reads a bit-vector's width. Each bit-vector type carries its width as
27     /// decimal text, such as `64`, in a key separate from this name, and this name stays the same
28     /// 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 this
32     /// constant before it reads an array's widths. Each array type carries its index width and its
33     /// element width as text, such as `8:32`, in a key separate from this name, and this name stays
34     /// the same for every pair of widths. `SmtDialect.getArrayType` builds these types, and
35     /// `SmtDialect.arrayShape` reads the widths back.
36     pub const array = "smt.array";
37 };
38 
39 /// The keys of the seven attributes the dialect's operations carry. The operation structs of
40 /// `SmtDialect` set and read every attribute under these keys, and a caller that reads an attribute
41 /// straight from an `ir.Operation` uses the same key. Each operation's specification lists the keys
42 /// of its attributes, and its struct's getters read the attributes back. The namespace and the
43 /// `dialect` file re-export it.
44 pub const attr_names = struct {
45     /// The key of a name, `name`, held as a string attribute. The structs of variables, function
46     /// applications and assertions store and read a name under this key. It names a variable
47     /// (`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, and
51     /// `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 under
54     /// this key, and their `getValue` functions read it back. `BoolConstOp` holds the value as a
55     /// 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 integer
58     /// 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, and
63     /// `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. The
66     /// zero and sign extension operations store the number of added bits under this key, and their
67     /// `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 an
70     /// integer attribute. The two rotation operations store the rotation amount under this key, and
71     /// their `getAmount` functions read it back. `BvRotlOp` and `BvRotrOp` carry it.
72     pub const amount = "amount";
73 };