问题描述
总结一下，我的问题会涉及到对多个“路径”的一些分析，每个路径对应一个约束。所有约束都将与带有 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() 将从新鲜。
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）