Скажем, я пишу простой код с квантификаторами, как показано ниже:
from z3 import *
s = SolverFor("LIA")
x1, y1 = Ints('x1 y1')
s.add(ForAll(x1, Implies(x1>=0, Exists(y1, (y1>x1)))))
печать (s.check()) печать (s.model())
Результат:
sat
[ ]
Разве это не должно выводить значение y1, для которого оно выполнимо?
И что это будет за значение? Обратите внимание, что значение y1 зависит от x1 в вашей формуле, поэтому не имеет смысла печатать только y1.
В общем, как только вы зайдете под универсальный квантор, z3 больше не сможет печатать значения переменных. Чтобы сделать это осмысленно, ему пришлось бы печатать все универсальные префиксы, и если бы все ваши домены не были конечными, это не имело бы смысла. (И это было бы полезно.)
