在SMT-LIB中表示C结构

Question

我正在尝试使用Z3求解器(它在SMT-LIB上工作)来对涉及结构的C程序进行推理。我想用某种方式来表示结构是一个包含SMT-LIB中其他变量的变量，但我找不到这样做的方法。有没有人知道在SMT-LIB中表示C结构的方法？

Answer 1

您可以使用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都支持它。求解器的质量可能会因您使用的功能而有所不同，但如果您只是使用数据类型来构造和解构数值，那么它应该可以开箱即用。