如何从 z3py 计算中得到结果？
How to get result from z3py calculation?
我想用z3py来说明下面的家谱练习（pa是“parent”，grpa是“grand-parent”）
pa(Rob,Kev) ∧ pa(Rob,Sama) ∧ pa(Sama,Tho) ∧ pa(Dor,Jim) ∧ pa(Bor,Jim) ∧ pa(Bor,Eli) ∧ pa(Jim ,Tho) ∧ pa(Sama,Samu) ∧ pa(Jim,Samu) ∧ pa(Zel,Max) ∧ pa(Samu,Max)
∀X,Y,Z pa(X,Z) ∧ pa(Z,Y) → grpa(X,Y)
练习在于找出 X 的哪个值具有以下内容：
∃X grpa(Rob,X) ∧ pa(X,Max)
（答案是：对于 X == Samu。）我想在 z3py 中重写这个问题，所以我引入了一个新的排序 Hum（对于“人类”）并编写了以下内容：
import z3
Hum = z3.DeclareSort('Hum')
pa = z3.Function('pa',Hum,Hum,z3.BoolSort())
grpa = z3.Function('grpa',Hum,Hum,z3.BoolSort())
Rob,Kev,Sama,Tho,Dor,Jim,Bor,Eli,Samu,Zel,Max = z3.Consts('Rob Kev Sama Tho Dor Jim Bor Eli Samu Zel Max', Hum)
s=z3.Solver()
for i,j in ((Rob,Kev),(Rob,Sama),(Sama,Tho),(Dor,Jim),(Bor,Jim),(Bor,Eli),(Jim,Tho),(Sama,Samu),(Jim,Samu),(Zel,Max),(Samu,Max)):
s.add(pa(i,j))
x,y,z=z3.Consts('x y z',Hum)
whi=z3.Const('whi',Hum)
s.add(z3.ForAll([x,y,z],z3.Implies(z3.And(pa(x,z),pa(z,y)),grpa(x,y))))
s.add(z3.Exists(whi,z3.And(grpa(Rob,whi),pa(whi,Max))))
代码被 Python 和
接受
print(s.check())
我明白了
sat
现在我知道有解决办法了。问题是：如何获得 whi 的值？
当我要求 print(s.model()[whi]) 时，我得到 None。当我请求 s.model().evaluate(whi) 时，我得到 whi，这不是很有帮助。
我怎样才能得到 whi 必须是 Samu 才能使最后一个公式成立的信息？
(辅助问题：为什么常量和变量没有区别？我把x,y,z定义成常量虽然是变量，但我有点疑惑。
为什么我不能写 x=Hum('x') 来表明 x 是一个 Hum 类型的变量？）
当你写这样的东西时：
X, Y = Const('X Y', Hum)
它 而不是 意味着您要声明两个常量，名称为 X 和 Y，类型为 Hum。 （是的，这确实令人困惑！特别是如果你来自类似 Prolog 的背景！）
相反，它的意思是说有两个对象 X 和 Y，它们属于 Hum 类型。它甚至不意味着 X 和 Y 不同。它们很可能是相同的，除非您明确声明，如下所示：
s.assert(z3.Distinct([X, Y]))
这也可以解释您对常量和变量的困惑。在您的模型中，一切都是变量；你根本没有声明任何常量。
你关于 whi 为什么不是 Samu 的问题解释起来有点棘手，但它源于这样一个事实，即你所拥有的只是变量，根本没有常量。此外，whi 当用作量化变量时，在模型中永远不会有值：如果您想要一个变量的值，它必须是一个顶级声明的变量，它有自己的断言。这通常会让刚接触 z3py 的人感到困惑：当你对一个变量进行量化时，顶层声明只是一个技巧，只是为了在范围内获得一个名称，它实际上与量化变量无关。如果您发现这令人困惑，那么您并不孤单：这是一个 "hack" 可能最终对新手来说更令人困惑而不是帮助。如果您有兴趣，请在此处详细解释：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-quantifiers-and-lambda-binding 但我建议您只相信绑定变量 whi 以及您在顶层声明的内容 whi 只是两个不同的变量。一旦您更加熟悉 z3py 的工作原理，您可以查看此 hack 背后的细节和原因。
回到您的建模问题：您确实希望这些常量出现在您的模型中。特别是，你想说这些是我宇宙中的人类而不是其他人，他们都是不同的。 （有点像 Prolog 的封闭世界假设。）这种事情是通过 z3py 中所谓的枚举排序来完成的。以下是我将如何为您的问题建模：
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
我相信这就是您想要实现的目标。
注意z3的Horn-logic可以更好的表达此类问题。为此，请参见此处：https://rise4fun.com/Z3/tutorialcontent/fixedpoints。它是 z3 支持的扩展，在 SMT 求解器中不可用，使其更适合关系编程任务。
话虽如此，虽然使用 SMT 求解器确实可以表达这些类型的关系，但此类问题实际上并不是 SMT 求解器的设计目的。它们更适用于涉及算术、位向量、数组、未解释函数、浮点数等的无量词逻辑片段。尝试将这类问题作为学习练习总是很有趣，但如果这某种问题是您真正关心的，您应该真正坚持使用更适合这种建模的 Prolog 及其变体。
我想用z3py来说明下面的家谱练习（pa是“parent”，grpa是“grand-parent”）
pa(Rob,Kev) ∧ pa(Rob,Sama) ∧ pa(Sama,Tho) ∧ pa(Dor,Jim) ∧ pa(Bor,Jim) ∧ pa(Bor,Eli) ∧ pa(Jim ,Tho) ∧ pa(Sama,Samu) ∧ pa(Jim,Samu) ∧ pa(Zel,Max) ∧ pa(Samu,Max)
∀X,Y,Z pa(X,Z) ∧ pa(Z,Y) → grpa(X,Y)
练习在于找出 X 的哪个值具有以下内容：
∃X grpa(Rob,X) ∧ pa(X,Max)
（答案是：对于 X == Samu。）我想在 z3py 中重写这个问题，所以我引入了一个新的排序 Hum（对于“人类”）并编写了以下内容：
import z3
Hum = z3.DeclareSort('Hum')
pa = z3.Function('pa',Hum,Hum,z3.BoolSort())
grpa = z3.Function('grpa',Hum,Hum,z3.BoolSort())
Rob,Kev,Sama,Tho,Dor,Jim,Bor,Eli,Samu,Zel,Max = z3.Consts('Rob Kev Sama Tho Dor Jim Bor Eli Samu Zel Max', Hum)
s=z3.Solver()
for i,j in ((Rob,Kev),(Rob,Sama),(Sama,Tho),(Dor,Jim),(Bor,Jim),(Bor,Eli),(Jim,Tho),(Sama,Samu),(Jim,Samu),(Zel,Max),(Samu,Max)):
s.add(pa(i,j))
x,y,z=z3.Consts('x y z',Hum)
whi=z3.Const('whi',Hum)
s.add(z3.ForAll([x,y,z],z3.Implies(z3.And(pa(x,z),pa(z,y)),grpa(x,y))))
s.add(z3.Exists(whi,z3.And(grpa(Rob,whi),pa(whi,Max))))
代码被 Python 和
接受print(s.check())
我明白了
sat
现在我知道有解决办法了。问题是：如何获得 whi 的值？
当我要求 print(s.model()[whi]) 时，我得到 None。当我请求 s.model().evaluate(whi) 时，我得到 whi，这不是很有帮助。
我怎样才能得到 whi 必须是 Samu 才能使最后一个公式成立的信息？
(辅助问题：为什么常量和变量没有区别？我把x,y,z定义成常量虽然是变量，但我有点疑惑。
为什么我不能写 x=Hum('x') 来表明 x 是一个 Hum 类型的变量？）
当你写这样的东西时：
X, Y = Const('X Y', Hum)
它 而不是 意味着您要声明两个常量，名称为 X 和 Y，类型为 Hum。 （是的，这确实令人困惑！特别是如果你来自类似 Prolog 的背景！）
相反，它的意思是说有两个对象 X 和 Y，它们属于 Hum 类型。它甚至不意味着 X 和 Y 不同。它们很可能是相同的，除非您明确声明，如下所示：
s.assert(z3.Distinct([X, Y]))
这也可以解释您对常量和变量的困惑。在您的模型中，一切都是变量；你根本没有声明任何常量。
你关于 whi 为什么不是 Samu 的问题解释起来有点棘手，但它源于这样一个事实，即你所拥有的只是变量，根本没有常量。此外，whi 当用作量化变量时，在模型中永远不会有值：如果您想要一个变量的值，它必须是一个顶级声明的变量，它有自己的断言。这通常会让刚接触 z3py 的人感到困惑：当你对一个变量进行量化时，顶层声明只是一个技巧，只是为了在范围内获得一个名称，它实际上与量化变量无关。如果您发现这令人困惑，那么您并不孤单：这是一个 "hack" 可能最终对新手来说更令人困惑而不是帮助。如果您有兴趣，请在此处详细解释：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-quantifiers-and-lambda-binding 但我建议您只相信绑定变量 whi 以及您在顶层声明的内容 whi 只是两个不同的变量。一旦您更加熟悉 z3py 的工作原理，您可以查看此 hack 背后的细节和原因。
回到您的建模问题：您确实希望这些常量出现在您的模型中。特别是，你想说这些是我宇宙中的人类而不是其他人，他们都是不同的。 （有点像 Prolog 的封闭世界假设。）这种事情是通过 z3py 中所谓的枚举排序来完成的。以下是我将如何为您的问题建模：
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
我相信这就是您想要实现的目标。
注意z3的Horn-logic可以更好的表达此类问题。为此，请参见此处：https://rise4fun.com/Z3/tutorialcontent/fixedpoints。它是 z3 支持的扩展，在 SMT 求解器中不可用，使其更适合关系编程任务。
话虽如此，虽然使用 SMT 求解器确实可以表达这些类型的关系，但此类问题实际上并不是 SMT 求解器的设计目的。它们更适用于涉及算术、位向量、数组、未解释函数、浮点数等的无量词逻辑片段。尝试将这类问题作为学习练习总是很有趣，但如果这某种问题是您真正关心的，您应该真正坚持使用更适合这种建模的 Prolog 及其变体。