lib/smt/src/choir/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! A checker that asks an SMT solver about a program can state its questions as formulas in the
 2 //! same intermediate representation as the program. The namespace defines those formulas as the
 3 //! operations and types of one dialect: Boolean, fixed-width bit-vector and array formulas,
 4 //! applications of uninterpreted functions, and named assertions.
 5 //!
 6 //! A checker builds one formula per property it must check, names each assertion and gives it a
 7 //! group label, and later reads the assertions back to hand them to a solver. Code that reads a
 8 //! formula back needs each value's type to carry what a solver needs: a bit-vector its width, an
 9 //! array its index width and its element width.
10 //!
11 //! Operators change width: concatenation adds the widths of its operands, extraction keeps a range
12 //! of bits, extension adds bits, and reading an array yields its element width. The type of such a
13 //! result depends on the operands' types and on numbers the operation carries. Other operators need
14 //! Boolean operands or operands of one type, and code that builds an operation from values made
15 //! elsewhere can pass values that break those rules. The representation finds the dialect that owns
16 //! an operation or a type from the first part of its name, so a context has to know the dialect
17 //! before it can make the dialect's operations and types.
18 //!
19 //! [MLIR](https://mlir.llvm.org/), a compiler framework from the LLVM project, groups the
20 //! operations and types of one domain into a dialect that a context loads, and names each operation
21 //! by its dialect's name, a dot and a short name. Its operations produce typed results that later
22 //! operations take as operands. [SMT-LIB](https://smt-lib.org/), the standard text language of SMT
23 //! solvers, defines theories of Booleans, fixed-size bit-vectors and arrays and names their
24 //! operators. The dialect takes those three theories, and most of its operations take the SMT-LIB
25 //! operator's name.
26 //!
27 //! The operations form one dialect, `smt`, of the compiler intermediate representation the package
28 //! depends on (*Choir*), which follows MLIR's model. Each operation's name is `smt.` followed by a
29 //! short name. For 27 of the 42 operations the short name is the SMT-LIB operator's name, such as
30 //! `smt.bvadd`, `smt.bvult` and `smt.bvuaddo`. The other 15 operations take short names of the
31 //! dialect's own, such as `smt.eq` for the SMT-LIB operator `=`, `smt.bvzeroext` for `zero_extend`,
32 //! and `smt.var` for a declared constant. The three types are `smt.bool`, `smt.bv` and `smt.array`.
33 //! A bit-vector type carries its width as decimal text, such as `64`, and an array type maps
34 //! bit-vectors to bit-vectors and carries its index width and element width as text, such as
35 //! `8:32`. Only the rotation, width-changing and array operations check their operands' types when
36 //! they are created, and the width-changing and array operations compute their result's width from
37 //! those types. For every other rule (Boolean operands, operands of one type, a result of the
38 //! operands' type), the dialect registers the rule with the context, and the IR's verifier
39 //! (`ir.verifyOperation`) checks it. A caller makes the dialect known to a context in one of three
40 //! ways. `registerDialect` records a loader that the context runs when it first meets the name
41 //! `smt`, `loadDialect` loads the dialect at once, and each type getter of `SmtDialect` loads the
42 //! dialect on first use. The package has no function that turns these operations into its own terms
43 //! or into clauses. A caller reads the assertions back and builds one term for each operation, with
44 //! the term operator of the same meaning. The namespace exports its two files as `dialect` and
45 //! `names`, and it re-exports `SmtDialect`, `registerDialect`, `loadDialect` and `registry` from
46 //! `dialect` and `type_names` and `attr_names` from `names`.
47 pub const dialect = @import("dialect.zig");
48 pub const names = @import("names.zig");
49 
50 pub const attr_names = names.attr_names;
51 pub const loadDialect = dialect.loadDialect;
52 pub const registerDialect = dialect.registerDialect;
53 pub const registry = dialect.registry;
54 pub const SmtDialect = dialect.SmtDialect;
55 pub const type_names = names.type_names;