【发布时间】：2021-01-13 14:55:29
【问题描述】：
我正在尝试使用 Z3 求解器（在 SMT-LIB 上工作）来推理涉及结构的 C 程序。我想要某种方式来表示该结构是一个包含 SMT-LIB 中其他变量的变量，但我找不到这样做的方法。有人知道在 SMT-LIB 中表示 C 结构的方法吗？
【问题讨论】：
【发布时间】：2021-01-13 14:55:29
【问题描述】：
您可以使用 SMTLib 2.6 的代数数据类型功能对结构进行建模。请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.2.3 节
此功能不仅允许常规结构声明，还允许递归声明；即，您还可以对具有相同类型字段的结构进行建模。
我应该补充一点，SMT 中的代数数据类型实际上比您需要的更通用，它们实际上可用于对使用不同代数构造函数构造的值进行建模。 （对于简单的记录案例，您只需使用一个构造函数。）
代数数据类型是 SMTLib 中的一项新功能，但 Z3 和 CVC4 都支持它。求解器质量可能会因您使用的功能而异，但如果您只是使用数据类型来构造和解构值，它应该可以开箱即用。
【讨论】：