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

项

术语通过 amzn_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 特性构建函数参数的迭代器，以及为将类型转换为 IOp 和 Term 实现的 Debug、Display 和 From。
• Visit：实现 SuperVisit 特性，以执行操作枚举的标准递归遍历。
• Fold：实现 SuperFold 特性，以执行操作枚举的标准递归转换。