我需要证明 map 数据结构的一些性质(如空性、域、更新等)。 Z3 是否支持 map ？
我找到了一个提案:https://www.kroening.com/smt-lib-lsm.pdf 及其相关的SMT理论http://www.philipp.ruemmer.org/smt-lsm/SMT-LIB.tar.gz .该提案将映射视为具有相应公理的数组。但是，我无法在定理证明器中找到现成的实现。
如果我想在 Z3 中支持 map ，有没有关于从哪里开始的建议？
我最好的选择是，我需要在 Z3 中添加一个新理论，该理论假设对 Z3 的实现有很好的了解——假设在我的情况下不成立。
最佳答案
Z3 本身不支持 map 。最好的办法是暂时使用记录数组(代数数据类型)来模拟它们。
将理论添加到 SMT 求解器是一项重大任务。我建议先探索数组和记录，然后再沿着这条路走下去。
关于z3 - Z3中的 map 数据结构，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/52313122/