我需要证明有关地图数据结构的一些属性(例如空性，域，更新等(。Z3 中是否支持地图？
我找到了一个提案：https://www.kroening.com/smt-lib-lsm.pdf 及其相关的SMT理论 http://www.philipp.ruemmer.org/smt-lsm/SMT-LIB.tar.gz。该提案将映射视为具有相应公理的数组。但是，我在定理证明器中找不到现成的实现。
如果我想在 Z3 中支持地图，有什么建议可以开始吗？
我最好的选择是我需要在 Z3 中添加一个新理论，它假设对 Z3 的实现有很好的了解 - 这个假设在我的情况下并不成立。
Z3 没有对地图的原生支持。最好的办法是暂时使用记录数组(代数数据类型(来模拟它们。
将理论添加到 SMT 求解器是一项艰巨的任务。我建议在走这条路之前先探索数组和记录。
或者，看看Dafny的地图公理：
https://github.com/Microsoft/dafny/blob/master/Binaries/DafnyPrelude.bpl#L1113
Dafny被广泛使用(用于形式化方法工具;-((，因此它的公理化相当成熟。
映射公理用 Boogie 语言表示，但将 Boogie 公理化转换为 SMT-LIB 通常是直截了当的。