加速解决Z3问题的一般原则和方向

【问题标题】：General principles and directions to accelerate the solving of Z3 problem加速解决Z3问题的一般原则和方向
【发布时间】：2022-01-23 09:24:39
【问题描述】：

我正在使用 Z3 解决一个问题，我发现它非常慢。有没有关于 Z3 求解器加速的一般原则或指导方针？如：

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

正如克里斯托夫所提到的，没有“一刀切”的建议可以统一适用于所有问题。但是，这种性能问题经常出现，之前已经讨论过堆栈溢出，并总结了如何考虑可伸缩性：Scalability of z3

我将首先查看此答案，看看您是否有具体问题。特别是，分享您的实际问题的详细信息以及您如何在 z3 中对其进行建模对于获得更好的指导至关重要。

【讨论】：

【解决方案2】：

没有普遍适用的规则；否则我们会实施并自动化它们。如果没有有关问题的更多信息，就无法帮助您。进行性能调查的好地方是Z3 GitHub discussion。

【讨论】：