预定义的 Logic 和它们相应的操作类型定义在 aws_smt_ir::logic 模块中。用户也可以使用提供的 derive 宏定义自定义 Logic 和操作，以实现预期的特性（请参阅 "Derives" 部分）。

项

术语通过以下格式表示：aws_smt_ir::Term<L: Logic>，它表示逻辑L中的SMT术语。

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>),
}

注意：因为Core被隐式包含在每种逻辑中，所以CoreOp可能存在于任何类型的Term中。

类型名称前的I前缀表示这些类型被内部化以防止重复（也称为哈希化）。带有I前缀的类型实际上是它们对应的唯一数据的指针，这些数据存储在以哈希值为键的查找表中。当一个这些类型的值被实例化时，首先检查相应的表是否包含该值；如果包含，则返回现有副本的指针；如果不包含，则在表中存储该值，并返回新副本的指针。I前缀的类型通过委派给内部值来实现Rust的大部分标准特质，尽管PartialEq和Eq是通过指针相等性实现的（由于每个值都存在唯一副本，因此等效）。

遍历

该库提供了两种遍历IR节点的模式。

计算

Visit系列特质（Visitor、Visit和SuperVisit）提供了遍历IR节点并构建某些结果（存储在Visitor中）的访问者模式。有关详细信息，请参阅特质的相应文档。

转换

Fold系列特质（Folder、Fold和SuperFold）提供了一种将IR节点转换为其他IR节点的模式。有关详细信息，请参阅特质的相应文档。

派生

该库提供了三个派生宏，用于生成用作操作的类型（即L::Op的L: Logic）所期望的特质实现。

• Operation：实现了Operation特质，该特质确定如何从函数符号和参数列表解析操作，实现了Iterate特质，该特质允许通过Args特质构建函数参数的迭代器，以及Debug、Display和From实现，用于将类型转换为IOp和Term。
• Visit：实现了用于执行操作枚举的标准递归遍历的SuperVisit特质。
• Fold：实现了用于执行操作枚举的标准递归转换的SuperFold特质。