tiny.smt.choir

1//! A checker that asks an SMT solver about a program can state its questions as formulas in the2//! same intermediate representation as the program. The namespace defines those formulas as the3//! 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 a7//! group label, and later reads the assertions back to hand them to a solver. Code that reads a8//! formula back needs each value's type to carry what a solver needs: a bit-vector its width, an9//! array its index width and its element width.10//!11//! Operators change width: concatenation adds the widths of its operands, extraction keeps a range12//! of bits, extension adds bits, and reading an array yields its element width. The type of such a13//! result depends on the operands' types and on numbers the operation carries. Other operators need14//! Boolean operands or operands of one type, and code that builds an operation from values made15//! elsewhere can pass values that break those rules. The representation finds the dialect that owns16//! an operation or a type from the first part of its name, so a context has to know the dialect17//! 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 the20//! operations and types of one domain into a dialect that a context loads, and names each operation21//! by its dialect's name, a dot and a short name. Its operations produce typed results that later22//! operations take as operands. [SMT-LIB](https://smt-lib.org/), the standard text language of SMT23//! solvers, defines theories of Booleans, fixed-size bit-vectors and arrays and names their24//! operators. The dialect takes those three theories, and most of its operations take the SMT-LIB25//! operator's name.26//!27//! The operations form one dialect, `smt`, of the compiler intermediate representation the package28//! depends on (*Choir*), which follows MLIR's model. Each operation's name is `smt.` followed by a29//! short name. For 27 of the 42 operations the short name is the SMT-LIB operator's name, such as30//! `smt.bvadd`, `smt.bvult` and `smt.bvuaddo`. The other 15 operations take short names of the31//! 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 maps34//! bit-vectors to bit-vectors and carries its index width and element width as text, such as35//! `8:32`. Only the rotation, width-changing and array operations check their operands' types when36//! they are created, and the width-changing and array operations compute their result's width from37//! those types. For every other rule (Boolean operands, operands of one type, a result of the38//! operands' type), the dialect registers the rule with the context, and the IR's verifier39//! (`ir.verifyOperation`) checks it. A caller makes the dialect known to a context in one of three40//! ways. `registerDialect` records a loader that the context runs when it first meets the name41//! `smt`, `loadDialect` loads the dialect at once, and each type getter of `SmtDialect` loads the42//! dialect on first use. The package has no function that turns these operations into its own terms43//! or into clauses. A caller reads the assertions back and builds one term for each operation, with44//! the term operator of the same meaning. The namespace exports its two files as `dialect` and45//! `names`, and it re-exports `SmtDialect`, `registerDialect`, `loadDialect` and `registry` from46//! `dialect` and `type_names` and `attr_names` from `names`.47pub const dialect = @import("dialect.zig");48pub const names = @import("names.zig");4950pub const attr_names = names.attr_names;51pub const loadDialect = dialect.loadDialect;52pub const registerDialect = dialect.registerDialect;53pub const registry = dialect.registry;54pub const SmtDialect = dialect.SmtDialect;55pub const type_names = names.type_names;

1pub const choir = @import("choir/root.zig");