Когда вы пишете что-то вроде:
X, Y = Const('X Y', Hum)
Это не означает, что вы объявляете две константы с именами X и Y сорта Hum. (Да, это действительно сбивает с толку! Особенно, если вы исходите из фона, похожего на Пролог!)
Вместо этого все, что это означает, это то, что вы говорите, что есть два объекта X и Y, которые принадлежат к роду Hum. Это даже не означает, что X и Y различны. Они вполне могут быть одинаковыми, если вы явно не укажете это, например:
s.assert(z3.Distinct([X, Y]))
Это также может объяснить вашу путаницу в отношении констант и переменных. В вашей модели все является переменной; вы вообще не объявили никаких констант.
Ваш вопрос о том, почему whi не является Samu, немного сложнее объяснить, но это связано с тем фактом, что все, что у вас есть, это переменные, а не постоянные на всех. Кроме того, whi при использовании в качестве количественной переменной никогда не будет иметь значения в модели: если вы хотите получить значение для переменной, это должна быть объявленная переменная верхнего уровня со своими собственными утверждениями. Обычно это сбивает с толку тех, кто плохо знаком с z3py: когда вы выполняете количественную оценку по переменной, объявление верхнего уровня - это просто уловка, позволяющая просто получить имя в области видимости, оно на самом деле не относится к количественной переменной. Если вы находите, что это сбивает с толку, вы не одиноки: это «хак», который, возможно, в конечном итоге оказался более запутанным, чем полезным для новичков. Если вам интересно, это подробно объясняется здесь: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec -quantifiers-and-lambda-binding Но я бы рекомендовал просто принять это на веру в то, что связанная переменная whi и что вы объявленные на верхнем уровне как whi это просто две разные переменные. Как только вы ознакомитесь с принципами работы z3py, вы сможете изучить детали и причины этого взлома.
Возвращаясь к вашему вопросу моделирования: вы действительно хотите, чтобы эти константы присутствовали в вашей модели. В частности, вы хотите сказать, что это люди в моей вселенной и никто другой, и все они разные. (Вроде как предположение Пролога о замкнутом мире.) Такого рода вещи выполняются с помощью так называемой нумерации в z3py. Вот как я бы go смоделировал вашу проблему:
from z3 import *
# Declare an enumerated sort. In this declaration we create 'Human' to be a sort with
# only the elements as we list them below. They are guaranteed to be distinct, and further
# any element of this sort is guaranteed to be equal to one of these.
Human, (Rob, Kev, Sama, Tho, Dor, Jim, Bor, Eli, Samu, Zel, Max) \
= EnumSort('Human', ('Rob', 'Kev', 'Sama', 'Tho', 'Dor', 'Jim', 'Bor', 'Eli', 'Samu', 'Zel', 'Max'))
# Uninterpreted functions for parent/grandParent relationship.
parent = Function('parent', Human, Human, BoolSort())
grandParent = Function('grandParent', Human, Human, BoolSort())
s = Solver()
# An axiom about the parent and grandParent functions. Note that the variables
# x, y, and z are merely for the quantification reasons. They don't "live" in the
# same space when you see them at the top level or within a ForAll/Exists call.
x, y, z = Consts('x y z', Human)
s.add(ForAll([x, y, z], Implies(And(parent(x, z), parent(z, y)), grandParent(x, y))))
# Express known parenting facts. Note that unlike Prolog, we have to tell z3 that
# these are the only pairs of "parent"s available.
parents = [ (Rob, Kev), (Rob, Sama), (Sama, Tho), (Dor, Jim) \
, (Bor, Jim), (Bor, Eli), (Jim, Tho), (Sama, Samu) \
, (Jim, Samu), (Zel, Max), (Samu, Max) \
]
s.add(ForAll([x, y], Implies(parent(x, y), Or([And(x==i, y == j) for (i, j) in parents]))))
# Find what makes Rob-Max belong to the grandParent relationship:
witness = Const('witness', Human)
s.add(grandParent(Rob, Max))
s.add(grandParent(Rob, witness))
s.add(parent(witness, Max))
# Let's see what witness we have:
print s.check()
m = s.model()
print m[witness]
Для этого z3 говорит:
sat
Samu
, чего, я считаю, вы и добились.
Обратите внимание, что Horn-logi c из z3 может express решить такие проблемы приятнее. Об этом см. Здесь: https://rise4fun.com/Z3/tutorialcontent/fixedpoints. Это расширение, которое поддерживает z3, недоступное в решателях SMT, что делает его более подходящим для задач реляционного программирования.
Сказав это, в то время как действительно возможно express такого рода отношений с использованием SMT решатель, такие проблемы на самом деле не предназначены для решателей SMT. Они гораздо больше подходят для фрагментов логики без количественных показателей, которые включают в себя арифметику c, битовые векторы, массивы, неинтерпретированные функции, числа с плавающей точкой и т. Д. c. Всегда полезно испытывать подобные проблемы в качестве учебного упражнения, но если проблема такого рода - то, что вас действительно волнует, вам следует придерживаться Prolog и его вариантов, которые гораздо больше подходят для такого типа моделирования.