amzn-smt-ir

amzn-smt-ir is a Rust library for working with SMT-LIB formulas.

Representation

Logics

SMT-LIB logics are represented by the amzn_smt_ir::Logic trait, which encapsulates the type of operations in the logic (more on this later) as well as whether quantifiers and uninterpreted functions are allowed (corresponding to the QF (Quantifier-Free) and UF (including Uninterpreted Functions) prefixes in SMT-LIB logic names.) Logics that wish to leave out non-Core operations, quantifiers, or uninterpreted functions can specify amzn_smt_ir::Void as the corresponding associated type -- since Void is uninhabitable, it will be impossible at the type level for terms in the resulting logic to contain the corresponding components.

Operations

Note: This library calls SMT functions "operations" to avoid confusion with Rust's Fn traits.

SMT-LIB theory functions are represented as enums. For instance, a simplified version of SMT-LIB Core might look like the following:

enum CoreOp<Term> {
	Not(Term),
	And(Vec<Term>),
	Ite(Term, Term, Term),
}

This makes it possible to encode the distinctions between different functions at the type level e.g. encoding that not is a unary function, ite is ternary, and and may take any number of arguments (since it is annotated with :left-assoc).

Note: Indexed functions are defined as containing an array of indices as their first tuple field e.g. Extract([IIndex; 2], Term) for the bit-vector extract function.

Pre-defined Logics and their corresponding operation types are defined in the amzn_smt_ir::logic module. Users can also define custom Logics and operations using the provided derive macros to implement the expected traits (see the "Derives" section).

Terms

Terms are represented by amzn_smt_ir::Term<L: Logic>, which represents an SMT term in logic L:

enum Term<T: Logic> {
    /// A constant value.
    Constant(IConst),

    /// A variable representing a value.
    Variable(IVar<T::Var>),

    /// An operation in SMT-LIB's Core theory.
    CoreOp(ICoreOp<T>),

    /// A non-Core operation.
    OtherOp(IOp<T>),

    /// An uninterpreted function.
    UF(IUF<T>),

    /// Simultaneous let-binding e.g. `(let ((x true) (y false)) (and x y))`
    Let(ILet<T>),

    /// SMT-LIB `match` expression -- not yet supported
    Match(IMatch<T>),

    /// Quantified term.
    Quantifier(IQuantifier<T>),
}

Note: Because Core is implicitly included in every logic, CoreOps may be present in any type of Term.

The I prefixes of type names signal that the types are interned to prevent duplication (also called hash-consed). I-prefixed types are essentially pointers to a unique copy of the data they correspond to stored in a lookup table with hashes as keys. When a value of one of these types is instantiated, the corresponding table is first checked to see if it contains the value; if it does, a pointer to the existing copy is returned; if not, the value is stored in the table and a pointer to the new copy is returned. I-prefixed types implement most of Rust's standard traits by delegating to the inner value, although PartialEq and Eq are implemented with pointer equality (equivalent because there exists a unique copy of each value).

Traversals

The library provides two patterns for traversing IR nodes.

Computing

The Visit family of traits (Visitor, Visit, and SuperVisit) provide a visitor pattern for traversing IR nodes and building up some result (stored in a Visitor). See the traits' respective docs for more details.

Transforming

The Fold family of traits (Folder, Fold, and SuperFold) provide a pattern for transforming IR nodes into other IR nodes. See the traits' respective docs for more details.

Derives

The library provides three derive macros for generating trait implementations expected of types used as operations (i.e. the L::Op of an L: Logic):

• Operation: implements the Operation trait, which determines how an operation is parsed from a function symbol and list of arguments, the Iterate trait, which allows for constructing an iterator of function arguments (used through the Args trait), as well as Debug, Display, and From implementations for converting the type to IOp and Term.
• Visit: implements the SuperVisit trait for performing the standard recursive traversal of an operation enum.
• Fold: implements the SuperFold trait for performing the standard recursive transformation of an operation enum.