python - Z3 Solver() 中约束的大小

Question

有没有办法让我们知道解算器中添加了多少约束？例如，我们初始化一个 z3 求解器 s = Solver()，然后使用 s.add() 添加约束。我们如何获得最终添加到求解器中的约束数量？

Answer 1

您可以使用断言方法:

from z3 import *

s = Solver()

i = Int('i')
s.add (i > 1)
s.add (i < 12)

print s.assertions()
print len(s.assertions())

打印:

[i > 1, i < 12]
2