Размер ограничений в Z3 Solver ()

Question

Есть ли у нас способ узнать, сколько ограничений было добавлено в решатель? Например, мы инициализируем решатель z3 s = Solver() и затем добавляем к нему ограничения, используя s.add(). Как мы можем получить количество ограничений, которые были окончательно добавлены в решатель?

Answer 1

Вы можете использовать метод assertions:

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