为什么z3.And()运行缓慢？

Question

为什么z3.And()运行缓慢？

4

我正在使用Z3 Python绑定创建一个And表达式，通过z3.And(exprs),其中exprs是一个包含48000个布尔变量的等式约束的Python列表。在2.6GHz处理器的MBP上，此操作需要2秒钟的时间。可能是什么问题导致这种情况？这是否与z3 Python绑定有关？您有没有优化这种构造的任何想法？顺便说一下，在我的实验中，构造这些表达式所需的时间比解决结果公式的时间更长:)

- Venkatesh-Prasad Ranganath

通常情况下，没有Python绑定需要多长时间？你计算过计算时间与构建时间的比吗？ - Flavian Hautbois

我没有尝试过不使用Python绑定。然而，使用Python绑定，tmp1[i] = value == z3.is_false(interpretation) 耗时约为0.0001秒，而 n.append(z3.And(tmp1)) 则需要约2秒。至于检查时间，初始检查需要8.67秒，而随后的检查（加入更多约束条件（来自上述的tmp1））只需要0.3秒。 - Venkatesh-Prasad Ranganath

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Nikolaj Bjorner · Accepted Answer

使用Python的Z3通常会很慢。它包括参数检查和编组（包括_coerce_expr等）。为了实现可扩展性，最好使用其他绑定或尽可能绕过Python运行时。