В качестве примера возьмем следующее:
from z3 import *
a, b, c, d, e = Bools('a b c d e')
s = Solver()
s.add(Implies(a, b))
s.add(Implies(c, d))
s.add(a)
print s.check()
print s.model()
z3 возвращает:
sat
[a = True, b = True, c = False, d = False]
модель, которая говорит, что c и d ложны. Но на самом деле эти две переменные могут быть либо истинными, либо ложными. Кажется, что z3 возвращает модель, которая присваивает False переменным решения (то есть переменным, значения которых не имеют значения) по умолчанию. Есть ли способ получить эти переменные решения? В этом примере это [c, d, e].