python – 为什么z3.And()慢？
作者：互联网
我使用Z3 Python绑定通过z3.And(exprs)创建一个And表达式,其中exprs是一个对布尔变量的48000个相等约束的python列表.在具有2.6GHz处理器的MBP上,此操作需要2秒.
我能做错什么？这是z3 Python绑定的问题吗？关于如何优化这种结构的任何想法？
顺便说一句,在我的实验中,这些表达式的构造花费的时间比解决得到的公式要多:)
解决方法:
在Python上使用Z3通常很慢.它包括参数检查和编组(_coerce_expr等).
对于可伸缩性,您最好使用其他绑定之一或尽可能绕过Python运行时.
标签：python,z3,z3py 来源： https://codeday.me/bug/20190703/1362864.html