z3 在基于假设的增量求解中要慢得多

如何解决z3 在基于假设的增量求解中要慢得多

总结一下，我的问题会涉及到对多个“路径”的一些分析，每个路径对应一个约束。所有约束都将与带有 Implies 的 bool 关联并添加到求解器中。

我注意到在有大约 100 个约束之后，所有后续的假设检查（使用新的求解器立即完成）变得明显变慢，有些甚至会挂起几分钟。

对 smt 求解器或 z3 内部没有太多了解，我很好奇为什么会这样？因为无论如何我们都禁用了大部分约束。例如：

编辑：smt 文件转储位于 https://pastebin.com/4Ja2mKJg 在下面运行时，它会卡住几分钟，但是当运行其他不相关的约束时，它会立即完成。

from z3 import *

s = Solver()
s.from_file("test.smt")  # ~70 constraints
i = Bools("assume13 assume22 assume26 assume20 assume76 assume29")
print(s.check(i))    # stuck
print(s.model())

编辑 2：使用 z3.Then('simplify','smt') 策略可将运行时间显着减少到约 2 秒，即使没有预期的那么快。

编辑 3：进行了一些挖掘，看起来设置 smt.auto_config = False 和 smt.relevancy = 0 会加快速度，同时仍然使用增量求解器，这与每个 check() 将从新鲜。