问题描述
我正在尝试使用Z3求解器（在SMT-LIB上运行）来推理涉及结构的C程序。我想以某种方式表示该结构是一个包含SMT-LIB中其他变量的变量，但是我找不到实现此目的的方法。有谁知道在SMT-LIB中表示C结构的方法吗？
解决方法
您可以使用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都支持它。求解器的质量可能会因所使用的功能而异，但是，如果仅使用数据类型来构造和解构值，则解开器的工作原理非常简单。