有没有办法让我们知道解算器中添加了多少约束?例如,我们初始化一个 z3 求解器 s = Solver()
,然后使用 s.add()
添加约束。我们如何获得最终添加到求解器中的约束数量?
最佳答案
您可以使用断言
方法:
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
关于python - Z3 Solver() 中约束的大小,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/54099202/